Formal Verification of Low-level Programs

We are interested in the formal verification of low-level software. For this purpose, we have developed in the Coq proof assistant formalizations of Separation logic (as presented in the survey by John C. Reynolds). We have applied these formalizations to several use-cases, including:

• the verification of the heap manager of the Topsy operating system (paper)
• the verification of arithmetic functions written in SmartMIPS assembly:
  • Montgomery multiplication (paper) and exponentiation
  • BBS pseudorandom number generator (Coq code and papers)
  • binary extended gcd (Coq code and papers)
• parsing of network packets written in C (Coq code and papers)

Besides the formalization of Separation logic in itself, these experiments led us to develop potentially formal tools such as an original verifier for Separation logic triples (triples written in a fragment of separation logic with lists, see this paper) or a small compiler preserving Separation logic triples (a formalization of this article by A. Saabas and T. Uustalu).

The compute Coq code and documentation is available online (most of it being (* seplog (c) AIST 2005-2013. R. Affeldt, N. Marti, et al. GNU GPLv3. *) (* seplog (c) AIST 2014-2018. R. Affeldt et al. GNU GPLv3. *)).

All Technical Documents ↵

1. An Intrinsic Encoding of a Subset of C and its Application to TLS Network Packet Processing (Journal of Formalized Reasoning, 7(1):63-104, 2014, revised version of the PLPV 2013 paper)
2. On Construction of a Library of Formally Verified Low-level Arithmetic Functions (Innovations in Systems and Software Engineering, 9(2):59-77, revised version of the SAC 2012 paper)
3. Towards Formal Verification of TLS Network Packet Processing Written in C (presented at the PLPV 2013 workshop)
4. On Construction of a Library of Formally Verified Low-level Arithmetic Functions (presented at the SAC 2012 symposium)
5. Manuscript about an instance of seplog to C (presented at the JSSST 2011 meeting).
6. Certifying Assembly with Formal Cryptographic Proofs: the Case of BBS (Science of Computer Programming, 77(10-11):1058-1074, revised version of the AVoCS 2009 paper)
7. Certifying Assembly with Formal Cryptographic Proofs: the Case of BBS (presented at the AVoCS 2009 workshop)
8. Overview poster (in Japanese) on formal verification of implementation of cryptographic primitives (e.g., Montgomery exponentiation, Separation logic triple)
9. SGoto in Coq (HTML documentation: goto.html, sgoto.html, sgoto_hoare.html, sgoto_hoare_example.html, compile.html, and compile_example.html)
10. A Certified Verifier for a Fragment of Separation Logic (Computer Software 25(3):135-147, revised version of the PPL 2007 paper)
11. Web interface to a certified verifier for a fragment of separation logic
12. A Certified Verifier for a Fragment of Separation Logic (presented at the PPL 2007 workshop)
13. Formal Verification of an implementation of the Montgomery multiplication (presented at the ASIAN 2006 conference, revised version of the JSSST 2006 manuscript)
14. Application of seplog to a subset of SmartMIPS (presented at the JSSST 2006 meeting)
15. Spin model of the Topsy operating system that enables verification of task isolation (presented at the JSSST 2006 workshop)
    
16. Formal Verification of the heap manager of an operating system using separation logic (presented at the ICFEM 2006 conference, revised version of the SPACE 2006 paper)
17. Verification of the heap manager of an operating system using separation logic (presented at the SPACE 2006 workshop, slides)
    
18. Overview paper (presented at the JSSST 2005 meeting, slides)

Implementation ↵

1. Coq code and documentation (2007-2015)
2. Older archives: ASIAN 2006 (31/08/06), ICFEM 2006 (04/08/06), SPACE 2006 (10/01/06), online cvs (started 06/01/06, not maintained anymore), Spin experiment at JSSST 2006 (07/08/06)

08/08/2005: page created

Contact information: reynald dot affeldt at aist dot go dot jp