SecJ: a Modular Secure Information Flow Inferencer for Object-Oriented Programs

What is SecJ?

It is a compiler that checks programs written in a Java-like language to ensure that they satisfy the information flow policies, confidentiality and integrity. Information flow labels are inferred. The inference is inter-procedural and modular: incremental inference can be performed on individual program components, and the result used as libraries for other components. The constraint-based inference algorithm uses access control (stack inspection) information to improve the precision of the inference.

Who is involved?

Qi Sun designed and implemented the system as part of his PhD dissertation supervised by Anindya Banerjee and Dave Naumann. Chunyu Tang is now assisting with development.

Where can I get SecJ?

The download contains installation instructions. The distribution is licensed under the LGPL.

Learn more:

The PhD dissertation of Qi Sun discusses the problem, documents the tool, formally proves soundness of the inference algorithm, and much more.

There is also a research paper: Modular and constraint-based information flow inference for an object-oriented language, by Qi Sun, Anindya Banerjee, and David Naumann, which appeared in the 11th International Static Analysis Symposium SAS 2004 pages 84-99.

You might also be interested in related tools by other research groups: the Jif project or Flow Caml.

Support:

Development of SecJ was supported in part by the National Science Foundation under grants CCR-0208984 and CNS-0627338.

SecJ uses the java libraries SableCC and PolyGlot, which in turn depend on JavaCup and JFlex.