INRIA Campus de Beaulieu, 35042 Rennes, France
Tel: (+33 / 0) 2 99 84 74 78
Fax: (+33 / 0) 2 99 84 71 71
Program analysisStatic program analysis aims at determining properties of the behaviour of a program without actually executing it. Static analysis is founded on the theory of abstract interpretation for proving the correctness of analyses with respect to the semantics of a programming language. My work has among other things been concerned with
I have been working on security of various versions of embedded Java, including Java Card and Java for mobile telephones. Java security can be further enhanced by extending the static byte code verification to other properties. The SAWJACard project developed a tool for certifying Java Card applications according to NFC industry norms.
Software securityThe particular branch of information security called "language-based security" is concerned with the study of programming language features for ensuring the security of software. Programming languages such as Java offer a variety of language constructs for securing an application. Verifying that these constructs have been used properly to ensure a given security property is a challenge for program analysis,
I am interested in mixing static and dynamic program analysis for precise information flow control. Such hybrid analysis aims at computing a precise estimation of attacker knowledge, with application eg. to identification of web tracking scripts.
Software Fault Isolation is a technique for
executing untrusted code without jeopardizing the host
system's integrity, by placing the code in a sandbox that
limits its actions. Classical SFI relies on a code
verifier that checks that the sandboxing is done
correctly. This verifiercan be formalized as an abstract
It is also possible to do away with the a posteriori
verifier by integrating SFI in to a verified compiler such