Secure the Clones
A companion web page

Formalization in Coq

The annotation Java package

The secure cloning type checker

How to use it

How to annotate your classes

There are several kinds of annotations.

Examples

A sample List class, implementing two copy methods, and annotated with two different policies.

@DeclareCopyPolicy(     // Declare a policy DL for in-depth copy.
  id = "DL",
  policy = {@FieldCopy(value="val", copy=@Deep("V.Default")),
            @FieldCopy(value="next", copy=@Deep("DL"))})

public class MyList implements Cloneable
{
    public @Shallow V val;    // Declare val as a Shallow field in the default policy.
    public @Deep MyList next; // Declare next as a Deep field in the default policy.

    public MyList(V val, MyList next) {
	this.val = val;
	this.next = next;
    }

    @Copy                   // The clone() method will adhere to the default copy policy.
    public MyList clone() {
        return new MyList(val,(next==null)?null:next.clone());
    }

    @Copy("MyList.DL")      // The deepClone() method will adhere to the DL copy policy.
    public MyList deepClone() {
        return new MyList((V) ((MyCloneable) val).clone(),(next==null)?null:next.deepClone());
    }

    public static void main(String[] args) {
	System.out.println("OK");
    }
}

Diff result between annotated and vanilla LinkedList from the GNU Classpath. Several obervations can be made:

46,47d45
< import jamvm.java.security.*;
< 
89c87
<   transient @Deep Entry first;
---
>   transient Entry first;
94c92
<   transient @Deep Entry last;
---
>   transient Entry last;
107c105
<     @Shallow T data;
---
>     T data;
110c108
<     @Deep Entry next;
---
>     Entry next;
113c111
<     @Deep Entry previous;
---
>     Entry previous;
529,645d501
<   // Duplicate the addAll method, marking it private to enable inlining.
<   private boolean cloneAddAll(Collection c)
<   {
<     int index = size;
<     checkBoundsInclusive(index);
<     int csize = c.size();
< 
<     if (csize == 0)
<       return false;
< 
<     Iterator itr = c.iterator();
< 
<     // Get the entries just before and after index. 
<     Entry after = null;
<     Entry before = null;
<     before = last;
< 
<     // Create the first new entry. 
<     Entry e = new Entry(itr.next());
<     e.previous = before;
<     Entry prev = e;
<     Entry firstNew = e;
< 
<     // Create and link all the remaining entries.
<     for (int pos = 1; pos < csize; pos++)
<       {
<         e = new Entry(itr.next());
<         e.previous = prev;
<         prev.next = e;
<         prev = e;
<       }
< 
<     // Link the new chain of entries into the list.
<     modCount++;
<     size += csize;
<     prev.next = after;
<     if (after != null)
<       after.previous = e;
<     else
<       last = e;
< 
<     if (before != null)
<       before.next = firstNew;
<     else
<       first = firstNew;
<     return true;
<   }
< 
660,671d515
<   // Duplicate the cloneClear method, marking it private to enable inlining.
<   private void cloneClear()
<   {
<     modCount++;
<     first = null;
<     last = null;
<     size = 0;
<   }
< 
807d650
<   @Copy
818,819c661,662
<     copy.cloneClear();
<     copy.cloneAddAll(this);
---
>     copy.clear();
>     copy.addAll(this);

Performance

The following benchmark plots the real time used by the analysis, by the number of lines of bytecode in the clone methods of the unannotated GNU Classpath. The size of the nodes is proportional to the size of the infered types. Method signatures are displayed by hovering on nodes.