Runtime verification of security properties with E-ACSL

Julien Signoles - CEA LIST, Software Security and Reliability Lab

Frama-C is a framework for code analysis of C code, including many analyzers. This talk presents E-ACSL, its runtime verification tool, and its applications to verification of security properties. E-ACSL automatically converts a C code annotated with formal specifications to another C code that checks them at runtime. Several usages of E-ACSL rely on automatic generation of these specifications, so that writing them by hand is not necessary. The verification process is therefore fully automatic. In this talk, we will focus on such automatic usages for verification of security properties, including verification of memory safety and information flow properties.

Download this presentation

About Julien Signoles

Julien Signoles is an expert researcher-engineer at CEA LIST’s Software Security and Reliability Lab (LSL) in France since 2007. He is one of the main developers of Frama-C, a code analysis framework for C code, and the author of E-ACSL, its runtime verification plug-in. His research interests focus on runtime assertion checking and applications of program analysis techniques to source code security. He got a PhD in Computer Science from University Paris 11 (France) in 2006.