LJGS: Gradual Security Typing for (Lightweight) Java

by Luminous Fennell and Peter Thiemann

LJGS is a lightweight Java core calculus with a gradual security type system. The calculus guarantees secure information flow for sequential, class-based, typed object-oriented programming with mutable objects and virtual method calls. An LJGS program is composed of fragments that are checked either statically or dynamically. Statically checked fragments adhere to a security type system which guarantees that their execution is free from security errors. Dynamically checked fragments rely on run-time security labels to track information flows. Dynamic checking is more precise than static type checking but terminates the program when detecting an illegal flow and incurs a run-time overhead. The programmer marks the boundaries between static and dynamic checking with casts so that it is always clear whether a program fragment requires run-time checks.

LJGS requires security annotations on methods and fields while the types of local variables are inferred. A method annotation specifies a constrained polymorphic security signature. A field annotation either specifies a fixed static security level or it prescribes dynamic checking. Dynamically typed fields are checked flow-sensitively with the no-sensitive-upgrade (NSU) policy at run-time. The types of local variables in method bodies are analyzed flow-sensitively. The labels of dynamically typed local variables are tracked with a standard hybrid technique that relies on a static analysis of local write effects.

Implementation

We are currently working on an implementation of LJGS. It is based on the Soot compiler framework and aims to support the sequential subset of Java. Development of the implementation takes place in this github Repository:

Publication

Luminous Fennell, Peter Thiemann

LJGS: Gradual Security Types for Object-Oriented Languages

European Conference on Object-Oriented Programming 2016 (paper & talk)

(technical report)