Formal Verification of Memory Properties

We are interested in the formal verification of memory properties 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 and the verification of cryptographic primitives written in SmartMIPS assembly (Montgomery multiplication, Montgomery exponentiation, BBS pseudorandom number generator). Besides the formalizations of separation logic in themselves, these experiments led us to develop potentially reusable formal tools such as an original verifier for separation logic triples (triples written in a fragment of separation logic with lists) or a small compiler preserving separation logic triples (a formalization of this article by Ando Saabas and Tarmo Uustalu). We also explore alternative approaches to verification of memory properties such as model-checking using the Spin model-checker.

Progress News

• 01/07/09: paper about the formal verification of an implementation of BBS pseudorandom number generator (implementation).
• 09/03/09: poster about the formal verification of an implementation of Montgomery exponentiation presented at the PPL 2009 workshop (verified program, separation logic triple).
• 11/12/08: SGoto in Coq. (HTML documentation: goto.html, sgoto.html, sgoto_hoare.html, sgoto_hoare_example.html, compile.html, and compile_example.html)
• 17/10/07: paper about the certification of a verifier for a fragment of separation logic to appear in Computer Software.
• 09/03/07: paper about the certification of a verifier for a fragment of separation logic presented at the PPL 2007 workshop.
• 09/01/07: Web interface to a certified verifier for a fragment of separation logic
• 08/12/06: paper about the formal verification of the Montgomery multiplication presented at ASIAN 2006
• 05/12/06: decision procedure for a fragment of separation logic (with loops and lists),
  presented at the The 2nd Franco-Japanese Computer Security Workshop
• 14/09/06: Seplog extension to SmartMIPS, presented at the JSSST 2006 workshop
• 13/09/06: a Spin model of Topsy, presented at the JSSST 2006 workshop
• 04/08/06: new specification of the allocation function (whose precondition forbids failure of the allocator)
• 17/07/06: paper about the formal verification of the heap manager to appear in ICFEM 2006
• 23/05/06: new simplification of the specifications and the verification of the heap manager
• 18/04/06: a Spin model of Topsy that enables verification of task isolation
• 08/02/06: simplification of the specifications and the verification of the heap manager
• 27/01/06: decision procedure for a fragment of separation logic (for straight-line code)
• 06/01/06: Coq development moved to online cvs
• 27/12/05: heap module extended with extensionality
• 09/12/05: technical document about the verification of the heap manager
• 12/10/05: specifications and the verification of the (pacthed) heap manager completed
• 08/08/05: page created

Technical Documents

1. Certifying Assembly with Formal Cryptographic Proofs: the Case of BBS (presented at the AVoCS 2009 workshop)
2. Overview poster (in Japanese) on formal verification of implementation of cryptographic primitives
3. A Certified Verifier for a Fragment of Separation Logic (Computer Software 25(3):135-147, revised version of the PPL 2007 paper)
4. A Certified Verifier for a Fragment of Separation Logic (presented at the PPL 2007 workshop)
5. Formal Verification of an implementation of the Montgomery multiplication (presented at the ASIAN 2006 conference, revised version of the JSSST 2006 paper)
6. Application of seplog to a subset of SmartMIPS (presented at the JSSST 2006 workshop)
7. Spin model of the Topsy operating system (presented at the JSSST 2006 workshop)
   
8. 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)
9. Verification of the heap manager of an operating system using separation logic (presented at the SPACE 2006 workshop, slides)
   
10. Overview paper (presented at the JSSST 2005, slides)

Implementation

1. Coq archives: last version, 31/08/06 (ASIAN 2006), 04/08/06 (ICFEM 2006), 10/01/06 (SPACE 2006)
2. Spin archive: 07/08/06 (JSSST 2006)

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