A PCC Architecture based on Certified Abstract Interpretation

Frédéric Besson 1 Thomas Jensen 1 David Pichardie 1
1 Lande - Logiciel : ANalyse et DEveloppement
IRISA - Institut de Recherche en Informatique et Systèmes Aléatoires, Inria Rennes – Bretagne Atlantique
Abstract : 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.
Type de document :
Rapport
[Research Report] RR-5751, INRIA. 2005, pp.35
Liste complète des métadonnées

https://hal.inria.fr/inria-00070268
Contributeur : Rapport de Recherche Inria <>
Soumis le : vendredi 19 mai 2006 - 19:47:30
Dernière modification le : mercredi 16 mai 2018 - 11:23:03
Document(s) archivé(s) le : dimanche 4 avril 2010 - 20:47:24

Fichiers

Identifiants

  • HAL Id : inria-00070268, version 1

Citation

Frédéric Besson, Thomas Jensen, David Pichardie. A PCC Architecture based on Certified Abstract Interpretation. [Research Report] RR-5751, INRIA. 2005, pp.35. 〈inria-00070268〉

Partager

Métriques

Consultations de la notice

423

Téléchargements de fichiers

133