Sun and the CERT recommend for secure Java development to “not allow partially initialized objects to be accessed”. The solution currently used to enforce object initialization is to implement a coding pattern. We propose a modular type system to formally specify initialization policies and a type checker. The type system and its soundness theorem have been formalized and machine checked using Coq. This allows to prove the absence of bugs which have allowed some famous privilege escalations in Java. Our experimental results show that by adding 57 simple annotations we proved safe all classes but 4 our of java.lang, java.security and javax.security.

Static analysis is a powerful technique for automatic verification of programs but raises major engineering challenges when developing a full-fledged analyzer for a realistic language such as Java. This paper describes the Sawja library: a static analysis framework fully compliant with Java 6 which provides OCaml modules for efficiently manipulating Java bytecode programs. We present the main features of the library, including (i) efficient functional data-structures for representing program with implicit sharing and lazy parsing, (ii) an intermediate stack-less representation, and (iii) fast computation and manipulation of complete programs.

Although in most cases class initialization works as expected, some static fields may be read before being initialized, despite being initialized in their corresponding class initializer. We propose an analysis that can be applied to identify the static fields that may be read before being initialized and show how this can improve the precision of a null-pointer analysis.

Keywords: Java, semantics, class initialization, static analysis, control flow, verification

We present a non-null annotations inferencer for the Java bytecode language. This paper proposes extensions to our former analysis in order to deal with the Java bytecode language. We have implemented both analyses and compared their behaviour on several benchmarks. The results show a substantial improvement in the precision and, despite being a whole-program analysis, production applications can be analyzed within minutes.

Keywords: Java, NonNull, annotation, inference, static analysis

This paper proposes a semantics-based automatic null pointer analysis for inferring non-null annotations of fields in object-oriented programs. We prove the analysis correct with respect to a semantics of a minimalistic OO language and complete with respect to the non-null type system proposed by Fähndrich and Leino, in the sense that for every typable program the analysis is able to prove the absence of null dereferences without any hand-written annotations. Experiments with a prototype implementation of the analysis show that the inference is feasible for large programs.

Keywords: Java, NonNull, annotation, inference, static analysis