S3 Formal Verification Solution — Workflows (3/4)

Layering¶

A number of good practices shall drive the formalization of the safety specification. It is usually desirable to interpose an insulation layer between the model of the system and the safety specification, renaming inputs, outputs, and internal variables in order to protect the safety specification from potential modifications in the naming convention of the system itself. HLL namespaces are a useful way of supporting such an insulation. Integration of the safety specification and the system is obtained by using these renamed system variables in the safety specification. As far as possible, higher level concepts describing the system or its environment shall be captured in an intermediate layer of helper definitions to maximize both clarity and reuse (e.g. plane is landing, train is approaching a signal, washing machine is in spin cycle,… ).

Structural-Level Specification¶

Different “levels” of safety specifications exist. At the lowest level, loosely related to safety, this specification can be automatically generated based on the code structure and semantics. Such a specification allows to perform analyses ensuring the absence of undefined behaviors in the code (e.g. division by zero, out of bounds array access, use of uninitialized variable,… ) or detecting dead or otherwise unreachable code.

Requirement-Level Specification¶

At an intermediate level, the safety specification can be derived from some level of system functional specification (i.e. requirements) to show that the code conforms to this functional specification. The closer the functional specification and the code, the simpler it will be to express and prove the properties. The model of the environment needed to perform the proof will also be simplified, or, most often, unnecessary. The same applies to lemmas needed to achieve the proofs. All in all, the development of the safety specification is thus rather simple.

However, such a safety specification can “only” be used to check that the code respects its functional specification. It does not give any insight on the correctness of this functional specification, nor on its ability to ensure the overall safety or mission of the system. Another drawback is that, when the functional specification is very close to the code, the expression of the properties may become very similar to that of the code, and the proof becomes a mere verification of the equivalence of two diversified developments. Pushed to the limit, this may become a complete validation strategy based on proving the equivalence of two diversified implementations (see third alternative of the figure about development processes), one of which could be expressed using HLL.

When based on the specification of a system, the properties usually contain references to some of the code internal variables in their expressions. The system is considered as a white-box in which the developer of the safety specification can look. Here it is important that every internal variable used in some properties to characterize the way another variable or output shall be computed is itself characterized by other properties. This shall be applied iteratively to express an uninterrupted chain of characterizations, linking the inputs of the system to its outputs.

Safety-Level Specification¶

When applicable, better results are usually achieved by taking a safety-related point of view to the design of the safety specification. Performing a hazard analysis of the system enables to identify the safety hazards leading to an accident. Refining these safety hazards enables to develop a set of safety properties which, when achieved by the system, ensures its safety. Being obtained using a method different from that used to develop the system, such properties are able to find problems in the code, but also potential flaws in the specification preventing it from ensuring the safety of the system. Once the code has been proved to respect such a safety specification, it may be used as a convincing argument in the demonstration of the overall safety of the system.

Depending on the level of refinement of the safety hazards, several levels of safety properties may be expressed. As a general rule, the closer to the safety hazards, the easier the modeling of the safety properties, and the more convincing that they imply the overall safety of the system. However, using high-level properties also complexifies the environment model, and makes these safety properties harder to prove.

Contrarily to the specification based approach, here, the system is considered as a black-box for the safety specification, and the safety properties are expressed using primarily the inputs and outputs of the system. No chain of characterization is needed. Still, the lemmas may have access to the internal variables of the code. However, that does not breach the reasoning because lemmas are always proved before being used: they are not part of the safety specification, just a helper for the model checker.

This approach may also be applied to address the analysis of the security of a system, and to a lesser extent its ability to achieve its missions in the general sense.

Trustworthiness and Certification¶

Finally, for systems developed in a normative environment or for which trustworthiness of the safety verification is required (see preliminary post), the assessment of the correctness and completeness of the safety specification is usually achieved by reviews performed by an independent team. In this sense, having a clear, simple, and readable safety specification, which unambiguously implies the safety of the system at the highest possible level, is clearly a plus. A drawback lies in the complexity of the environment model whose constraints have to be thoroughly checked for soundness, correctness, and completeness. In particular, it shall be verified that this modeling does not over-constrain the input scenarios (i.e. the constraints are fulfilled by the real environment). However, this is usually a simpler task than checking completeness of a low-level safety specification.

Protecting the Analyses¶

The first identified weakness is of course that of the model checker incorrectly reporting some property to be proved. This can arise if S3 reports as proved a property that it did not prove, or for which it derived an incorrect proof, or if it reasoned about a system different from the one contained in the given LLL file (e.g. because of a bug in its parser). Ensuring the correctness of a complete model checker using a standard mix of peer-reviews and tests is a very difficult task. A more pragmatic approach is to use an a posteriori technique called proof logging/proof checking. In this technique, S3 is enhanced with the capability, when it finds the proof of a property, to log this proof in a file which, starting from a reformulation of the analyzed LLL file, derives the proof as a deduction tree in a formally specified resolution-based proof system. After the S3 run, a specialized tool, the proof-checker checks that the reformulation corresponds to the LLL file given to S3, that the proofs are made of correct deductions, and that all properties have been proved.

In SAT-based model checking, finding a proof is a complex task relying on error-prone algorithms, optimizations, and heuristics. However, checking a proof is fairly simple and can be done with a high degree of confidence.

The following figure shows a synoptic view of the proof logging/proof checking mechanism. It is used for every run of the model checker (except when used in the uncertified workflow).

Protecting the Analyses

Protecting the Translation Workflow¶

The next identified weakness is in the translation of the system design to HLL. An error in this translation could easily lead to an erroneous proof because the properties are analyzed on an incorrect model. The following figure gives a synoptic view of the solution used to protect against this weakness.

Protecting the Translation Workflow

The translation is protected using diversification. The translation is done twice, by diversified tools, developed by independent teams, using different programming languages and paradigms. Here, to increase confidence, the sources are also diversified by considering, on the one hand the translation of the system design, and on the other the translation of the system code. The obtained HLL models are then both expanded to LLL. The expansion is a complex model transformation in which an error could also lead to an incorrect model (i.e. when the semantics is not preserved between the HLL and the LLL models), and thus to an erroneous proof. To protect this transformation, the expansion is also diversified using two independent expanders. For each model transformation (i.e. translations and expansion), a precise Logical Foundation Document, describing the syntax and semantics of the involved languages together with the transformation principles, is used to specify this transformation, prove its correctness and soundness, and develop test suites. This document is extensively reviewed by an independent expert team.

A second technique, called sequential equivalence checking, is used to compare the resulting LLL models. A tool, the equivalence-constructor takes the pair of LLL models and creates a third one, that encodes, as an LLL problem, the fact that the two models, fed with the same input sequences, produce the same outputs. The resulting equivalence LLL file is given to the S3 model checker to prove, using induction, that the equivalence holds. When it is the case, confidence is gained that the various model transformations (i.e. translations and expansions) have been correctly performed. There is indeed very little chance that a bug in one translator or expander is “matched” by another bug in the other tool-chain.

To make the equivalence system inductive and simplify the model checker task, an additional tool is needed. The mapper attempts to create a list as complete as possible of mapping points between the design and the code, i.e. variables or expressions that correspond in the two models. After having proved that they are indeed equivalent, these points are used to help prove the equivalence of the overall models. These pairs of mapping points are thus used in a way similar to lemmas for safety properties. As the potential equivalences output by the mapper are going to be proved by the model checker before being used, this tool does not need to be protected. It can take any source to perform its work, in particular the models themselves, and any traceability information produced by the code generator.

Finally, sometimes an analysis of the produced LLL model of the code is also necessary to ensure some aspects of the correctness of the code modeling and translation. Some languages do not have a fully defined semantics and the modeling adds automatic POs to the resulting model to verify that none of these undefined behaviors (such as accessing an uninitialized variable, reading outside an array,… ) are triggered by the code. The modeling is thus considered correct, with respect to these undefined behaviors, if and only if these POs hold.

Incidentally, the proof that the code is equivalent to the design is an interesting result in itself. First, it shows that the code generator, or compiler, has produced a correct code 2, and thus enables to remove the verification activities usually performed to assess this correctness. Secondly, it shows that the safety properties that have been shown to hold on the design also hold on the code.

Protecting the Safety Verification Workflow¶

The last identified weakness is in the expansion of the overall system composed of the safety specification and the system model. The expansion of this element corresponds to the connection of the two parts through named variables, and the model transformation to LLL. Once again, an error in this transformation can lead to an incorrect model and thus an incorrect proof. As previously, this transformation is protected (see following figure) by expanding the system twice with independent expanders, and proving that the obtained pair LLL of models are equivalent. Finally one of the models is analyzed to prove that the safety specification holds on the system design.

Protecting the Safety Verification Workflow

Overall Workflow¶

The overall solution synoptic, assembling the different protection mechanisms described previously, is presented in the following figure. It can be completed with a number of CRC to insure that the files input and produced by the solution are not degraded during the various transformations and analyses.

This workflow aims at automating the verification process and eliminating as much as possible the repetitive, time-consuming, expensive, incomplete, and error-prone human verification activities usually devoted to this task.

Complete S3 Solution Synoptic

The expanders, equivalence-constructor, and the S3 model checker are generic tools proven in use on industrial-size systems. Some generic translators for design and coding languages also exists, for sHLL (see section Modeling Languages), Scade©, C, and Ada. For other domain or customer specific languages, custom translators are developed. These translators produce a bit-precise, exact HLL model of the system. The various tools of the S3 toolset have been developed using a process involving a complete set of specification, design, and validation documentation, together with the necessary quality and verification activities. This process, associated to the described protection mechanisms enables an formal S3 verification solution to be used as a “verification tool”.