ISO/IEC 23643:2020

Software and systems engineering - Capabilities of software safety and security verification tools

This document specifies requirements for the vendors and gives guidelines for both the users and the developers of software safety and security verification tools. The users of such tools include, but are not limited to, bodies performing verification and software developers who need to be aware and pay attention to safety and/or security of software. This document guides the verification tool vendors to provide as high-quality products as possible and helps the users to understand the capabilities and characteristics of verification tools. This document introduces use cases for software safety and security verification tools and entity relationship model related to them. This document also introduces tool categories for software safety and security verification tools and gives category specific guidance and requirements for the tool vendors and developers.

Ingénierie du logiciel et des systèmes — Capacités des outils de vérification de la sûreté et de la sécurité des logiciels

General Information

• Status: Published
• Publication Date: 11-Jun-2020
• ICS: 35.080 - Software
• Technical Committee: ISO/IEC JTC 1/SC 7 - Software and systems engineering
• Drafting Committee: ISO/IEC JTC 1/SC 7/WG 4 - Tools and environment
• Current Stage: 9060 - Close of review
• Completion Date: 02-Dec-2030

Overview

ISO/IEC 23643:2020 - "Software and systems engineering - Capabilities of software safety and security verification tools" defines capabilities, vendor requirements and user/developer guidance for tools that verify software safety and security. The standard focuses on verification of software artefacts (specifications, models, pseudo-code) via analysis and animation rather than execution testing. It is domain‑independent, excludes hardware, and is intended to improve the quality and transparency of software safety and security verification tools.

Key topics and technical scope

• Purpose and scope
  • Requirements for verification tool vendors and guidance for users and developers.
  • Clarifies differences between verification and validation; testing tools are excluded (see ISO/IEC 30130).
• Models and use cases
  • Introduces models, use cases and an entity‑relationship chart to help match tools to verification workflows.
• Tool categories covered
  • Specification and refinement tools
  • Model checking tools
  • Program analysis tools (static and dynamic program analysis is defined)
  • Proof tools (formal verification)
  • Monitoring tools
  • Programming rules checkers
  • Security categories: vulnerability analysis, security modeling, threat modeling
• Capabilities and requirements
  • Defines capabilities expected of safety and security verification tools and category‑specific guidance and requirements for vendors and developers.
  • Addresses common concerns such as false positives/false negatives, evaluator roles, and assurance levels.
• Operational context
  • Encourages continuous verification aligned with agile and continuous delivery practices.
  • Distinguishes software verification from system-level safety/security.

Practical applications and who uses it

ISO/IEC 23643:2020 is useful for:

• Verification tool vendors - to design, document and market tools that meet recognized capability and quality expectations.
• Software developers and V&V teams - to select and apply appropriate verification tools for safety‑critical and security‑sensitive software.
• Independent evaluators and certification bodies - to assess tool claims, capability, and fit for purpose.
• Safety/security engineers - to integrate model checking, formal verification, static analysis, runtime monitoring and threat/vulnerability modeling into development lifecycles.

Typical applications include verification of software in transportation, energy, IoT, medical devices and other safety‑critical systems where software defects or security vulnerabilities have high impact.

Related standards

• ISO/IEC 20741 (guidance for single tool capabilities)
• ISO/IEC 30130 (testing tools) - testing tools are covered there, while ISO/IEC 23643 focuses on analysis/animation of artefacts.

Keywords: ISO/IEC 23643:2020, software safety, security verification tools, model checking, program analysis, formal verification, vulnerability analysis, threat modeling, verification tool vendors.

Standards Content (Sample)

INTERNATIONAL ISO/IEC
STANDARD 23643
First edition
2020-06
Software and systems engineering —
Capabilities of software safety and
security verification tools
Ingénierie du logiciel et des systèmes — Capacités des outils de
vérification de la sûreté et de la sécurité des logiciels
Reference number
©
ISO/IEC 2020
© ISO/IEC 2020
All rights reserved. Unless otherwise specified, or required in the context of its implementation, no part of this publication may
be reproduced or utilized otherwise in any form or by any means, electronic or mechanical, including photocopying, or posting
on the internet or an intranet, without prior written permission. Permission can be requested from either ISO at the address
below or ISO’s member body in the country of the requester.
ISO copyright office
CP 401 • Ch. de Blandonnet 8
CH-1214 Vernier, Geneva
Phone: [phone]
Email: [e-mail]
Website: www.iso.org
Published in Switzerland
ii © ISO/IEC 2020 – All rights reserved

Contents Page
Foreword .iv
Introduction .v
1 Scope . 1
2 Normative references . 1
3 Terms and definitions . 1
4 Abbreviated terms . 6
5 Models for software safety and security verification tools . 7
6 Use cases of software safety and security verification tools . 9
6.1 General . 9
6.2 Verification for low criticality software .10
6.3 Verification for medium criticality software .10
6.4 Verification for high criticality software .11
7 Entity relationship chart of software safety and security verification .12
8 Categories, capabilities of and requirements for software safety and security
verification tools .13
8.1 General .13
8.2 Categories of software safety verification tools .13
8.2.1 General.13
8.2.2 Specification and refinement tools .13
8.2.3 Model checking tools .13
8.2.4 Program analysis tools . .14
8.2.5 Proof tools.14
8.2.6 Monitoring tools .14
8.2.7 Programming rules checkers .14
8.3 Categories of software security verification tools .15
8.3.1 General.15
8.3.2 Vulnerability analysis tools .15
8.3.3 Security modeling tools .15
8.3.4 Threat modeling tools .15
8.4 Capabilities of software safety and security verification tools .15
8.5 Common requirements for safety and security verification tools .19
8.6 Requirements for specification and refinement tools .20
8.7 Requirements for model checking tools .20
8.8 Requirements for program analysis tools .21
8.9 Requirements for proof tools .21
8.10 Requirements for monitoring tools.22
8.11 Requirements for programming rules checking tools .22
8.12 Requirements for vulnerability analysis tools .22
8.13 Requirements for security modeling tools .23
8.14 Requirements for threat modeling tools .23
Annex A (informative) Evaluation assurance levels of ISO/IEC 15408 common criteria .24
Annex B (informative) How to use this document with ISO/IEC 20741 .28
Bibliography .29
© ISO/IEC 2020 – All rights reserved iii

Foreword
ISO (the International Organization for Standardization) and IEC (the International Electrotechnical
Commission) form the specialized system for worldwide standardization. National bodies that
are members of ISO or IEC participate in the development of International Standards through
technical committees established by the respective organization to deal with particular fields of
technical activity. ISO and IEC technical committees collaborate in fields of mutual interest. Other
international organizations, governmental and non-governmental, in liaison with ISO and IEC, also
take part in the work.
The procedures used to develop this document and those intended for its further maintenance are
described in the ISO/IEC Directives, Part 1. In particular, the different approval criteria needed for
the different types of document should be noted. This document was drafted in accordance with the
editorial rules of the ISO/IEC Directives, Part 2 (see www .iso .org/ directives).
Attention is drawn to the possibility that some of the elements of this document may be the subject
of patent rights. ISO and IEC shall not be held responsible for identifying any or all such patent
rights. Details of any patent rights identified during the development of the document will be in the
Introduction and/or on the ISO list of patent declarations received (see www .iso .org/ patents) or the IEC
list of patent declarations received (see http:// patents .iec .ch).
Any trade name used in this document is information given for the convenience of users and does not
constitute an endorsement.
For an explanation of the voluntary nature of standards, the meaning of ISO specific terms and
expressions related to conformity assessment, as well as information about ISO's adherence to the
World Trade Organization (WTO) principles in the Technical Barriers to Trade (TBT) see www .iso .org/
iso/ foreword .html.
This document was prepared by Joint Technical Committee ISO/IEC JTC 1, Information technology,
Subcommittee SC 7, Software and systems engineering.
Any feedback or questions on this document should be directed to the user’s national standards body. A
complete listing of these bodies can be found at www .iso .org/ members .html.
iv © ISO/IEC 2020 – All rights reserved

Introduction
Since a few decades, the importance of software safety and security verification tools has increased for
several reasons: 1) rapidly increasing complexity of software applications and systems, 2) increasing
number of safety-critical systems through growing integration between software applications and
systems (e.g. in critical infrastructures), 3) the rapid increase of the number of cyber threats, and 4)
the urgent needs of safety in high and medium critical software-driven systems (e.g. transportation,
energy production, Internet of Things (IoT), and general purpose Operating Systems and middleware).
Additionally, the number of products and system development cases, where the origin of all software
components to be used is not exactly known, even for open-source applications, is increasing and thus
making safety and security verification and validation (V&V) essential.
This document restricts its point of view to software and excludes computing and any other hardware
from the context. In these other domains, other V&V methods and tools are used.
It is important to realize that verification of safety and security of software does not necessarily verify
the system safety and system security of a system using the software as a component. However, if a
system consists of software components which are not verified, the safety and security of the system
cannot be guaranteed at any level.
“Continuous everything”, including continuous software development and thus versioning delivery,
requires continuous software safety and security verification. At every new version, V&V needs to be
redone. The popular “agile development processes” permit shorter development iterations and more
frequent product delivery, and consequently this requires more frequent verification than traditional
development approaches. Verification is needed during software development as well as during
software maintenance, whenever safety or security of software can be endangered.
Validation answers the question “are we building the right product?”
Verification answers the question “are we building the product right?”
Software validation checks if the software product satisfies the intended use, such as defined in
requirements and specifications. In other words (ISO/IEC 17029): “purpose of validation is to find out,
whether a declared information (claim) is plausible”. Software verification checks if the specifications
and requirements are met either by running the software (testing) or by reviewing its artefacts
(specification, model, or pseudo code). The latter can consist of animating or analyzing statically one of
its artefacts. ISO/IEC 17029 defines that the “purpose of verification is to find out, whether a declared
information (claim) is truthful”. This document does not concern testing but animating and analyzing
the artefacts, because “testing tools” is already well covered by and is the subject of ISO/IEC 30130.
This document is prepared as one of the series of single tool capabilities which are used with
ISO/IEC 20741.
This document defines capabilities of and requirements for software safety and security verification tools.
This document is independent of the target application domains, as the languages, methods and
associated tools are of general purpose, and can fit into different kinds of problems (e.g. functional
specification languages can be used for any functional program).
© ISO/IEC 2020 – All rights reserved v

INTERNATIONAL STANDARD ISO/IEC 23643:2020(E)
Software and systems engineering — Capabilities of
software safety and security verification tools
1 Scope
This document specifies requirements for the vendors and gives guidelines for both the users and the
developers of software safety and security verification tools. The users of such tools include, but are
not limited to, bodies performing verification and software developers who need to be aware and pay
attention to safety and/or security of software. This document guides the verification tool vendors to
provide as high-quality products as possible and helps the users to understand the capabilities and
characteristics of verification tools.
This document introduces use cases for software safety and security verification tools and entity
relationship model related to them. This document also introduces tool categories for software safety
and security verification tools and gives category specific guidance and requirements for the tool
vendors and developers.
2 Normative references
There are no normative references in this document.
3 Terms and definitions
For the purposes of this document, the following terms and definitions apply.
ISO and IEC maintain terminological databases for use in standardization at the following addresses:
— ISO Online browsing platform: available at https:// www .iso .org/ obp
— IEC Electropedia: available at http:// www .electropedia .org/
3.1
application domain
well-defined set of applications
3.2
capability
quality of being able to perform a given activity
[SOURCE: ISO 19439:2006, 3.5]
3.3
certificate
attestation document issued by an independent third-party certification body
[SOURCE: ISO 22222:2005, 3.2]
3.4
defect
fault, or deviation from the intended level of performance of a system or software (3.19)
© ISO/IEC 2020 – All rights reserved 1

3.5
dynamic program analysis
process of evaluating a software (3.19) system or component based on its behaviour during execution
Note 1 to entry: The definition means that the software shall actually be compiled and run on a certain number of
input data test cases. The physical response from the system is then examined and compared to expected results.
Dynamic program analysis can be done manually or using an automated process. The results are examined either
manually (e.g. with small input test data) or automatically using oracles.
3.6
entity
data concept that may have attributes and relationships to other entities
[SOURCE: ISO/TR 25100:2012, 2.1.3, modified — Note 1 to entry has been removed.]
3.7
evaluator
competent person engaged in the verification (3.33) or validation (3.32) of a system or software (3.19)
3.8
false negative
true defect (3.4) that has not been observed
Note 1 to entry: The term is used for analysis tools producing defect information during the analysis of an
application. In the presence of false negatives, the tool is said to be incomplete with respect to the real set of
defects in the software (3.19) under analysis. False negatives can be due to several reasons such as 1) the use of
heuristics for detecting defects, 2) too restrictive analysis data.
3.9
false positive
observed defect (3.4) which does not correspond to a true defect
Note 1 to entry: The term is used for analysis tools producing defect information during the analysis of an
application. False positives appear during the analysis because of several possible reasons, such as lack of
precision of the analysis rules.
3.10
formal verification
activity proving or disproving the correctness of intended applications with respect to a formal
specification or a property, using formal methods of mathematics
3.11
malfunction
behaviour of a system or component that deviates from the specifications
3.12
protection
process to secure content
[SOURCE: ISO/IEC 15444-8:2007, 3.24]
3.13
risk
effect of uncertainty on objectives
Note 1 to entry: ISO 22538-4 defines risk as “probability of loss or injury from a hazard”.
[SOURCE: ISO 31000:2018, 3.1, modified — Notes 1, 2 and 3 to entry have been removed; a new Note 1
to entry has been added.]
3.14
safety
freedom from unacceptable risk (3.13)
2 © ISO/IEC 2020 – All rights reserved

3.15
safety-critical system
system whose failure or malfunction (3.11) may result in one (or more) of the following outcomes:
— death or serious injury to people
— loss or severe damage to equipment/property
— environmental harm
EXAMPLE Examples of safety-critical systems are critical infra-structures, medical equipment,
transportation, and nuclear power plants. Safety-critical systems are also sometimes called life-critical systems.
3.16
security
resistance to intentional, unauthorized act(s) designed to cause harm or damage to a system
3.17
security level
combination of a hierarchical security (3.16) classification and a security category that represents the
sensitivity of an object or the security clearance of an individual
Note 1 to entry: The minimum security level is an indication of the minimum protection (3.12) required.
3.18
semi-formal verification
method that is based on a description given in semi-formal notation
3.19
software
all or part of the programs, procedures, rules, and associated documentation of an information
processing system
[SOURCE: ISO/IEC 19770-3:2016, 3.1.26, modified — Note 1 to entry has been removed.]
3.20
software item
identifiable part of a software (3.19) product, consisting of source code, object code, control code,
control data, or a collection of these
Note 1 to entry: Software item is a generic term that designates well-identified parts of software source code,
object code or data. A software item belongs to a syntactic category of the programming language in which the
software is written. Examples are classes, variables, functions and types. A software item is an identifiable part
of a software product.
3.21
software safety
ability of software (3.19) to be free from unacceptable risk (3.13)
Note 1 to entry: It is the ability of software to resist failure and malfunctions (3.11) that can lead to death or
serious injury to people, loss or severe damage to property, or severe environmental harm.
Note 2 to entry: Software quality, including software safety, is achieved using software engineering. Software
engineering for safety-critical systems (3.15) emphasizes the following directions:
— process engineering and management;
— selecting the appropriate tools and environment for the system; the principle of using the best tools fit to the
purpose prevails as in most engineering disciplines;
— adherence to requirements.
© ISO/IEC 2020 – All rights reserved 3

3.22
software security
ability of software (3.19) to protect its assets from a malicious attacker
Note 1 to entry: According to software product quality model in ISO/IEC 25010, software security applies to
software assets and is decomposed into the following set of properties: confidentiality, integrity, availability,
authentication, authorization and non-repudiation.
3.23
software unit
smallest independent piece of software (3.19), which can be independently translated, and which can be
tested with the relevant data on whether it performs to specification
3.24
static program analysis
sub-field of formal methods concerned by analyzing the properties of a software (3.19) code without
executing this code in the target (binary) format
3.25
system safety
ability of a system to be free from unacceptable risk (3.13)
Note 1 to entry: A system is defined as a set or group of interacting, interrelated or interdependent elements
or parts, that are organized and integrated to form a collective unity or a unified whole, to achieve a common
objective. In a broader view the definition of a system consists in the hardware, software (3.19), human systems
integration, procedures and training. Therefore, system safety is part of the systems engineering process and
should systematically address all of these domains and areas in engineering and operations in a concerted
fashion to prevent, eliminate and control hazards.
Note 2 to entry: A system safety concept helps the system designer(s) to model, analyze, gain awareness about,
understand and eliminate the hazards, and apply controls to achieve an acceptable level of safety (3.14). The
systems-based approach to safety requires the application of scientific, technical and managerial skills to hazard
identification, hazard analysis, and elimination, control, or management of hazards throughout the life-cycle
of a system, program, project or an activity or a product. Hazop is one of several techniques available for the
identification of hazards.
3.26
target of verification
TOV
software (3.19), or a set of software items (3.20) or units (3.23), to be verified (e.g. in terms of safety
(3.14) and security (3.16))
Note 1 to entry: Target of evaluation (TOE) is a commonly used term in systems security techniques. TOE is
defined as a set of software, firmware and/or hardware possibly accompanied by guidance.
3.27
target software
final product of a software (3.19) development process, containing at least the binary code able to run
on the target computer
Note 1 to entry: Target software may consist of several files, including binary and source files, libraries,
installation and compilation script files, documentation and data files. The target software often relies on
underlying layers of software, that are not part of the target software, but that are necessary to be executed on
the target platform, for instance libraries.
3.28
target system
complete computing platform capable of running the target software (3.27)
Note 1 to entry: A target system consists of hardware resources and software (3.19) resources installed on the
hardware.
4 © ISO/IEC 2020 – All rights reserved

3.29
toolbox
set of tools completing each other in terms of capabilities, to cover a larger area of their intended use
3.30
trust
degree to which a user or other stakeholder has confidence that a product or system will behave as
intended
[SOURCE: ISO/IEC 25010:2011, 4.1.3.2]
3.31
use case
specification of a sequence of actions, including variants, that a system (or other entity (3.6)) can
perform, interacting with actors of the system
[SOURCE: ISO 15745-1:2003, 3.35, modified — The domain "" at the beginning and "[UML]" at
the end of the definition has been removed.]
3.32
validation
confirmation, through the provision of objective evidence, that the requirements for a specific intended
use or application have been fulfilled
EXAMPLE Safety (3.14) validation has been defined as an assurance, based on examination and tests, that
the safety goals are sufficient and have been achieved (ISO 26262-1).
[SOURCE: ISO/IEC 25000:2014, 4.41, modified — Note 1 to entry have been removed; EXAMPLE has
been added.]
3.33
verification
confirmation, through the provision of objective evidence, that specified requirements have been
fulfilled
[SOURCE: ISO/IEC 25000:2014, 4.43, modified — Note 1 to entry have been removed.]
3.34
verification method
method for producing objective evidence that specified requirements of a system have been fulfilled
3.35
verification tool
instrument that can be used during verification (3.33) to collect information about the target of
verification (3.26), to perform interpretation of information or to automate part of the verification
3.36
vulnerability
potential flaw or weakness in software (3.19) design or implementation that could be exercised
(accidentally triggered or intentionally exploited) and result in harm to the system
Note 1 to entry: The CVE classification (see Reference [25]) defines the de-facto standard classes of the known
software vulnerabilities.
Note 2 to entry: A vulnerability is exploitable if it can be activated in practice.
© ISO/IEC 2020 – All rights reserved 5

4 Abbreviated terms
AASPE automated assurance of security policy enforcement tool
ACSL ANSI/ISO C specification language
ARM advanced RISC machine
BDD binary decision diagram
BNF Backus–Naur form
CASE computer-aided software engineering tool
CC common criteria
CSPN Certification de Sécurité de Premier Niveau
CTL computation tree logic
dns domain name server, domain name system
DREAD damage, reproducibility, exploitability, affected users, and discoverability risk assess-
ment model
EAL evaluation assurance level
FMEA failure mode and effects analysis
HAZOP hazard and operability analysis
LTL linear temporal logic
OSINT open-source intelligence
RM reference manual
SAT satisfiability
SCL Safety Culture Ladder
SDLC software development life-cycle
SMT satisfiability modulo theory
SQL structured query language
STRIDE spoofing, tampering, repudiation, information disclosure, denial of service and elevation of
privilege
SWOT strengths, weaknesses, opportunities and threats
UML unified modeling language
VDM-SL Vienna development method - specification language
V&V verification and validation
XSS cross-site scripting
6 © ISO/IEC 2020 – All rights reserved

5 Models for software safety and security verification tools
The model for software safety and security verification is needed to define capabilities of and
requirements for tools by their input, processes and output. The model consists of the following
elements:
a) a set of use cases for concretizing the use of software safety and security verification tools,
b) a set of entities that represents identifiable information which appears in software safety and
security verification activities, and
c) a categorization for software safety and security verification tools.
Figure 1 — Overall structure of models of software safety and security verification
Software safety and security verification activities, including use of tools, are needed whenever any
person (or a thing) develops safety and/or security critical software. Any change to the software can
also require new verification activities (e.g. a whole new verification process). Other typical uses for
software safety and security verification tools are related to software quality evaluation and software
certification cases. The use of such tools may be part of system or application security verification
process, as defined in ISO/IEC 27034 (all parts).
As safety and security issues are becoming increasingly important within software intensive industry
and software intensive systems, a lot of new terms and concepts emerge more and more frequently.
Terms like cyber security, systems of systems, and Internet of Things were never heard of some years
ago, and today they are supposed to be recognized and understood by anyone using or developing
software and systems. Unfortunately, there is still a lot of space for loose communication and
misunderstanding. Commonly accepted and mutually understood terminology between the developers
and users of safety and security verification tools is needed. The most often needed terms and entities
are defined in Clause 3 and discussed in Clause 7.
Clause 6 introduces the use cases of software safety and security verification through some usage
scenarios. They describe the way how software developers or evaluators are intended to use verification
and validation tools to ensure that the end-product becomes of the adequate quality in terms of safety
and security. The target level of safety and security is often defined during the requirements stage of
each development case.
Both safety and security of software are equally essential. However, there are no single tools that can
manage both of such areas of requirements perfectly. That is why the users need to use several tools,
representing several tool categories, when they want to convince themselves and other stakeholders
to trust the overall safety and security of the target software. Clause 8 introduces the verification tool
categories, each specified by capabilities of the tools in the category, and specifies requirements for
software safety and security verification tools.
© ISO/IEC 2020 – All rights reserved 7

Software industry recognizes several different software development life-cycle (SDLC) models and
development approaches, known for example as V-shaped, linear, prototypical or agile. In safety and
security critical cases, the work often follows a standard SDLC where the activities of the development
process are represented and well-identified with the same names and same order. Software cannot be
tested before being programmed. Verification cannot be done and verification tools cannot be used if
there are no specified requirements. To highlight the verification opportunities during a standard SDLC,
Figure 2 introduces a case of V-shaped life-cycle for developing safety and security critical software.
Figure 2 — A simplified view of safety and security critical software development life-cycle
Each box in Figure 2 represents an activity and grey arrows represent the flow of artefacts between
the activities. For each activity the text in the box indicates some exemplary tools needed to perform
verification and/or validation tasks. The horizontal arrows in Figure 2 represent the links between
pairs of activities when V&V activities occur. For each V&V activity on the right side the arrows show
the correspondence to a development activity on the left side against which outcomes verification and
validation are performed. The related verification actions are actually performed immediately after
provision of development outcomes on the left side, before moving to the next development activity, and
the validation actions only after the implementation and preceding V&V activities. In more details, the
following correspondences occur:
— conformance of unitary V&V to the detailed specifications and to the design;
— conformance of software integration V&V to the specifications;
— conformance of system integration to the requirements and global specifications.
For each activity, Figure 2 indicates its main outcome (also sometimes called main artefact or by-
product) as a small black box. Different techniques, methods and tools can be used to provide
understandable form for artefacts (e.g. UML, ACSL).
8 © ISO/IEC 2020 – All rights reserved

6 Use cases of software safety and security verification tools
6.1 General
By definition the use cases specify a sequence of actions that a system can perform, when interacting
with its users (i.e. the actors of the system). In this document, the use cases are defined at a level where
the users interact with one or more software safety and security verification tools. Selection of the
tools to be used can be made following the processes of ISO/IEC 20741, which introduces the generic
process for evaluating and selecting any software engineering tools (see Annex B).
In this document the detailed variations for using specific tools are ignored because the purpose of
introducing use cases here is not to give specifications for building the tools but to help the readers to
understand the environment where the tools are used. For that purpose, the use cases are not presented
in any standard format, but rather as usage scenarios, although the term “use case” is still used.
Actors of software verification are as follows:
— Developers perform the development and verification tasks given in the life-cycle. They produce all
intermediate products to be verified. They also perform the validation of the intermediate products
and testing, sometimes together with the client.
— Evaluators are verifying and validating the software against some safety or security standard.
st
They are independent from the developers’ tasks, but may belong to the same (1 party) or an
independent third-party organization.
— Certification bodies examine the verification results already done, perform further verifications
if needed and deliver, if acceptable, a certificate to the software verified. Certification bodies are
always third-party organizations (ISO/IEC 17000).
Figure 3 introduces the overview of verification use cases and the actors related to them. Purpose of
the verification and the criticality of the TOV are the main differentiators of the use cases. The higher
the criticality of the TOV is in terms of safety and security, the more demanding the verification process
is, and the more expertise is required from the evaluator(s).
Figure 3 — Use cases of software safety and security verification tools
Formality of the verification varies by the criticality of the TOV. In some cases it is good enough to
run an informal or a semi-formal verification whereas in the most critical cases, a formal verification
is required. For the lowest criticality level, when the purpose of verification is not to achieve a
certificate, an independent evaluator is not needed at all. All verification use cases aiming to certify a
TOV shall specify the target safety and/or security level within an applicable standard (e.g. evaluation
assurance levels EAL1 to EAL7 of common criteria for information technology security evaluation in
© ISO/IEC 2020 – All rights reserved 9

ISO/IEC 15408 (all parts) or DO-178 B/C). The definitions of evaluation assurance levels of Common
Criteria are in Annex A.
6.2 to 6.4 introduce the lists of actions of the verification use cases.
6.2 Verification for low criticality software
For low-criticality software, requirements can be handled through informal methods and developers
often perform their own testing. If the goal of the verification is certification there are additional
actions for reaching a minimum level of safety and security. These additional actions are the optional
items e), f), g), h) and k) below.
The scenario may include the following actions:
a) informal specification and design;
b) implementation;
c) verification by testing;
d) integration;
e) selection of an evaluation and certification scheme capable of assessing low criticality software
(e.g. CSPN, SCL or CC) — third-party verification;
f) selection of the desired minimum certification level — third-party verification;
g) evaluation of the TOV to a defined level of safety or security — third-party verification;
h) certification by some certification body to obtain approval — third-party verification;
i) deployment/acceptance;
j) update/maintenance;
k) re-evaluation — third-party verification.
6.3 Verification for medium criticality software
Medium criticality developments do not need verification to their full extent, but a rigorous approach
with intermediate products (artefacts) is used. The intermediate products may use different languages,
which may require annual translations between activities. For each activity it is best to use only one
language. If the goal of the verification is certification there are additional steps for reaching a minimum
level of safety and security. These additional actions are the optional items c), k), m), n) and q) below.
The scenario may include the following actions:
a) qualification of tools (e.g. compilers);
b) requirements definition using preferably a semi-formal specification language;
c) selection of the certification level and definition of the TOV — third-party verification;
d) detailed specifications using preferably a formal specification language;
e) detailed design, using a semi-formal design language (e.g. UML);
f) implementation;
g) unit testing to give an intuitive understanding of the TOV made so far; the generation of the
corresponding test cases can use the specifications to delimit them; testing consists of e.g. in
coverage and boundary testing;
10 © ISO/IEC 2020 – All rights reserved

h) verification of the components of the TOV, to check the satisfiability of the specifications, e.g. using
the later as assertions;
i) integration of the components;
j) integration testing;
k) verification and validation of the integrated software — third-party verification;
l) system integration;
m) evaluation of the TOV to a defined level of safety or security — third-party verification;
n) certification to obtain approval — third-party verification;
o) deployment/acceptance;
p) update/maintenance;
q) re-evaluation — third-party verification.
6.4 Verification for high criticality software
Any software provider organization developing high criticality components (e.g. embedded software)
can be willing to verify the safety and security of their products first without certification and start the
official third-party evaluation later.
This use case deals with the production of high criticality software. The scenario may include the
following actions:
a) qualification of tools (e.g. compilers);
b) requirements definition using preferably a semi-formal specification language;
c) selection of the certification level and definition of the TOV — third-party verification;
d) detailed specifications using a formal specification language (e.g. VDM-SL, B, Z, or ACSL);
e) specifications refinement (optional) or formal design with a formal compliance check;
f) implementation;
g) unit testing to give an intuitive understanding of the TOV made so far;
h) completing unit testing by static program analysis — third-party verification;
i) verification of the components of the TOV, to extract low-level (e.g. run-time) faults and high-level
behavioural faults; the later checks the satisfiability of the specifications by the code; the formal
specifications produced above are used for compliance verification, using e.g. Hoare Logic and
formal proofs are done;
j) formal verification of the components — third-party verification;
k) integration of the components;
l) integration testing;
m) verification and validation of the integrated TOV;
n) system integration;
o) system testing on the target system;
p) evaluation of the TOV to a defined level of safety or security — third-party verification;
© ISO/IEC 2020 – All rights reserved 11

q) deployment/acceptance;
r) update/maintenance;
s) re-evaluation — third-party verification.
7 Entity relationship chart of software safety and security verification
It is important to use common and well-defined terms with software safety and security verification
tools, services, and methods, that might be evaluated, compared and selected by any third-party
representatives. The nature of and the relationships among the most important entities can be
understood in similar ways by all the actors of a verification activity.
The entities involved in the area of interest of this document are organized in the diagram in Figure 4.
Figure 4 — Entity relationship chart of software safety and security verification
The most important entities in the world of software safety and security verification tools are “software”,
“verification” and “verification tool”. In every instance of verification, the target of verification means
software, which consists of one or more software units and/or software items. The software may be
part of a system or several systems, but it is not relevant from the software verification point of view.
A person called evaluator is running the verification, where he or she uses one or more verification
tools. The tools are usually based on one or more verification methods (e.g. dynamic or static program
analysis or formal verification). Tools based on same methods often represent the same tool category,
having similar capabilities for identifying potential vulnerabilities of the software (i.e. TOV). Several
tools with different capabilities that mostly complete each other, may together constitute a toolbox.
Selection of an applicable toolbox or set of applicable tools can be made based on the known required
safety and/or security levels of the TOV.
The target of verification (software) may be certified by the evaluator representing a certification body,
if the verification proves the software free of vulnerabilities at the target safety and security levels.
The required expertise of the evaluator may be higher, if the purpose of verification is to achieve a
certificate.
12 © ISO/IEC 2020 – All rights reserved

8 Categories, capabilities of and requirements for software safety and security
verification tools
8.1 General
As software, by definition, consists of all or part of the programs, procedures, rules, and associated
documentation of an information processing system, it may be complicated to verify. Because of the
complexity of software, there are many kinds of verification tools. In this document the types of
software safety and security verification tools are divided into several categories, specified by the
capabilities of the tools included in the category. The capabilities enable the tools to analyze and
verify some software code or artefacts. Verification activities are human guided, but very often tool
assisted, and the level of automation varies category by category, and tool by tool within the category.
Verification capabilities allow performing various kinds of verification activities in various tasks of a
software development process. Figure 5 introduces the categories of software safety verification tools,
and Figure 6 the categories of software security verification tools.
8.2 Categories of software safe
...