Formalizing non-interference for a simple bytecode language in Coq
In: Formal aspects of computing, Jg. 20 (2008), Heft 3, S. 259-275
Online
academicJournal
- print, 1 p
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), Heft 3, S. 259-275 |
Veröffentlichung: | London: Springer, 2008 |
Medientyp: | academicJournal |
Umfang: | print, 1 p |
ISSN: | 0934-5043 (print) |
Schlagwort: |
|
Sonstiges: |
|