AIST > RISEC > Projects > Formal Verification for Software Security

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