By Collins
During their presentations, Stylianos (Stelios) Basagiannis and Simone Fulvio Rollini from Collins, on Formal Verification Techniques, both speakers defined the concept as mathematical reasoning to build system models at design time and verify the generated state space for property guarantees. In a System-of-Systems context, such as the one elaborated within the REWIRE project, with multiple engineering teams, the main purpose is to trace overarching requirements through different levels of module development, using various formal verification tools.
Within the REWIRE Framework Architecture, a series of tools is used to provide evidence from a requirements perspective, crucial for product certification, especially in domains where security and safety are tightly connected. More analytically, the framework utilizes tools such as Sail, Cover, Coq, NuXMV, CBMC, and VeriVal to provide guarantees at different levels, from hardware to software and attestation protocols.
In addition, as far as the Formal Verification Focus Areas are concerned, the two main technical topics refer to (a) modeling and verification of a leakage-resistant mode of operation for block ciphers and (b) modeling and verification of the specification of an attestation protocol. For the algorithm modeling, SMV and its extensions were used to characterize functional correctness through encoding/decoding correspondence and tag generation/verification correspondence. Moreover, the use of abstraction as a soundness-preserving technique aims to simplify models for verification, while maintaining the validity of proven properties. The LRBC2 mode of operation encoding in SMV involves functions like KDF, MEN, TGF, and a parametric block cipher. The reasoning behind the selection of SMV was its strong capability in handling fixed-width unsigned integers, which are relevant to these algorithms.
Furthermore, scalability is a significant issue for exhaustive verification using model checking due to the large search space. Verification is split into initialization and solving phases, with the size of the intermediate representation being a key difficulty. Different verification settings, including a simple XOR cipher and AES, were used to assess scalability, with abstraction techniques yielding better results for proving properties with a limited number of blocks.
On the verification of implementation, the approach used to verify the implementation against the specification used CBMC and considered properties of correspondence and integration. Similar to specification verification, different settings were used, including the original C implementation, one with a minimal XOR cipher, and one with an abstracted block cipher. CBMC’s ability to perform abstraction via interpreted functions was crucial. Additionally, contrasted SAT and SMT-based techniques in model checking, noting the trade-offs between encoding complexity and reasoning capabilities. SMT allows for more direct reasoning on data structures but can be more challenging for tools when combining theories.
Following the detailed presentation of the core concepts, an illustration was performed on how simplifications and abstractions were introduced in C code for verification, including uninterpreted functions and the use of XOR. Verification was performed by progressively constraining the input domain to assess scalability, and the results showed the lowest verification time with XOR abstraction, while the full AES implementation only yielded a proof in one case. On soundness and spurious counterexamples, the evidence shows that while abstraction is sound (valid properties in the abstracted model hold in the original), it can introduce spurious counterexamples that don’t reflect actual program behavior, something that differs from the specification verification in SMV using NuXMV2. Finally, on memory safety and undefined behaviors, tools like CBMC seem to enable the examination and detection of memory safety issues and undefined behaviors in the C implementation, while several issues, such as arithmetic overflows, were identified and reported to the development team for fixing or justification.
On modeling and verifying an attestation protocol with zero-knowledge capabilities, the implementation was performed with VeriVal. VeriVal was chosen for its closeness to semiformal protocol representations, understandable output, built-in security properties, and automatic translation to ProVerif and Coq. Several considerations for choosing a language for protocol verification include expressivity, soundness, completeness, and termination. The VeriVal framework showed the close mapping between VeriVal encoding and semiformal protocol specifications. The framework operates under the Dolev-Yao attacker model with a public channel and perfect cryptography. It offers passive and active attacker modes, with the possibility of introducing leakage and defining guarded messages.
At the end of the presentation, the speakers referred to the need for confidentiality analysis of the attestation protocol’s join phase against passive and active attackers under various scenarios of guarded and unguarded messages. The tool scaled well for both passive and active attackers, with mostly guarded messages, but faced limitations for the active attacker, given the higher level of freedom. Future steps on this aspect might consider the execution of an analysis of an extended protocol version for confidentiality and authenticity, also considering leakage scenarios.