![[HTTP Mutual Access Authentication]](/files/special/MutualAuth/index-en/mutual.png)
![[Fail-Safe C]](/files/project/FailSafeC-ja/FSC-logo.png){kind=logo}
![[Physical Analysis Attack on Cryptographic Module]](/special/SASEBO/SASEBO_banner_en.png)
![[LR-AKE]](/files/project/LRAKE-en/renew8.gif)
Formal Verification for Software Security
The most trustful kind of validation for security is formal verification. In essence, formal verification is about producing machine-checkable proofs of mathematical statements. Actually, security specifications are no more than mathematical statements about pieces of software, and our work is precisely to study means to write and prove formally security specifications. Among others, we have been working on formal languages for specification, their application to formal verification of software and cryptographic protocols.
Members
- Reynald Affeldt
- David Nowak
- Miki Tanaka
- Kiyoshi Yamada
Selected Results
- Reynald Affeldt, David Nowak, and Kiyoshi Yamada. Certifying Assembly with Formal Cryptographic Proofs: the Case of BBS. AVoCS 2009. Article. Abstract in Japanese.
- Reynald Affeldt and Hubert Comon-Lundh. Verification of Security Protocols with a Bounded Number of Sessions based on Resolution for Rigid Variables. Formal to Practical Security, LNCS 5458, May 2009. (c)Springer. Springer online. Preprint.
- Nicolas Marti and Reynald Affeldt. A Certified Verifier for a Fragment of Separation Logic. Computer Software, 25(3):135-147, July 2008. Preprint.
- Reynald Affeldt, Miki Tanaka, and Nicolas Marti. Formal Proof of Provable Security by Game-playing in a Proof Assistant. Provsec 2007, LNCS 4784. (c)Springer. Springer online. Preprint. Abstract in Japanese.
- David Nowak. A Framework for Game-Based Security Proofs. ICICS 2007, LNCS 4861. Cryptology ePrint Archive: Report 2007/199.
- Stephane Demri and David Nowak. Reasoning about transfinite sequences. International Journal of Foundations of Computer Science, 18(1):87-112, February 2007. Preprint
- Stephane Demri, Ranko Lazic, and David Nowak. On the freeze quantifier in Constraint LTL: decidability and complexity. Information and Computation, 205(1):2-24, January 2007. Preprint
- Reynald Affeldt and Nicolas Marti. An approach to formal verification of arithmetic functions in assembly. ASIAN 2006, LNCS 4435. (c)Springer. Springer online. Preprint.
- Slawomir Lasota, David Nowak, and Yu Zhang. On completeness of logical relations for monadic types. ASIAN 2006, LNCS 4435.
- Nicolas Marti, Reynald Affeldt, and Akinori Yonezawa. Formal verification of the heap manager of an operating system using separation logic. ICFEM 2006. LNCS 4260. (c) Springer. Springer online. Preprint
- Reynald Affeldt and David Nowak. Application of formal verification to software security. ISSS 2006. Slides and examples
- Reynald Affeldt and Nicolas Marti. Seplog: a Coq implementation of separation logic and its application to verification of low-level programs.
More results are available on members homepages.