Modular Semi-Automated Formal Verification of Security-Critical Software

In our increasingly computer-oriented society, the computer programs we rely on tend to increase in size and complexity. Since we almost have no choice but to trust these programs with our secrets and privacy, managing the quality of software has become ever more important. Countless techniques have been developed to demonstrate the correctness of security-critical software and this thesis extends on one of those: i.e. formal verification.

In the first part of this thesis we present an approach to verify different pieces of an application separately. This modular approach was dubbed symbolic linking and it significantly reduces the complexity of verifying large pieces of software. If an annotation-based verifier for C source code supports both symbolic linking and preprocessing, care must be taken to ensure soundness. The problem is that the result of a header expansion depends upon the macros defined. We propose a preprocessing technique which ensures soundness by construction and show that the resulting semantics after type checking are equivalent to those of standard C. We implemented this preprocessing technique in VeriFast, an annotation-based verifier for C source code that supports symbolic linking, and initial experiments indicate that the modified preprocessor allows most common use cases. To the extent of our knowledge, we are the first to support both modular and sound verification of annotated C source code.

In the second part of this thesis we focus on security-critical software that employs cryptographic operations to establish certain security goals. More precisely, we developed the extended symbolic model as an approach to verify cryptographic protocol implementations written against existing cryptographic APIs for C. We encoded this model in VeriFast and the encoding supports specifying and verifying integrity and confidentiality properties of protocol implementations that use hashing, the generation of random values, (authenticated) symmetric and asymmetric encryption. As a theoretical underpinning for this encoding, we devised a simple programming language and sound proof system that capture most interesting aspects of the encoding and have all necessary features to state and prove integrity properties of protocols.