Mercurial > urweb
changeset 1228:7dfa67560916
Using multiple policies to check a written value
| author | Adam Chlipala <adamc@hcoop.net> |
|---|---|
| date | Sun, 11 Apr 2010 16:46:38 -0400 |
| parents | 1d8fba74e7f5 |
| children | a2cd6664f57f |
| files | src/iflow.sml tests/policy.ur |
| diffstat | 2 files changed, 112 insertions(+), 9 deletions(-) [+] |
line wrap: on
line diff
--- a/src/iflow.sml Sun Apr 11 16:06:16 2010 -0400 +++ b/src/iflow.sml Sun Apr 11 16:46:38 2010 -0400 @@ -310,6 +310,66 @@ lvi end +fun bumpLvars by = + let + fun lvi e = + case e of + Const _ => e + | Var _ => e + | Lvar lv => Lvar (lv + by) + | Func (f, es) => Func (f, map lvi es) + | Recd xes => Recd (map (fn (x, e) => (x, lvi e)) xes) + | Proj (e, f) => Proj (lvi e, f) + | Finish => e + in + lvi + end + +fun bumpLvarsP by = + let + fun lvi p = + case p of + True => p + | False => p + | Unknown => p + | And (p1, p2) => And (lvi p1, lvi p2) + | Or (p1, p2) => And (lvi p1, lvi p2) + | Reln (r, es) => Reln (r, map (bumpLvars by) es) + | Cond (e, p) => Cond (bumpLvars by e, lvi p) + in + lvi + end + +fun maxLvar e = + let + fun lvi e = + case e of + Const _ => 0 + | Var _ => 0 + | Lvar lv => lv + | Func (f, es) => foldl Int.max 0 (map lvi es) + | Recd xes => foldl Int.max 0 (map (lvi o #2) xes) + | Proj (e, f) => lvi e + | Finish => 0 + in + lvi e + end + +fun maxLvarP p = + let + fun lvi p = + case p of + True => 0 + | False => 0 + | Unknown => 0 + | And (p1, p2) => Int.max (lvi p1, lvi p2) + | Or (p1, p2) => Int.max (lvi p1, lvi p2) + | Reln (r, es) => foldl Int.max 0 (map maxLvar es) + | Cond (e, p) => Int.max (maxLvar e, lvi p) + in + lvi p + end + fun eq' (e1, e2) = case (e1, e2) of (Const p1, Const p2) => Prim.equal (p1, p2) @@ -2390,16 +2450,50 @@ in if decompH p (fn hyps => - (fl <> Control Where - andalso imply (hyps, [AReln (Known, [Var 0])], SOME [Var 0])) - orelse List.exists (fn (p', outs) => - decompG p' - (fn goals => imply (hyps, goals, SOME outs))) - client) then + let + val avail = foldl (fn (AReln (Sql tab, _), avail) => SS.add (avail, tab) + | (_, avail) => avail) SS.empty hyps + + fun tryCombos (maxLv, pols, g, outs) = + case pols of + [] => + decompG g + (fn goals => imply (hyps, goals, SOME outs)) + | (g1, outs1) :: pols => + let + val g1 = bumpLvarsP (maxLv + 1) g1 + val outs1 = map (bumpLvars (maxLv + 1)) outs1 + fun skip () = tryCombos (maxLv, pols, g, outs) + in + if decompG g1 + (List.all (fn AReln (Sql tab, _) => + SS.member (avail, tab) + | _ => true)) then + skip () + orelse tryCombos (Int.max (maxLv, + maxLvarP g1), + pols, + And (g1, g), + outs1 @ outs) + else + skip () + end + in + (fl <> Control Where + andalso imply (hyps, [AReln (Known, [Var 0])], SOME [Var 0])) + orelse List.exists (fn (p', outs) => + decompG p' + (fn goals => imply (hyps, goals, SOME outs))) + client + orelse tryCombos (0, client, True, []) + orelse (reset (); + Print.preface ("Untenable hypotheses", + Print.p_list p_atom hyps); + false) + end) then () else - (ErrorMsg.errorAt loc "The information flow policy may be violated here."; - Print.preface ("The state satisifies this predicate:", p_prop p)) + ErrorMsg.errorAt loc "The information flow policy may be violated here." end fun doAll e =
--- a/tests/policy.ur Sun Apr 11 16:06:16 2010 -0400 +++ b/tests/policy.ur Sun Apr 11 16:46:38 2010 -0400 @@ -9,7 +9,9 @@ CONSTRAINT Fruit FOREIGN KEY Fruit REFERENCES fruit(Id) (* Everyone may knows IDs and names. *) -policy sendClient (SELECT fruit.Id, fruit.Nam +policy sendClient (SELECT fruit.Id + FROM fruit) +policy sendClient (SELECT fruit.Nam FROM fruit) (* The weight is sensitive information; you must know the secret. *) @@ -50,11 +52,18 @@ AND order.Qty = 13) (fn x => <xml><li>{[x.Fruit.Nam]}: {[x.Order.Qty]}</li></xml>); + ro <- oneOrNoRows (SELECT fruit.Id, fruit.Nam + FROM fruit); + return <xml><body> <ul>{x1}</ul> <ul>{x2}</ul> + {case ro of + None => <xml>None</xml> + | Some _ => <xml>Some</xml>} + <form> Fruit name: <textbox{#Nam}/><br/> Secret: <textbox{#Secret}/><br/>