CELTIQUE Research team

Software certification with semantic analysis

Team presentation

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. 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. We target two application domains: Java software for mobile devices (in particular mobile telephones) and embedded C programs.

Research themes

Program analysis by abstract ianterpretation Interactipon between static analysis and decision procedures Extracting software certifications from static analysis Formal proof of programs and certification of semantic analysis tools

International and industrial relations

Participation to the European project MOBIUS on mobile code security Coordinator of several ANR projects (RAVAJ, CAVERN, DECERT) concerned with the static analysis and testing of software Participation in an industrial project paid by the National Defense Agency aiming at building a security-enhanced Java virtual machine

Keywords: Semantics Static analysis Test Software certification

Research teams of the same theme :

Inria Headquarters and research centres

Direct links

Social