Abstract |
This paper presents a type-based information flow analysis for
MicroJava, a substantial subset of sequential Java. The analysis is
given in the form of a type-and-effect system, which is required for
handling side-effecting expressions and dynamic method lookup. The
type system and a proof of noninterference are formalized in the
Isabelle proof assistant, extending a comprehensive existing model
of MicroJava.
Online Copy |
Available as Postscript
Also look at the technical report.
Isabelle Sources |
See here
BibTeX Entry |
@InProceedings{strecker03:_infoflow_type_confer, author = {Martin Strecker}, title = {Formal Analysis of an Information Flow Type System for {M}icro{J}ava}, booktitle = {???}, year = 2003, series = {???}, pages= {???}, note= {submitted for publication} }
Last modified: Sat Nov 11 20:34:39 CET 2006 |