Automated Fixing Information Flow Errors using Pseudo Boolean Optimization

IFC Solver Details

The technical report describing this technique is available at http://www.eecs.berkeley.edu/~jha/ifc.pdf

Contact for clarification: jha@cs.berkeley.edu

Implementation Details

Please send me a mail to obtain the solver (kept offline on request).                 Solver is available for download her

Associated Perl Script

The implementation is in Ocaml and will need Ocamlrun for execution. Please go through the sample available here before trying to use it.

1. Help with Command Line

2. Input Grammar

3. Output Format

4. Assumptions to be kept in mind while using the solver

5. A Perl Script to read Minisat+ output and Map File

6. An Example: explaining how the solver works

 

_________________________________________________________________________________

1.Help with Command Line

jha@cantor:~/IFC/ext$ ./ifc_solver --help

ifc_solver [-input <INPUTFILE> | -output <OUTPUTFILE> | -map <MAPFILE>] [-mode <"silent" or "verbose"> [-form <"LIN" or "SAT">]

Default:

input -> stdin

output -> stdout

map -> stdout

form -> LIN

mode -> silent

 

  -input Input file specification

  -output Output file specification

  -map Map file specification

  -mode Mode specification (silent or verbose)

  -form Form specification (LIN or SAT)

  -help  Display this list of options

  --help Display this list of options

 

_________________________________________________________________________________

2.INPUT GRAMMAR

lattice_constraint:

LATTICE size lattice CONSTRAINTS constraints EOF_TOK

size:

INT_TOK

lattice:

aconstraint LATTICE_SEP lattice

| aconstraint

constraints:

CONSRAINT_SEP aconstraint constraints

| CONSTRAINT_SEP aconstraint

| comments constraints

comments:

COMMENT comments

| COMMENT

aconstraint:

LCURL left RCURL PREC LCURL right RCURL

|  compl_dec DEC_SEP weight DEC_SEP LCURL left RCURL PREC LCURL right RCURL

|  LCURL left RCURL EQUALS LCURL right RCURL

|  compl_dec DEC_SEP weight DEC_SEP LCURL left RCURL EQUALS LCURL right RCURL

compl_dec:

   SYMB_TOK

|  NOT_SYMB SYMB_TOK

|  NOT_SYMB SYMB_TOK AND_SYMB compl_dec

weight:

  INT_TOK

left:

   SYMB_TOK JOIN left

|  SYMB_TOK

|      {["BOTTOM"]}

right:

   SYMB_TOK JOIN right

|  SYMB_TOK

|  {["BOTTOM"]}

Some Lexer Details:

CONSTRAINT_SEP is "-->" (which was there in extended-jif examples)

LATTICE_SEP is ","

DECLASSIFIER_SEP is "#"

TOP = "*:"

SYMBOL

['a'-'z' 'A'-'Z' '[' ']' '_']['a'-'z' 'A'-'Z' '(' ')' '#' '@' '/' ',' '-' ':' '.' '_' '0'-'9' '[' ']']*

| ['[']['a'-'z' 'A'-'Z' '{' '}' '(' ')' '*' ' ' '#' '@' '/' ',' '-' ':' '.' '_' '0'-'9' '[' ']']*[']']

| "break "symbol

| "_: _"

 

_________________________________________________________________________________

3. Output Format

Input of Minisat+. Please check minisat+ documentation (Default: LIN format)

It can also generate constraints in DIMACS format (specify using “-form SAT” in command line.

Setting mode to verbose will give step by step information about the translation to SAT.

Note that for a variable j (as explained in the pdf document), varj_i is 1 if and only if varj is greater than/equal to i in the lattice. So, when a var "kuch" is assigned say 1100 and BOT was 0, Alice was 1, TOP was assigned 2 and Bob was 3.Then it means "kuch" is greater than/equal to Bot, greater than equal to Alice. It is not greater than or equal to Bob or Top.

Look at the theory document and Perl script for semantics of the output.

_________________________________________________________________________________

4. Issues

We assume that - (enforced by "simplifier function" ) (since this holds on information - flow constraints)

if operator is PREC - righthand side has only one variable or constant.

if operator is EQ - lefthand side has only one variable or constant.

 

Lattice constraints are basically inequalities representing the partial ordering of lattice. We require that the first lattice constraint be of type BOTTOM PREC ANYTHING, that is, I use first symbol as Bottom.

 

Also, lattice constraints must list all the lattice relations - transitive closure. If lattice is BOT <= A and A<= TOP and BOT <= B and B <= TOP. The list of constraints would be their transitive closure which would include BOT <= TOP.

_________________________________________________________________________________

5. Perl Script (Download)

This reads the minisat+ output and the map file and creates the final assignment file which maps each declassification to 0 or 1 and each label to a tuple representing the lattice constant assigned to each. A label is assigned 1 in position i if and only if it is assigned label greater than or equal to the constant i.

Explained further with this example output of the script (This is the output obtained from the sample.map and sample.res from the sample here ):

---------------------------------------------------------------------------

sample.res is obtained by running minisat+ and redirecting the output.

minisat+ sample.lin > sample.res

---------------------------------------------------------------------------

The sample.res in this case was -

c Parsing PB file...
c Converting 56 PB-constraints to clauses...
c  -- Unit propagations: (none)
c  -- Detecting intervals from adjacent constraints: ==
c  -- Clauses(.)/Splits(s): ...........................................
c ==================================[MINISAT+]==========================
c | Conflicts | Original         | Learnt                          | Progress |
c |          | Clauses Literals |     Max Clauses Literals    LPC |          |
c =====================================================================
c |        0 |      43      91 |     14       0       0    nan |  0.000 % |
c =====================================================================
c ESC[1mFound solution: 0ESC[0m
c ESC[1mOptimal solution: 0ESC[0m
s OPTIMUM FOUND
v dec10 -dec7 -dec9 x -var1_3 var8_3 -var6_0 -var6_1 var1_1 var8_1 var3_0 var8_0
 -var0_2 var2_2 -var5_0 -var5_1 -var1_2 -var4_0 -var4_1 var1_0 var2_0 var8_2 var
3_3 var2_3 -var3_2 -var0_0 -var5_2 var2_1 -var6_2 -var3_1 -var6_3 -var4_2 -var0_
3 -var5_3 -var4_3 -var0_1
c ______________________________________________________________________________
c
c restarts             : 1
c conflicts            : 0              (0 /sec)
c decisions            : 7              (1750 /sec)
c propagations         : 0              (0 /sec)
c inspects             : 0              (0 /sec)
c CPU time             : 0.004 s
c ______________________________________________________________________________
 

-----------------------------------------------------------------------------

Running the perl script using

jha@cantor:~/IFC/perl$ perl evaluate.pl -assign sample.res -map sample.map -output sample.op

generates the following sample.op file.

sample.op

Declassification: d1 is 0
Declassification: d2 is 0
Declassification: d1d2 is 1

---------------------------------------------
Variable: 0 BOTTOM is [0000]
Variable: 1 Alice: is [1100]
Variable: 2 TOP  is [1111]
Variable: 3 Bob: is [1001]
Variable: 4 leakAlice_apireceiver  is [0000]
Variable: 5 NV7  is [0000]
Variable: 6 while  is [0000]
Variable: 8 NV8  is [1111]