Title: Secure Information Flow and Pointer Confinement in a Java-like Language

Abstract:
We consider a sequential object-oriented language with pointers
and mutable state, private fields and class-based visibility, dynamic binding
and inheritance, recursive classes, casts and type tests, and recursive
methods. Programs are annotated with security levels, constrained by security
typing rules.  A noninterference theorem shows how the rules ensure
pointer confinement and secure information flow.

Joint work with David A. Naumann (Stevens Institute of Technology)