Information Flow Security Analysys for Java

IFlow supports confidentiality and integrity annotations and customizable securty lattices.

Unlike the Tainting checker provided with the CheckerFramework distribution, IFlow supports detection of implicit flows and of side effect generated leaks via method call, providing a fully sound security analysis.

Download IFlow 1.0 source code for CheckerFramework.

Example:

import org.checkerframework.checker.secrecy.qual.*;
import org.checkerframework.checker.integrity.qual.*;

public class testc {

/** START OF TRUSTED UNSAFE CODE */

/* declassify int to public value */
@SuppressWarnings("secrecy")
@ESecret
private @Public("student") int declassify(int x)
{
	return x;
}

/* endorse int to trusted value */
@SuppressWarnings("integrity")
@ESecret
private @Trusted int trust(@UnTrusted int x)
{
	return x;
}

/** END OF TRUSTED UNSAFE CODE */

@ESecret
public @Public int x(boolean b, @Public int j, @Public @UnTrusted int i) 
{

  @Secret int k=2;
  @Trusted int p = trust(1); 

  k = j+1;
  if(k==0) m4();
  j = j+i;
  if(j==i){j=i;} ;
  if(i==trust(0)){p=trust(0)+p;} 
  return j;

}

@EPublic
public void m2() 
{
   x(true,declassify(2),declassify(4));
}

@EPublic
public void m3(@Public int i)
{
@Public int j = declassify(9);
j = i;
}

@ESecret
public void m4()
{
    m3(declassify(2)); 
}



}