Celtique is a joint project-team with INRIA, CNRS, University of Rennes 1 and École normale supérieure de Rennes. It is member of the INRIA Rennes - Bretagne Atlantique research center and of the IRISA UMR 6074 laboratory.
The Celtique project builds upon results from the Lande project that ended in 2008.
The goal of the Celtique project is to improve the security and reliability of software through software certificates that attest to the well-behavedness of a given software. We aim at providing certificates issued from semantic software analysis. The semantic analyses extract approximate but correct descriptions of software behaviour from which a proof of security can be constructed.
The analyses of relevance include numerical data flow analysis, control flow analysis for higher-order languages, alias and points-to analysis for heap structure manipulation and data race freedom of multi-threaded code.
Existing software certification procedures make extensive use of systematic test case generation. Semantic analysis can serve to improve these testing techniques by providing precise software models from which test suites for given test coverage criteria can be manufactured. Moreover, an emerging trend in mobile code security is to equip mobile code with proofs of well-behavedness that can then be checked by the code receiver before installation and execution. A prominent example of such proof-carrying code is the stack maps for Java byte code verification. We propose to push this technique much further by designing certifying analyses for Java byte code that can produce compact certificates of a variety of properties. Furthermore, we will develop efficient and verifiable checkers for these certificates, relying on proof assistants like Coq to develop provably correct checkers.