Enforcing Secure Object Initialization in Java's web page

Formalization in Coq

• Download the Coq development [.tgz] (tested with Coq 8.2pl1 (September 2009)).

The annotation Java package

• Java package to annotate your Java sources files

Our on-line object initialization type checker

• Here is our on-line type checker prototype.

How to use it:

• compile your java source files using our annotation package (only if you need to add manual annotations, see below)
• give the path of the file and click on analyze, type checking is done !

How to annotate your classes

There are several kinds of annotations.

• @Init would specify that a reference must only point to a fully initialized object or to the null constant, but as it is the default annotation in all cases where it may be needed, it is in fact not implemented.
• @Raw specifies that a reference may point to an object under initialization.
• @Raw(C.class) refines the previous annotation by specifying an initialization level: a reference with this annotation may point to an object under initialization that has finished a constructor of class C (and therefore be initialized up-to C).
• @Pre and @Post take an annotation as argument and specify the level of initialization for instance methods of the receiver before and after the execution of the method, respectively. I.e. if a method m is annotated with @Pre(A) @Post(B), m may only be called on reference of a sub-type of A and those references may be refined to B after the method call, and the receiver has type A at the beginning of the m and must be of a sub-type of B at the end of the method.

Examples

import rawtypes.*;
import java.io.*;

class Sample{
    @Init Object f;               // default annotation

    @Pre(@Raw)                    // default annotation
    @Post(@Raw(Sample.class))     // default annotation
    Sample(@Init Object param){   // default annotation
        super();
        this.init(param);
    }
    
    @Pre(@Raw(Object.class)) // non-default: we call the init method on objects
                             // partially initialized
    @Post(@Raw(Sample.class)) // non-default: the object is more initialized at
                              // the end of the method
    private void init(@Init Object param){ //default annotation
        this.f = param;
        ChangeType.SetInit(); //we declare the object as initialized
    }

    @Pre(@Raw(Sample.class)) // non-default: we allow the method to be called on
                             // partially initialized objects, as long as this.f
                             // has been initialized
    public @Init Object getF(){ // default-annotation
        return this.f;
    }

    public void setF(Object f){ // no annotation, setF can only be called on
                                // fully initialized objects
        this.f = f;
    }
}

class Sample2 extends Sample{
    Sample2(){
        super(new Object());
        Object o = this.getF(); // allowed
        this.setF(o); // fails: the current object has not finished its
                      // construction
    }
    void m(){
        this.setF(new Object()); // allowed: the current object has finished its
                                 // construction as it is a precondition of m
                                 // (default annotation)
    }
}