*********************************************************************
*                       Ecole Normale Supe'rieure                   *
*                                                                   *
*                              Se'minaire                           *
*                SEMANTIQUE ET INTERPRETATION ABSTRAITE             *
*                              P. Cousot                            *
*                                                                   *
*                        Vendredi, 14h00--15h30                     *
*                           Salle U/V, etage -2                     *
*                  DI  ENS  45 rue d'Ulm  75005 Paris               *
*********************************************************************

*** Vendredi 20 juin 2003 *******************************************

George Necula (University of Berkeley)

Extensible Code Verification

Re'sume': Widely-deployed virtual machines, such as the Java VM or
Microsoft's Common Language Infrastructure, feature code verification
algorithms that restrict drastically the format and the type system that can
be used by the foreign code to be verified. We propose instead that virtual
machines be designed with extensible verifiers, which allow the supplier of
the foreign code to also supply an appropriate untrusted verifier. This
scheme allows for maximum of flexibility in the choice of the type system
and compilation techniques that can be used for generating the foreign code.
The soundness of the verification process can be ensured by an architecture
in which the untrusted verifier is queried repeatedly about the semantics of
the foreign code by a resident trusted module. This trusted module also
checks the answers given by the untrusted verifier for soundness with
respect to a resident safety policy, such as memory safety. We show that
this architecture is sufficiently expressive to allow the untrusted verifier
to customize many software conventions, such as the stack discipline, the
calling convention, exception mechanisms and type systems.

 This work is done in collaboration with my graduate student Robert Schneck.

*********************************************************************
Pour recevoir l'annonce par courrier electronique: 
http://www.di.ens.fr/~cousot/annonceseminaire.shtml
*********************************************************************