Software certification with semantic analysis
Software certification with semantic analysis

The overall goal of the Celtique project is to improve the
security and reliability of software with semantics-based modeling,
analysis and certification techniques. To achieve this goal, the
project conducts work on improving semantic description and analysis
techniques, as well as work on using proof assistants (most notably
Coq) to develop and prove properties of these techniques. We are
applying such techniques to a variety of source languages, including
Java, C, and JavaScript. We also study how these techniques apply to
low-level languages, and how they can be combined with certified
compilation. The CompCert certified compiler and its intermediate
representations are used for much of our work on semantic modeling and
analysis of C and lower-level representations.

The semantic analyses extract approximate but sound
descriptions of software behaviour from which a proof of safety or
security can be constructed. The analyses of interest include
numerical data flow analysis, control flow analysis for higher-order
languages, alias and points-to analysis for heap structure
manipulation. In particular, we have designed several analyses for information
flow control, aimed at computing attacker knowledge and detecting
side channels.

We work with three application domains: Java software for small
devices (in particular smart cards and mobile telephones), embedded C
programs, and web applications.



Centre(s) inria
In partnership with
Université Rennes 1,École normale supérieure de Rennes


Team leader

Lemaile Gosselin

Team assistant