Subject: Vers un vérifieur de byte-code Java certifié Jour: 02/10/98 (Vendredi 2 Octobre) CHANGEMENT DE LIEU et d'HEURE En raison des exposes de Martin Abadi et Isabelle Attali a l'ENS dont vous trouverez l'annonce plus bas, il a ete decide de modifier le lieu et l'heure du seminaire Coq-Cristal-Para qui se tiendra vendredi 2 octobre a 15h30 a l'endroit suivant : ********************************************************************* * Ecole Normale Supe'rieure * * Salle W, 4e`me e'tage, toits du DMI * * DMI ENS 45 rue d'Ulm 75005 Paris * ********************************************************************* http://pauillac.inria.fr/bin/calendar/Seminaires S E M I N A I R E ____ ____ ___ / _ _ / __ __ /_ _ / / | _ __ _ / / \ / \ ___ / / | / /_ / __| / ___ /___/ __| / | __| |___ |_/ |_/ |____ / / __/ |_ |_/ |_ / |_/ / |_/ / / Vendredi 2 Octobre, 15h30 ------------------- Pascal BRISSET ------------------- CNET FRANCE-TELECOM Lannion ============================================================ Vers un ve'rifieur de byte-code Java certifie' ============================================================ L'expose' pre'sentera la re'alisation a` l'aide de Coq d'un ve'rifieur de byte-code pour un petit sous-ensemble de la machine virtuelle Java (JVM) comprenant des exceptions simplifie'es et des sous-routines (mais pas encore d'objets ni d'appels de me'thodes): - Formalisation de la machine et des crite`res de se'curite'; - De'finition d'une abstraction finie et preuve de sa pertinence; - Preuve d'un algorithme de ve'rification portant sur l'abstraction; - Extraction d'une imple'mentation en Caml. Les difficulte's a` envisager pour e'tendre cette approche a` la JVM comple`te seront discute'es en conclusion. ********************************************************************* * Ecole Normale Supe'rieure * * * * Se'minaire * * SEMANTIQUE ET INTERPRETATION ABSTRAITE * * P. Cousot * * * * Vendredi, 14h00--15h30 * * Salle W, 4e`me e'tage, toits du DMI * * DMI ENS 45 rue d'Ulm 75005 Paris * ********************************************************************* *** Vendredi 2 octobre 1998 **** 11h00 ****************************** Protection in Programming-Language Translations Martin ABADI (Compaq) Re'sume' : We discuss abstractions for protection and the correctness of their implementations. Relying on the concept of full abstraction, we consider two examples: (1) the translation of Java classes to an intermediate bytecode language, and (2) in the setting of the pi calculus, the implementation of private channels in terms of cryptographic operations. *** Vendredi 2 octobre 1998 **** 14h00 ****************************** A Formal Semantics and an Interactive Environment for Java and Java Card Isabelle Attali (INRIA Sophia-Antipolis) Re'sume' : We present a formal semantics for the Java programming language. More specifically, we cover the so-called "dynamic semantics" of the language, i.e. the specification of the behavior of Java programs. We are using the Centaur system (developed in Gilles Kahn's team) which provides an interactive interpreter and environment based on Natural Semantics. A semantic definition of Java within this framework, besides a formal reference, would also provide a computer-aided environment to study and to visualize the semantics, with the ability to check the semantics of specific programs through interpretation. The capability to graphically visualize the object graph during execution helps to study, understand and optimize applications. A prototype has been developed for Java (presented at www.inria.fr/croap/java together with screen-dumps of Java objects at execution). We are starting to specify the Java Card framework.