Tenth and final Meeting
- Laurent Gottely
-
Title: Verification of security properties of Java libraries using
model-checking and abstract interpretation techniques
- Abstract:
The Java sandbox is implemented by using a reference monitor (the SecurityManager) who implements checks
methods. Those methods are used throughout the libraries to prevent an unauthorized use of critical
methods. The goal of my work is to prove that these checks fulfill their requirements.
I propose an abstraction of the virtual machine which makes it possible to analyse data and control flow
properties of program fragments. References are abstracted in function of the knowledge of their allocation
site, enabling a precise abstract equality.
This abstraction is used to generate an accesibility graph. Properties are expressed with security automata
and checked by doing a synchronous product with the accessibility graph.
Furthermore, I developped a front end which generates automatically the security automaton from a high
level description of the couple (check method,critic method).