Formalizing non-interference for a simple bytecode language in Coq
In: Formal Aspects of Computing, Jg. 20 (2008-05-01), S. 259-275
Online
unknown
Zugriff:
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.
Titel: |
Formalizing non-interference for a simple bytecode language in Coq
|
---|---|
Autor/in / Beteiligte Person: | Kammüller, Florian |
Link: | |
Zeitschrift: | Formal Aspects of Computing, Jg. 20 (2008-05-01), S. 259-275 |
Veröffentlichung: | Association for Computing Machinery (ACM), 2008 |
Medientyp: | unknown |
ISSN: | 1433-299X (print) ; 0934-5043 (print) |
DOI: | 10.1007/s00165-007-0055-2 |
Schlagwort: |
|
Sonstiges: |
|