Formalizing non-interference for a simple bytecode language in Coq

In this paper, we describe the application of the interactive theorem prover Coq to the security analysis of bytecode as used in Java. We provide a generic specification and proof of non-interference for bytecode languages using the Coq module system. We illustrate the use of this formalization by a...

Full description

Saved in:
Bibliographic Details
Published in:Formal aspects of computing 2008-05, Vol.20 (3), p.259-275
Main Author: Kammüller, Florian
Format: Article
Language:English
Subjects:
Applied sciences
Computer Science
Computer science
control theory
systems
Exact sciences and technology
Math Applications in Computer Science
Miscellaneous
Original Article
Theoretical computing
Theory of Computation
Citations: Items that this one cites
Items that cite this one
Online Access:Get full text
Tags: Add Tag
No Tags, Be the first to tag this record!
Description
Summary:In this paper, we describe the application of the interactive theorem prover Coq to the security analysis of bytecode as used in Java. We provide a generic specification and proof of non-interference for bytecode languages using the Coq module system. We illustrate the use of this formalization by applying it to a small subset of Java bytecode. The emphasis of the paper is on modularity of a language formalization and its analysis in a machine proof.
ISSN:0934-5043
1433-299X
DOI:10.1007/s00165-007-0055-2