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
The implementation is in Ocaml and will need Ocamlrun for execution. Please go through the sample available here before trying to use it.
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
_________________________________________________________________________________
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
_________________________________________________________________________________
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
| "_: _"
_________________________________________________________________________________
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.
_________________________________________________________________________________
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]