********************************************************************* * Ecole Normale Supe'rieure * * * * Se'minaire * * SEMANTIQUE ET INTERPRETATION ABSTRAITE * * P. Cousot * * * * Vendredi, 14h00--15h30 * * Salle S15, etage -1 * * DI ENS 45 rue d'Ulm 75005 Paris * ********************************************************************* *** Vendredi 18 fevrier 2005 **** 15h30 (note unsual time) ****************** George Necula (Berkeley Univ. & visiting prof. ENS) The Open Verifier Framework for Building Foundational Verifiers Abstract: We present the Open Verifier architecture for verifying untrusted code using customized verifiers. This framework can be viewed as an instance of foundational proof-carrying code where an untrusted program can be checked using the verifier most natural for it instead of using a single generic type system. Our design of the Open Verifier places special emphasis on reducing the burden of expressing both type-based and Hoare-style verifiers. A new verifier is created by providing an untrusted executable extension module, which can incorporate directly pre-existing non-foundational verifiers based on data-flow analysis or type checking. We show how multiple extensions can cooperate for verifying programs that use foreign functions. The extensions control virtually all aspects of the verification by carrying on a dialogue with the Open Verifier using a language designed both to correspond closely to common verification actions and to carry simple adequacy proofs for those actions. We describe our experience implementing proof-carrying code, typed assembly language, and data-flow or abstract interpretation based verifiers in this unified setting. ********************************************************************* Pour recevoir l'annonce par courrier electronique: http://www.di.ens.fr/~cousot/annonceseminaire.shtml *********************************************************************