Formal Analysis of an Information Flow Type System for MicroJava
(conference version)

Martin Strecker



 
 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