********************************************************************* * Ecole Normale Supe'rieure * * * * Se'minaire * * SEMANTIQUE ET INTERPRETATION ABSTRAITE * * P. Cousot * * * * Vendredi, 14h00--15h30 * * Salle R, etage -1 * * DI ENS 45 rue d'Ulm 75005 Paris * ********************************************************************* *** Vendredi 7 juin 2002 **** 14h00 ********************************* Renaud PACALET (ENST) Verification des systèmes sur puce (SoC - Systems on Chip) Re'sume': L'évolution des technologies de fabrication des semi-conducteurs permet aujourd'hui la réalisation de circuits intégrés d'une forte complexité. En quelques années ces dispositifs matériels sont passés du statut d'opérateur (transformée en cosinus discret) à celui de fonction (décodeur vidéo MPEG2 pour la télévision numérique) puis à celui de système (circuit unique pour la téléphonie de 3ème génération). Les outils et les méthodes utilisés par l'industrie du semi-conducteur ont également évolué, ainsi que la puissance des calculateur mais dans des proportions très inférieures. Les architectes de SoC doivent donc aujourd'hui concevoir des machines où coexistent des éléments de traitement analogique du signal, des unités de calcul numérique dédiées, des systèmes d'exploitation temps-réel, des applications logicielles, des micro-contrôleurs et des DSP. Il est devenu vital de concevoir des systèmes très complexes avec des outils aux performances insuffisantes Sous l'angle économique la situation est également tendue par deux phénomènes contraires. Tout d'abord, le coût d'entrée en fabrication - c'est à dire le prix qu'il faut payer pour obtenir un premier échantillon de circuit intégré - a, lui aussi, évolué pour atteindre des sommes comprises entre 500 000 et 1 000 000 d'euros. Il est donc devenu économiquement critique de ne lancer la fabrication qu'avec une grande confiance dans la qualité du produit conçu. A la différence des produits logiciels, les produits matériels ne sont en effet pas modifiables après fabrication. Un circuit intégré non fonctionnel est un grave handicap économique pour qui a financé sa réalisation. Un circuit non fonctionnel mais commercialisé est en général une catastrophe. Il est devenu vital de concevoir des systèmes très complexes de façon très sûre avec des outils aux performances insuffisantes. Le second phénomène économique important est le raccourcissement du temps de saturation des marchés de masse dans le secteur des technologies de pointe. La téléphonie mobile en est un exemple frappant qui est passée du statut de marché de produits haut de gamme à celui de marché saturé en phase de renouvellement quasi-statique en moins d'une décennie. La conséquence d'une telle tendance est le raccourcissement des cycles de conception. Lorsqu'un segment de marché apparait les acteurs économiques se mobilisent et proposent des solutions dans les délais les plus brefs. Les retardataires sont lourdement pénalisés et peinent à rentabiliser leurs investissements. Il est devenu vital de concevoir des systèmes très complexes de façon très sûre avec des outils aux performances insuffisantes dans un temps très court. L'exposé tentera de définir le concept de "System on Chip", présentera le cycle de conception de tels dispositifs et mettra l'accent sur les problèmes de validation rencontrés à chaque étape du cycle. *** Vendredi 14 juin 2001 **** 14h00 ******************************** Relâche. *** Vendredi 21 juin 2001 **** 14h00 ******************************** Bruno BLANCHET (ENS-CNRS) From Secrecy to Authenticity in Security Protocols Re'sume': We present a new technique for verifying authenticity in cryptographic protocols. This technique is fully automatic, it can handle an unbounded number of sessions of the protocol, and it is efficient in practice. It significantly extends a previous technique for the verification of secrecy. The protocol is represented in an extension of the pi calculus with fairly arbitrary cryptographic primitives. This protocol representation includes the authentication specification to be verified, but no other annotation. This representation is then translated into an abstract representation by Horn clauses, that can be used to prove the authentication specification. Our technique has been proved correct, and implemented. We have tested it on various protocols from the literature. The experimental results show that these protocols can be verified by our technique in less than 1 s. *** Vendredi 28 juin 2001 **** 14h00 ******************************** Isabella MASTROENI (U. Verona, visitant l'E'cole polytechnique) Handling the puzzle of semantics. Re'sume': In this work we apply abstract domain operations to systematically compare semantics. In 1997, Cousot introduced a hierarchy where semantics are related with each other by abstract interpretation. In this field we consider the standard abstract domain transformers, devoted to refine abstract domains in order to include attribute independent and relational information, respectively the reduced product and power of abstract domains, as domain operations to systematically design and compare semantics by abstract interpretation. We first prove that natural semantics can be decomposed in terms of complementary attribute independent observables, leading to an algebraic characterization of the symmetric structure of the hierarchy. Moreover, we prove that a specular hierarchy of non-standard semantics modeling transfinite computations of programs can be specified in such a way that the standard hierarchy can be derived by abstract interpretation. We prove that non-standard transfinite denotational and predicate transformer semantics can be both systematically derived as solutions of simple abstract domain equations involving the basic operation of reduced power of abstract domains. This allows us to prove the optimality of these semantics, i.e. they are the most abstract semantics in the hierarchy which are compositional and observe respectively the terminating and initial states of transfinite computations, providing an adequate mathematical model for program manipulation. ********************************************************************* Pour recevoir l'annonce par courrier electronique: cousot@di.ens.fr WWW: http://www.di.ens.fr/~cousot/annonceseminaire.shtml *********************************************************************