Formal Verification for Software Security
Overview and Background
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. We are mainly using the Coq proof-assistant for our experiments.
Research Contents
Formal Verification of the Source Code of Low-level Programs
With the dissemination of embedded systems, it has become important to provide strong security guarantees for low-level programs. According to international standards, the most reliable evaluation assurance method is formal verification. Unfortunately, given the current state of the art, it is still difficult to perform formal verification of the source code of large programs. Yet, low-level programs are characterized by detailed memory manipulations, for which the formalism of Separation Logic has been proposed by researchers. In this project, we develop an environment for formal verification based on Separation Logic, whose usefulness is demonstrated by realistic case studies (SmartMIPS implementations of a pseudorandom number generator and signed multi-precision arithmetic, including the binary extended GCD algorithm, as used in the implementation of cryptographic schemes, implementation of communication protocols). Additional information
Formalization of Information Theory and Error-correcting Codes
The properties of data transmission are described by the theory of information, whose most fundamental results are Shannon's theorems. These theorems have non-trivial proofs that are seldom detailed, even in the introductory litterature. This is an unfortunate situation because crucial results in computer security (e.g., unconditional security) relies on the theory of information. In this presentation, we report on the construction in the Coq proof-assistant of a library of formal definitions and lemmas for the theory of information. As a concrete evidence of its usefulness, we produce in particular the first formal proofs of Shannon's theorems about compression and coding. Additional information
Members
- AFFELDT Reynald
- SAKAGUCHI Kazuhiko
Selected Results
- Reynald Affeldt and Kazuhiko Sakaguchi. 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. online
- Reynald Affeldt, Manabu Hagiwara, Jonas Senizergues. Formalization of Shannon's Theorems. Journal of Automated Reasoning, 53(1):63-103, 2014. Springer. online
- Reynald Affeldt. On Construction of a Library of Formally Verified Low-level Arithmetic Functions. Innovations in Systems and Software Engineering, 9(2):59-77, 2013. NASA/Springer. online
- Reynald Affeldt, David Nowak, and Kiyoshi Yamada. Certifying Assembly with Formal Security Proofs: the Case of BBS. Science of Computer Programming, 77(10-11):1058-1074, 2012. Elsevier. online
Related Links
- Formal Proofs of Realistic Programs using Separation Logic (Database of Grants-in-Aid for Scientific Research)
- Model and Formal Verification of C for the Safe Implementation of Embedded Software (Database of Grants-in-Aid for Scientific Research)
- Formalization of Modern Coding Theory (Database of Grants-in-Aid for Scientific Research)