A certified lightweight non-interference Java bytecode verifier - Inria - Institut national de recherche en sciences et technologies du numérique Accéder directement au contenu
Article Dans Une Revue Mathematical Structures in Computer Science Année : 2013

A certified lightweight non-interference Java bytecode verifier

Tamara Rezk
  • Fonction : Auteur
  • PersonId : 949476

Résumé

Non-interference guarantees the absence of illicit information flow throughout program execution. It can be enforced by appropriate information flow type systems. Much of the previous work on type systems for non-interference has focused on calculi or high-level programming languages, and existing type systems for low-level languages typically omit objects, exceptions and method calls. We define an information flow type system for a sequential JVM-like language that includes all these programming features, and we prove, in the Coq proof assistant, that it guarantees non-interference. An additional benefit of the formalisation is that we have extracted from our proof a certified lightweight bytecode verifier for information flow. Our work provides, to the best of our knowledge, the first sound and certified information flow type system for such an expressive fragment of the JVM.
Fichier principal
Vignette du fichier
barthe_pichardie_rezk_2010_v2.pdf (517.42 Ko) Télécharger le fichier
Origine : Fichiers produits par l'(les) auteur(s)
Loading...

Dates et versions

hal-00915189 , version 1 (07-12-2013)

Identifiants

Citer

Gilles Barthe, David Pichardie, Tamara Rezk. A certified lightweight non-interference Java bytecode verifier. Mathematical Structures in Computer Science, 2013, 23 (5), pp.1032-1081. ⟨10.1017/S0960129512000850⟩. ⟨hal-00915189⟩
546 Consultations
327 Téléchargements

Altmetric

Partager

Gmail Facebook X LinkedIn More