Rapport Avancement Final Projet EVEREST INRIA Sophia-Antipolis Novembre 2006 Composition de l'équipe Gilles Barthe - DR INRIA Julien Charles - doctorant, allocation ministere Benjamin Grégoire - CR INRIA Marieke Huisman - CR INRIA Mariela Pavlova - doctorant, bourse INRIA Alejandro Tamalet - stagiaire via programme 'internships' Avancees principales * Jack: - development of plug-in for Coq, and interface to use Coq within Eclipse - continued work on framework for verification of programs at bytecode level (compiler JML2BML, plus verification condition generator for bytecode) - increased support for interactive verification; in particular with the native keyword that allows to link JML specification with the logic of the underlying theorem prover * high level security properties - annotation generation for high level security properties, and of preconditions to avoid exceptions and modifies clauses - formalisation of the annotation generation progress More detailed description: JACK: In 2003, the Everest team took over the development of Jack (Java Applet Correctness Kit, a tool for applet validation), initiated within the research laboratory of the smartcard manufacturer Gemplus (now Gemalto). The original motivation for Jack was to provide a developer-oriented environment to validate Java smartcard applications annotated with JML annotations; the main emphasis of the original release was in hiding the complexity of formal verification using automatic provers, and in enabling developers to use formal verification technology within a standard IDE, namely Eclipse. Since then, several features have been added to Jack: - A plug-in to prove proof obligations interactively using the Coq proof assistant, as well as an interface to use Coq within Eclipse. Together with the Coq plugin, we also developed several Coq tactics to solve or simplify some proof obligations automatically (and therewith increase their readability). A similar Coq plug-in has been developed for ESC/Java. - A plug-in to generate annotations from high-level security properties, and another plugin to generate annotations to prevent nullpointer and array-index-out-of-bound exceptions, and to generate modifies clauses. - A plug-in (JML2BML) to translate JML specifications into BML specifications (BML is the bytecode cousin of JML, developed by the team in 2004-2005), and another plug-in (BML-VcGen) to generate verification conditions from Java bytecode and its BML specification~\cite{BP06JSV}. - Support for a native keyword in JML, to enable connecting a JML specification with the logic of the underlying prover. This makes it easier to reason about complicated data structures~\cite{Charles:ftfjp06}. The Jack tool has been used in small to medium-scale experiments. The most conclusive application, carried out by the Everest team in collaboration with researchers from the POPS team at INRIA Futurs and researchers from Gemalto, used the verification tool at bytecode level to reduce the footprint of Java-to-native compilation schemes~\cite{DBLP:conf/cardis/CourbotPGV06}. * High level security properties The algorithm to generate annotations for high-level security properties has been implemented in Jack. We are currently formalising it, in order to prove its correctness. Given a property described by a finite state machine (FSM) and a Java application, we have defined how the FSM can be captured by appropriate JML set annotations. We have defined a ``monitoring semantics'', describing how the transitions in the FSM are triggered by method calls in the Java application. The FSM is extended in such a way that if it cannot make a transition, it will end up in a sink-state. For the Java application, we add an invariant that this sink-state should never be reached, and we prove that if the monitoring semantics does not reach the sink-state, this invariant will not be violated. Currently, we are proving that if the monitoring with the FSM will not find any errors, then runtime assertion checking will not find any assertion violations. A next step will be to propagate the annotations, and to show that eventually correctness of the annotations can be proven statically. We are discussing with Besancon if we can integrate our algorithm with their JML front-end for temporal formulae. Publications (format Bibtex), statut des logiciels. @MASTERSTHESIS{Cha05, AUTHOR = {J. Charles}, TITLE = {V\'erification d'un composant {Java}: Le v\'erificateur de bytecode}, SCHOOL = {Universit\'e de Nice}, YEAR = {2005}, PSURL = {http://www-sop.inria.fr/everest/personnel/Julien.Charles/papers/05-06-17-rapport.ps}, PDFURL = {http://www-sop.inria.fr/everest/personnel/Julien.Charles/papers/05-06-17-rapport.pdf}, TOPICS = {team} } @INPROCEEDINGS{HWS06, AUTHOR = {M. Huisman and P. Worah and K. Sunesen}, TITLE = {A temporal logic characterisation of observational determinism}, CROSSREF = {csfw06}, TOPICS = {team}, PDFURL = {ftp://ftp-sop.inria.fr/everest/personnel/Marieke.Huisman/obsequiv_char.pdf} } @INPROCEEDINGS{BP06JSV, AUTHOR = {L. Burdy and M. Pavlova}, TITLE = {Java Bytecode Specification and Verification}, BOOKTITLE = {proceedings of SAC'06}, YEAR = 2006, PUBLISHER = {ACM}, SERIES = {}, EDITOR = {L.M.~Liebrock}, TOPICS = {team}, PDFURL = {http://www-sop.inria.fr/everest/personnel/Mariela.Pavlova/bcSpecVerify.pdf} } @INPROCEEDINGS{DBLP:conf/cardis/CourbotPGV06, AUTHOR = {A. Courbot and M. Pavlova and G. Grimaud and J.J. Vandewalle}, TITLE = {A Low-Footprint {Java}-to-Native Compilation Scheme Using Formal Methods.}, BOOKTITLE = {proceedings of CARDIS}, YEAR = {2006}, PAGES = {329-344}, EE = {http://dx.doi.org/10.1007/11733447_24}, CROSSREF = {DBLP:conf/cardis/2006}, BIBSOURCE = {DBLP, http://dblp.uni-trier.de}, TOPICS = {team} } @INPROCEEDINGS{Charles:ftfjp06, AUTHOR = {J. Charles}, TITLE = {Adding Native Specifications to {JML}}, BOOKTITLE = {Proceedings of the ECOOP workshop on Formal Techniques for {Java}-like Programs (FTfJP'2006)}, PSURL = {http://www-sop.inria.fr/everest/personnel/Julien.Charles/papers/06-07-10-ftfjp06-paper.ps}, YEAR = 2006, TOPICS = {team} } @misc{BBCGHLPR06:FMCO, title = " {JACK:} a tool for validation of security and behaviour of Java applications", author = "G. Barthe and L. Burdy and J. Charles and B. Gr\'egoire and M. Huisman and J.-L. Lanet and M. Pavlova and A. Requet", booktitle = "FMCO", year = 2006, note = "Abstract for tutorial, longer version to appear" } @phdthesis{Pavlova:phd, title = {Bytecode Verification and its Applications}, author = {M. Pavlova}, YEAR = {2006}, SCHOOL = {Universit\'e de Nice Sophia-Antipolis}, TOPICS = {team} }