CheckLT

# checklt -Alattice=yourxmlfile.xml YourClass.java

<linear-lattice>

    <!-- all levels must first be declared -->
    <levels>
        <level>Private</level>
        <level>UserTrusts</level>
        <level>User</level>
        <level>Public</level>
    </levels>


    <!-- 
         'level-specs' is a collection defining the relations
         of the various levels 
    -->
    <level-specs>

        <!-- level spec for Public -->
        <!-- (trusts everyone)     -->
        <level-spec>
            <name>Public</name>

            <trusts>
                <level>Private</level>
                <level>UserTrusts</level>
                <level>User</level>
            </trusts>
        </level-spec>

        <!-- level spec for User -->
        <level-spec>
            <name>User</name>

            <trusts>
                <level>UserTrusts</level>
                <level>Private</level>
            </trusts>
        </level-spec>


        <!-- level spec for UserTrusts -->
        <level-spec>
            <name>UserTrusts</name>

            <trusts>
                <level>Private</level>
            </trusts>
        </level-spec>


        <!-- level spec for UserTrusts -->
        <level-spec>
            <name>Private</name>

            <trusts>
                <!-- trusts no one (other than self) -->
            </trusts>
        </level-spec>

    </level-specs>

</linear-lattice>

Note: The DEFAULT level will always be ⊤. 
      It is determined by finding the element 
      of the lattice with the LEAST outgoing edges.

<level> ::= ‘"’ <string> ‘"’

<level-spec> ::= <level>

<security-annotation> ::= ‘@Level(’ <level-spec> ‘)’

@Level("Public")
int publicValue = 36;

@Level("Private")
int privateValue = 1337;

import checkers.latticetainting.quals.Level;


public class Simple {

    public static void main(String args[]) {

        // This assiangment is from Private -> Public
        // which is not allowed in our lattice

        //@Level("Public")
        //int e = Simple.testVal();

        // To allow such an assignment, we can "declassify" the value
        // like so:

        @Level("Private")
        int secretValue = Simple.testVal();

        @Level("Public")
        int publicValue = declassify(secretValue);

    }

    public static int testVal() {
        @Level("Private")
        int notSecret = 1000;
        return notSecret;
    }

    public static @Level("Public") int declassify(@Level("Private") int privateVal){
        // Specify "safe" here to override the lattice
        @SuppressWarnings("safe")
        @Level("Public")
        int publicVal = privateVal;

        return publicVal;
    }  
}

<linear-lattice>


    <levels>
        <level>Internal</level>
        <level>TouchedByUser</level>
    </levels>

    <level-specs>

        <level-spec>
            <name>Internal</name>

            <trusts>
                <level>TouchedByUser</level>
            </trusts>
        </level-spec>

        <!-- level spec for User -->
        <level-spec>
            <name>TouchedByUser</name>

            <trusts>
              <!-- 
                   this sort of information is "quarantined" and my not 
                   go anywhere
              -->
            </trusts>
        </level-spec>

    </level-specs>

</linear-lattice>

import java.sql.Connection;
import java.sql.DriverManager;
import java.sql.PreparedStatement;
import java.sql.ResultSet;
import java.sql.SQLException;
import java.sql.Statement;
import java.io.*;
import checkers.latticetainting.quals.*;


public class SqlExample {

    public Connection getConnection() throws Exception {
        Class.forName("com.mysql.jdbc.Driver");
        return DriverManager.getConnection("jdbc:mysql://localhost/examp");
    }

    // require that all of the executed queries are "Safe"
    private void executeQuery(@Level("Internal") String q) throws Exception {

        Connection c = getConnection();

        try {
            Statement stmt = getConnection().createStatement();
            ResultSet rs =   stmt.executeQuery(q);
        }finally {
            c.close();
        }
    }

    // internal queries are "Safe" by definition

    public @Level("Internal") String getBaseQuery()
    {
        @Level("Internal")
        String query = "SELECT * from test_table";

        return query;
    }

    // running an internal query is no problem, since the types 
    // @Level("Internal") will match throughout.
    public void runInternalQuery() throws Exception {
        executeQuery(getBaseQuery());
    }

    public void getAndRunQueryFromUser() throws Exception {

        // baseQuery is implicitly @Level("Internal")
        String baseQuery = getBaseQuery();

        // newQuery is now @Level("TouchedByUser");
        String newQuery = baseQuery + getQueryFromUser();


        // This call will fail
        //executeQuery(newQuery);

        // It must be called like:
        executeQuery(SqlExample.sanitizeUserInput(newQuery));
    }



    // Because this has not been explicitly marked with 
    // @Level("Internal"), it is "TouchedByUser" by default
    public String getQueryFromUser(){

      System.out.print("Enter Query Filter [NONE]: ");

      BufferedReader br = new BufferedReader(new InputStreamReader(System.in));

      String query = null;

      try {
          query =  br.readLine();
      } catch (IOException ioe) {
          System.out.println("IO Error?");
          System.exit(1);
      }
      return query;
    }



    public static @Level("Internal") String sanitizeUserInput(
         @Level("TouchedByUser") String dirty
    ){

        //
        // do some cleanup, remove SQL injections, etc
        //

        // Mark this as "clean" input
        @SuppressWarnings("safe")
        @Level("Internal")
        String clean = dirty;

        return clean;
    } 

    public static void main(String args[]) throws Exception {

        System.out.println("====Executing Database Test===");

        SqlExample ex = new SqlExample();

        // first, try to run an internal query.
        ex.runInternalQuery();
        // next, try to execute an internal query that has 
        // been modified by the user
        ex.getAndRunQueryFromUser();
    }

}

public void getAndRunQueryFromUser() throws Exception {

    // baseQuery is implicitly @Level("Internal")
        String baseQuery = getBaseQuery();

        // newQuery is now @Level("TouchedByUser");
        String newQuery = baseQuery + getQueryFromUser();


        // This call will fail
        //executeQuery(newQuery);

        // It must be called like:
        executeQuery(SqlExample.sanitizeUserInput(newQuery));
}