Report 2004-1.
Ownership transfer and abstraction
by Anindya Banerjee and David A. Naumann
Abstract:
Ownership confinement expresses encapsulation in heap structures, in
support of modular reasoning about effects, representation
independence, and other properties. This paper studies heap encapsulation
from the perspective of substitutability for the class construct of
Java-like languages and a particular form of confinement is justified
by a representation independence result. A syntax-directed static analysis
is specified and proved sound for checking confinement in the presence of
ownership transfer.
Report 2004-2.
Constraint-based Secure Information Flow Inference for a Java-like
Language
by Qi Sun, David A. Naumann and Anindya Banerjee
Abstract:
We address the problem of checking programs written in a Java-like
language, to ensure that they satisfy information flow policies like
confidentiality and integrity in the presence of dynamic access
control mechanisms like stack inspection. Security policy is specified
using permission dependent security types. We present an inference
algorithm that infers such security types in a modular manner. For an
object-oriented language, this involves inference in the presence of
libraries, i.e., classes parameterized by security levels. Moreover we
show how modular inference is preserved in the presence of method
inheritance and override. We discuss a prototype implementation and
prove soundness of the algorithm.
Report 2004-3.
(PDF |
PS)
Information Flow Analysis in Logical Form
by Torben Amtoft and Anindya Banerjee
Abstract:
We specify an information flow analysis for a simple imperative
language, using a Hoare-like logic. The logic facilitates static checking
of a larger class of programs than can be checked by extant type-based
approaches in which a program is deemed insecure when it contains an
insecure subprogram. The logic is based on an abstract interpretation
of program traces that makes independence between program variables
explicit. Unlike other, more precise, approaches based on a Hoare-like
logic,
our approach does not require a theorem prover to generate
invariants. We demonstrate the modularity of our approach by showing
that a frame rule holds in our logic. Moreover, given an insecure but
terminating program, we show how strongest postconditions can be
employed to statically generate failure explanations.