# HG changeset patch # User Adam Chlipala # Date 1270412243 14400 # Node ID 509a6d7b60fb0f034f633e02515ec12e1eeda733 # Parent 8793fd48968c0c13261cb5a05ce15f00cbdafe29 Iflow tested with positive and negative cases diff -r 8793fd48968c -r 509a6d7b60fb src/iflow.sig --- a/src/iflow.sig Sun Apr 04 15:17:57 2010 -0400 +++ b/src/iflow.sig Sun Apr 04 16:17:23 2010 -0400 @@ -51,7 +51,7 @@ | Reln of reln * exp list | Select of int * lvar * lvar * prop * exp - exception Summaries of (string * exp * prop * (exp * prop) list) list + exception Imply of prop * prop val check : Mono.file -> unit diff -r 8793fd48968c -r 509a6d7b60fb src/iflow.sml --- a/src/iflow.sml Sun Apr 04 15:17:57 2010 -0400 +++ b/src/iflow.sml Sun Apr 04 16:17:23 2010 -0400 @@ -29,6 +29,8 @@ open Mono +structure IM = IntBinaryMap + structure SS = BinarySetFn(struct type ord_key = string val compare = String.compare @@ -75,7 +77,7 @@ | Select of int * lvar * lvar * prop * exp local - val count = ref 0 + val count = ref 1 in fun newLvar () = let @@ -116,17 +118,6 @@ sub end -fun eq' (e1, e2) = - case (e1, e2) of - (Const p1, Const p2) => Prim.equal (p1, p2) - | (Var n1, Var n2) => n1 = n2 - | (Lvar n1, Lvar n2) => n1 = n2 - | (Func (f1, es1), Func (f2, es2)) => f1 = f2 andalso ListPair.allEq eq' (es1, es2) - | (Recd xes1, Recd xes2) => ListPair.allEq (fn ((x1, e1), (x2, e2)) => x1 = x2 andalso eq' (e1, e2)) (xes1, xes2) - | (Proj (e1, s1), Proj (e2, s2)) => eq' (e1, e2) andalso s1 = s2 - | (Finish, Finish) => true - | _ => false - fun isKnown e = case e of Const _ => true @@ -174,14 +165,12 @@ Proj (e', s)) | Finish => Finish -fun eq (e1, e2) = eq' (simplify e1, simplify e2) - -fun decomp or = +fun decomp fals or = let fun decomp p k = case p of True => k [] - | False => true + | False => fals | Unknown => k [] | And (p1, p2) => decomp p1 (fn ps1 => @@ -195,22 +184,155 @@ decomp end -fun rimp ((r1 : reln, es1), (r2, es2)) = - r1 = r2 andalso ListPair.allEq eq (es1, es2) +val unif = ref (IM.empty : exp IM.map) -fun imp (p1, p2) = - decomp (fn (e1, e2) => e1 andalso e2 ()) p1 - (fn hyps => - decomp (fn (e1, e2) => e1 orelse e2 ()) p2 - (fn goals => - List.all (fn r2 => List.exists (fn r1 => rimp (r1, r2)) hyps) goals)) +fun lvarIn lv = + let + fun lvi e = + case e of + Const _ => false + | Var _ => false + | Lvar lv' => lv' = lv + | Func (_, es) => List.exists lvi es + | Recd xes => List.exists (lvi o #2) xes + | Proj (e, _) => lvi e + | Finish => false + in + lvi + end + +fun eq' (e1, e2) = + case (e1, e2) of + (Const p1, Const p2) => Prim.equal (p1, p2) + | (Var n1, Var n2) => n1 = n2 + + | (Lvar n1, _) => + (case IM.find (!unif, n1) of + SOME e1 => eq' (e1, e2) + | NONE => + case e2 of + Lvar n2 => + (case IM.find (!unif, n2) of + SOME e2 => eq' (e1, e2) + | NONE => n1 = n2 + orelse (unif := IM.insert (!unif, n1, e2); + true)) + | _ => + if lvarIn n1 e2 then + false + else + (unif := IM.insert (!unif, n1, e2); + true)) + + | (_, Lvar n2) => + (case IM.find (!unif, n2) of + SOME e2 => eq' (e1, e2) + | NONE => + if lvarIn n2 e1 then + false + else + (unif := IM.insert (!unif, n2, e1); + true)) + + | (Func (f1, es1), Func (f2, es2)) => f1 = f2 andalso ListPair.allEq eq' (es1, es2) + | (Recd xes1, Recd xes2) => ListPair.allEq (fn ((x1, e1), (x2, e2)) => x1 = x2 andalso eq' (e1, e2)) (xes1, xes2) + | (Proj (e1, s1), Proj (e2, s2)) => eq' (e1, e2) andalso s1 = s2 + | (Finish, Finish) => true + | _ => false + +fun eq (e1, e2) = + let + val saved = !unif + in + if eq' (simplify e1, simplify e2) then + true + else + (unif := saved; + false) + end + +exception Imply of prop * prop + +fun rimp ((r1, es1), (r2, es2)) = + case (r1, r2) of + (Sql r1', Sql r2') => + r1' = r2' andalso + (case (es1, es2) of + ([Recd xes1], [Recd xes2]) => + let + val saved = !unif + in + (*print ("Go: " ^ r1' ^ "\n");*) + (*raise Imply (Reln (r1, es1), Reln (r2, es2));*) + if List.all (fn (f, e2) => + List.exists (fn (f', e1) => + f' = f andalso eq (e1, e2)) xes1) xes2 then + true + else + (unif := saved; + false) + end + | _ => false) + | (Eq, Eq) => + (case (es1, es2) of + ([x1, y1], [x2, y2]) => + let + val saved = !unif + in + if eq (x1, x2) andalso eq (y1, y2) then + true + else + (unif := saved; + (*raise Imply (Reln (Eq, es1), Reln (Eq, es2));*) + eq (x1, y2) andalso eq (y1, x2)) + end + | _ => false) + | _ => false + +fun imply (p1, p2) = + (unif := IM.empty; + (*raise (Imply (p1, p2));*) + decomp true (fn (e1, e2) => e1 andalso e2 ()) p1 + (fn hyps => + decomp false (fn (e1, e2) => e1 orelse e2 ()) p2 + (fn goals => + let + fun gls goals onFail = + case goals of + [] => true + | g :: goals => + let + fun hps hyps = + case hyps of + [] => onFail () + | h :: hyps => + let + val saved = !unif + in + if rimp (h, g) then + let + val changed = IM.numItems (!unif) = IM.numItems saved + in + gls goals (fn () => (unif := saved; + changed andalso hps hyps)) + end + else + hps hyps + end + in + hps hyps + end + in + gls goals (fn () => false) + end))) + fun patCon pc = case pc of PConVar n => "C" ^ Int.toString n | PConFfi {mod = m, datatyp = d, con = c, ...} => m ^ "." ^ d ^ "." ^ c -exception Summaries of (string * exp * prop * (exp * prop) list) list + datatype chunk = String of string @@ -226,8 +348,8 @@ fun always v chs = SOME (v, chs) -fun parse p chs = - case p chs of +fun parse p s = + case p (chunkify s) of SOME (v, []) => SOME v | _ => NONE @@ -325,21 +447,33 @@ val query = wrap (follow select from) (fn (fs, ts) => {Select = fs, From = ts}) -fun queryProp rv e = - case parse query (chunkify e) of +fun queryProp rv oe e = + case parse query e of NONE => Unknown | SOME r => - foldl (fn ((t, v), p) => - And (p, - Reln (Sql t, - [Recd (foldl (fn ((v', f), fs) => - if v' = v then - (f, Proj (Proj (Lvar rv, v), f)) :: fs - else - fs) [] (#Select r))]))) - True (#From r) + let + val p = + foldl (fn ((t, v), p) => + And (p, + Reln (Sql t, + [Recd (foldl (fn ((v', f), fs) => + if v' = v then + (f, Proj (Proj (Lvar rv, v), f)) :: fs + else + fs) [] (#Select r))]))) + True (#From r) + in + case oe of + NONE => p + | SOME oe => + And (p, + foldl (fn ((v, f), p) => + Or (p, + Reln (Eq, [oe, Proj (Proj (Lvar rv, v), f)]))) + False (#Select r)) + end -fun evalExp env (e : Mono.exp, st as (nv, p, sent)) = +fun evalExp env (e as (_, loc), st as (nv, p, sent)) = let fun default () = (Var nv, (nv+1, p, sent)) @@ -348,7 +482,7 @@ if isKnown e then sent else - (e, p) :: sent + (loc, e, p) :: sent in case #1 e of EPrim p => (Const p, st) @@ -476,7 +610,7 @@ val r' = newLvar () val acc' = newLvar () - val qp = queryProp r' q + val qp = queryProp r' NONE q val doSubExp = subExp (r, r') o subExp (acc, acc') val doSubProp = subProp (r, r') o subProp (acc, acc') @@ -485,7 +619,9 @@ val p = And (p, qp) val p = Select (r, r', acc', p, doSubExp b) in - (Var r, (#1 st + 1, And (#2 st, p), map (fn (e, p) => (doSubExp e, And (qp, doSubProp p))) (#3 st'))) + (Var r, (#1 st + 1, And (#2 st, p), map (fn (loc, e, p) => (loc, + doSubExp e, + And (qp, doSubProp p))) (#3 st'))) end | EDml _ => default () | ENextval _ => default () @@ -504,7 +640,7 @@ fun check file = let - fun decl ((d, _), summaries) = + fun decl ((d, _), (vals, pols)) = case d of DVal (x, _, _, e, _) => let @@ -513,15 +649,31 @@ EAbs (_, _, _, e) => deAbs (e, Var nv :: env, nv + 1) | _ => (e, env, nv) - val (e, env, nv) = deAbs (e, [], 0) + val (e, env, nv) = deAbs (e, [], 1) val (e, (_, p, sent)) = evalExp env (e, (nv, True, [])) in - (x, e, p, sent) :: summaries + ((x, e, p, sent) :: vals, pols) end - | _ => summaries + + | DPolicy (PolQuery e) => (vals, queryProp 0 (SOME (Var 0)) e :: pols) + + | _ => (vals, pols) + + val () = unif := IM.empty + + val (vals, pols) = foldl decl ([], []) file in - raise Summaries (foldl decl [] file) + app (fn (name, _, _, sent) => + app (fn (loc, e, p) => + let + val p = And (p, Reln (Eq, [Var 0, e])) + in + if List.exists (fn pol => imply (p, pol)) pols then + () + else + ErrorMsg.errorAt loc "The information flow policy may be violated here." + end) sent) vals end end diff -r 8793fd48968c -r 509a6d7b60fb tests/policy.ur --- a/tests/policy.ur Sun Apr 04 15:17:57 2010 -0400 +++ b/tests/policy.ur Sun Apr 04 16:17:23 2010 -0400 @@ -1,11 +1,11 @@ table fruit : { Id : int, Nam : string, Weight : float, Secret : string } -policy query_policy (SELECT fruit.Id, fruit.Nam, fruit.Weight FROM fruit) +policy query_policy (SELECT fruit.Id, fruit.Nam FROM fruit) fun main () = - xml <- queryX (SELECT fruit.Id, fruit.Nam + xml <- queryX (SELECT fruit.Id, fruit.Nam, fruit.Secret FROM fruit) - (fn x =>
  • {[x.Fruit.Nam]}
    • ); + (fn x =>
  • {[x.Fruit.Secret]}
    • ); return {xml}