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.
Constraint-based Secure Information Flow Inference for a Java-like
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.
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.