A PCC Architecture based on Certified Abstract Interpretation

Proof Carrying Code (PCC) is a technique for downloading mobile code on a host machine while ensuring that the code adheres to the host's security policy. We show how certified abstract interpretation can be used to build a PCC architecture where the code producer can produce program certificates automatically. Code consumers use proof checkers derived from certified analysers to check certificates. Proof checkers carry their own correctness proofs and accepting a new proof checker amounts to type checking the checker in Coq. The checking of certificates is accelerated by a technique for (post-)fixpoint compression. The PCC architecture has been evaluated experimentally on a byte code language for which we have designed an interval analysis that allows to generate certificates ascertaining that no array-out-of-bounds accesses will occur. \\ Le Proof Carrying Code (PCC) est une technique pour télécharger du code sur une machine hôte tout en assurant que ce code adhère à la polique de sécurité de cette machine. Nous montrons comment l'interprétation abstraite certifiée peut être utilisée pour construire une architecture PCC pour laquelle la production de certificat est automatique pour le producteur de code. Pour vérifier les certificats, les consommateurs de code utilisent les vérificateurs de preuves produits à partir d'analyseurs statiques certifiés. Les vérificateurs de preuves sont eux-mêmes accompagnés de leur preuve de correction et accepter un nouveau vérificateur se ramène à vérifier son bon typage Coq. La vérification de certificats est accélérée par une technique de compression de (post-)points fixes. L'architecture PCC a été évaluée expérimentalement sur un langage àbytecode pour lequel nous avons conçu une analyse d'intervalles qui génère des certificats que assurent l'absence d'accès hors des bornes des tableaux