Yannick Moy

Kyriakos Georgiou, Guillaume Cluzel, Paul Butcher et al.

This white paper demonstrates how the assurance, reliability, and security of an existing professional-grade, open-source embedded TCP/IP stack implementation written in the C programming language is significantly enhanced by adopting the SPARK technology. A multifaceted approach achieves this. Firstly, the TCP layer's C code is being replaced with formally verified SPARK, a subset of the Ada programming language supported by formal verification tools. Then the lower layers, still written in C and on which the TCP layer depends, are modeled using SPARK contracts and validated using symbolic execution with KLEE. Finally, formal contracts for the upper layers are defined to call the TCP layer. The work allowed the detection and correction of two bugs in the TCP layer. In an increasingly connected world, where Cyber Security is of paramount importance, the powerful approach detailed in this work can be applied to any existing critical C library to harden their reliability and security significantly.

Yannick Moy

The automation offered by modern program proof tools goes hand in hand with the capability to interact with the tool when the verification fails. The SPARK proof tool tries to help the user by providing the right information, so that the user can help the tool complete the proof. In this article, we present these mechanisms and how they work concretely on a simple running example.

Sylvain Dailler, Claude Marché, Yannick Moy

Among formal methods, the deductive verification approach allows establishing the strongest possible formal guarantees on critical software. The downside is the cost in terms of human effort required to design adequate formal specifications and to successfully discharge the required proof obligations. To popularize deductive verification in an industrial software development environment, it is essential to provide means to progressively transition from simple and automated approaches to deductive verification. The SPARK environment, for development of critical software written in Ada, goes towards this goal by providing automated tools for formally proving that some code fulfills the requirements expressed in Ada contracts. In a program verifier that makes use of automatic provers to discharge the proof obligations, a need for some additional user interaction with proof tasks shows up: either to help analyzing the reason of a proof failure or, ultimately, to discharge the verification conditions that are out-of-reach of state-of-the-art automatic provers. Adding interactive proof features in SPARK appears to be complicated by the fact that the proof toolchain makes use of the independent, intermediate verification tool Why3, which is generic enough to accept multiple front-ends for different input languages. This paper reports on our approach to extend Why3 with interactive proof features and also with a generic client-server infrastructure allowing integration of proof interaction into an external, front-end graphical user interface such as the one of SPARK.