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.
Celtique is a joint project with the CNRS, the University of Rennes 1 and ENS Rennes.
Last activity report : 2016