Mercurial > urweb
changeset 1207:ae3036773768
Introduced the known() predicate
| author | Adam Chlipala <adamc@hcoop.net> |
|---|---|
| date | Tue, 06 Apr 2010 09:51:36 -0400 |
| parents | 772760df4c4c |
| children | b5a4c5407ae0 |
| files | lib/ur/basis.urs src/iflow.sig src/iflow.sml src/mono_reduce.sml src/monoize.sml tests/policy.ur |
| diffstat | 6 files changed, 253 insertions(+), 60 deletions(-) [+] |
line wrap: on
line diff
--- a/lib/ur/basis.urs Sun Apr 04 17:44:12 2010 -0400 +++ b/lib/ur/basis.urs Tue Apr 06 09:51:36 2010 -0400 @@ -498,6 +498,7 @@ -> sql_ufunc dom ran -> sql_exp tables agg exps dom -> sql_exp tables agg exps ran val sql_octet_length : sql_ufunc blob int +val sql_known : t ::: Type -> sql_ufunc t bool val sql_nullable : tables ::: {{Type}} -> agg ::: {{Type}} -> exps ::: {Type} -> t ::: Type
--- a/src/iflow.sig Sun Apr 04 17:44:12 2010 -0400 +++ b/src/iflow.sig Tue Apr 06 09:51:36 2010 -0400 @@ -39,7 +39,8 @@ | Finish datatype reln = - Sql of string + Known + | Sql of string | Eq datatype prop =
--- a/src/iflow.sml Sun Apr 04 17:44:12 2010 -0400 +++ b/src/iflow.sml Tue Apr 06 09:51:36 2010 -0400 @@ -29,6 +29,7 @@ open Mono +structure IS = IntBinarySet structure IM = IntBinaryMap structure SS = BinarySetFn(struct @@ -64,7 +65,8 @@ | Finish datatype reln = - Sql of string + Known + | Sql of string | Eq datatype prop = @@ -77,6 +79,85 @@ | Select of int * lvar * lvar * prop * exp local + open Print + val string = PD.string +in + +fun p_exp e = + case e of + Const p => Prim.p_t p + | Var n => string ("x" ^ Int.toString n) + | Lvar n => string ("X" ^ Int.toString n) + | Func (f, es) => box [string (f ^ "("), + p_list p_exp es, + string ")"] + | Recd xes => box [string "{", + p_list (fn (x, e) => box [string "x", + space, + string "=", + space, + p_exp e]) xes, + string "}"] + | Proj (e, x) => box [p_exp e, + string ("." ^ x)] + | Finish => string "FINISH" + +fun p_reln r es = + case r of + Known => + (case es of + [e] => box [string "known(", + p_exp e, + string ")"] + | _ => raise Fail "Iflow.p_reln: Known") + | Sql s => box [string (s ^ "("), + p_list p_exp es, + string ")"] + | Eq => + (case es of + [e1, e2] => box [p_exp e1, + space, + string "=", + space, + p_exp e2] + | _ => raise Fail "Iflow.p_reln: Eq") + +fun p_prop p = + case p of + True => string "True" + | False => string "False" + | Unknown => string "??" + | And (p1, p2) => box [string "(", + p_prop p1, + string ")", + space, + string "&&", + space, + string "(", + p_prop p2, + string ")"] + | Or (p1, p2) => box [string "(", + p_prop p1, + string ")", + space, + string "||", + space, + string "(", + p_prop p2, + string ")"] + | Reln (r, es) => p_reln r es + | Select (n1, n2, n3, p, e) => box [string ("select(x" ^ Int.toString n1 + ^ ",X" ^ Int.toString n2 + ^ ",X" ^ Int.toString n3 + ^ "){"), + p_prop p, + string "}{", + p_exp e, + string "}"] + +end + +local val count = ref 1 in fun newLvar () = @@ -290,6 +371,19 @@ eq (x1, y2) andalso eq (y1, x2)) end | _ => false) + | (Known, Known) => + (case (es1, es2) of + ([e1], [e2]) => + let + fun walk e2 = + eq (e1, e2) orelse + case e2 of + Proj (e2, _) => walk e2 + | _ => false + in + walk e2 + end + | _ => false) | _ => false fun imply (p1, p2) = @@ -344,7 +438,18 @@ fun chunkify e = case #1 e of EPrim (Prim.String s) => [String s] - | EStrcat (e1, e2) => chunkify e1 @ chunkify e2 + | EStrcat (e1, e2) => + let + val chs1 = chunkify e1 + val chs2 = chunkify e2 + in + case chs2 of + String s2 :: chs2' => + (case List.last chs1 of + String s1 => List.take (chs1, length chs1 - 1) @ String (s1 ^ s2) :: chs2' + | _ => chs1 @ chs2) + | _ => chs1 @ chs2 + end | _ => [Exp e] type 'a parser = chunk list -> ('a * chunk list) option @@ -385,6 +490,12 @@ NONE => p2 chs | v => v +fun altL ps = + case rev ps of + [] => (fn _ => NONE) + | p :: ps => + foldl (fn (p1, p2) => alt p1 p2) p ps + fun opt p chs = case p chs of NONE => SOME (NONE, chs) @@ -425,17 +536,17 @@ fun log name p chs = (if !debug then case chs of - String s :: [] => print (name ^ ": " ^ s ^ "\n") + String s :: _ => print (name ^ ": " ^ s ^ "\n") | _ => print (name ^ ": blocked!\n") else (); p chs) fun list p chs = - (alt (wrap (follow p (follow (ws (const ",")) (list p))) - (fn (v, ((), ls)) => v :: ls)) - (alt (wrap (ws p) (fn v => [v])) - (always []))) chs + altL [wrap (follow p (follow (ws (const ",")) (list p))) + (fn (v, ((), ls)) => v :: ls), + wrap (ws p) (fn v => [v]), + always []] chs val ident = keep (fn ch => Char.isAlphaNum ch orelse ch = #"_") @@ -461,10 +572,12 @@ SqConst of Prim.t | Field of string * string | Binop of Rel * sqexp * sqexp + | SqKnown of sqexp + | Inj of Mono.exp -val sqbrel = alt (wrap (const "=") (fn () => Exps (fn (e1, e2) => Reln (Eq, [e1, e2])))) - (alt (wrap (const "AND") (fn () => Props And)) - (wrap (const "OR") (fn () => Props Or))) +val sqbrel = altL [wrap (const "=") (fn () => Exps (fn (e1, e2) => Reln (Eq, [e1, e2]))), + wrap (const "AND") (fn () => Props And), + wrap (const "OR") (fn () => Props Or)] datatype ('a, 'b) sum = inl of 'a | inr of 'b @@ -487,50 +600,71 @@ val prim = wrap (follow (wrap int Prim.Int) (opt (const "::int8"))) #1 +fun known' chs = + case chs of + Exp (EFfi ("Basis", "sql_known"), _) :: chs => SOME ((), chs) + | _ => NONE + +fun sqlify chs = + case chs of + Exp (EFfiApp ("Basis", f, [e]), _) :: chs => + if String.isPrefix "sqlify" f then + SOME (e, chs) + else + NONE + | _ => NONE + fun sqexp chs = log "sqexp" - (alt - (wrap prim SqConst) - (alt - (wrap sitem Field) - (wrap - (follow (ws (const "(")) - (follow (wrap - (follow sqexp - (alt - (wrap - (follow (ws sqbrel) - (ws sqexp)) - inl) - (always (inr ())))) - (fn (e1, sm) => - case sm of - inl (bo, e2) => Binop (bo, e1, e2) - | inr () => e1)) - (const ")"))) - (fn ((), (e, ())) => e)))) - chs + (altL [wrap prim SqConst, + wrap sitem Field, + wrap known SqKnown, + wrap sqlify Inj, + wrap (follow (ws (const "(")) + (follow (wrap + (follow sqexp + (alt + (wrap + (follow (ws sqbrel) + (ws sqexp)) + inl) + (always (inr ())))) + (fn (e1, sm) => + case sm of + inl (bo, e2) => Binop (bo, e1, e2) + | inr () => e1)) + (const ")"))) + (fn ((), (e, ())) => e)]) + chs -val select = wrap (follow (const "SELECT ") (list sitem)) - (fn ((), ls) => ls) +and known chs = wrap (follow known' (follow (const "(") (follow sqexp (const ")")))) + (fn ((), ((), (e, ()))) => e) chs + +val select = log "select" + (wrap (follow (const "SELECT ") (list sitem)) + (fn ((), ls) => ls)) val fitem = wrap (follow uw_ident (follow (const " AS ") t_ident)) (fn (t, ((), f)) => (t, f)) -val from = wrap (follow (const "FROM ") (list fitem)) - (fn ((), ls) => ls) +val from = log "from" + (wrap (follow (const "FROM ") (list fitem)) + (fn ((), ls) => ls)) val wher = wrap (follow (ws (const "WHERE ")) sqexp) (fn ((), ls) => ls) -val query = wrap (follow (follow select from) (opt wher)) - (fn ((fs, ts), wher) => {Select = fs, From = ts, Where = wher}) +val query = log "query" + (wrap (follow (follow select from) (opt wher)) + (fn ((fs, ts), wher) => {Select = fs, From = ts, Where = wher})) -fun queryProp rv oe e = +fun queryProp env rv oe e = case parse query e of - NONE => (print "Crap\n"; Unknown) + NONE => (print ("Warning: Information flow checker can't parse SQL query at " + ^ ErrorMsg.spanToString (#2 e) ^ "\n"); + Unknown) | SOME r => let val p = @@ -553,6 +687,20 @@ (Exps f, inl e1, inl e2) => f (e1, e2) | (Props f, inr p1, inr p2) => f (p1, p2) | _ => Unknown) + | SqKnown e => + inr (case expIn e of + inl e => Reln (Known, [e]) + | _ => Unknown) + | Inj e => + let + fun deinj (e, _) = + case e of + ERel n => List.nth (env, n) + | EField (e, f) => Proj (deinj e, f) + | _ => raise Fail "Iflow: non-variable injected into query" + in + inl (deinj e) + end val p = case #Where r of NONE => p @@ -707,7 +855,7 @@ val r' = newLvar () val acc' = newLvar () - val qp = queryProp r' NONE q + val qp = queryProp env r' NONE q val doSubExp = subExp (r, r') o subExp (acc, acc') val doSubProp = subProp (r, r') o subProp (acc, acc') @@ -737,23 +885,34 @@ fun check file = let + val exptd = foldl (fn ((d, _), exptd) => + case d of + DExport (_, _, n, _, _, _) => IS.add (exptd, n) + | _ => exptd) IS.empty file + fun decl ((d, _), (vals, pols)) = case d of - DVal (x, _, _, e, _) => + DVal (_, n, _, e, _) => let - fun deAbs (e, env, nv) = + val isExptd = IS.member (exptd, n) + + fun deAbs (e, env, nv, p) = case #1 e of - EAbs (_, _, _, e) => deAbs (e, Var nv :: env, nv + 1) - | _ => (e, env, nv) + EAbs (_, _, _, e) => deAbs (e, Var nv :: env, nv + 1, + if isExptd then + And (p, Reln (Known, [Var nv])) + else + p) + | _ => (e, env, nv, p) - val (e, env, nv) = deAbs (e, [], 1) + val (e, env, nv, p) = deAbs (e, [], 1, True) - val (e, (_, p, sent)) = evalExp env (e, (nv, True, [])) + val (e, (_, p, sent)) = evalExp env (e, (nv, p, [])) in - ((x, e, p, sent) :: vals, pols) + (sent @ vals, pols) end - | DPolicy (PolQuery e) => (vals, queryProp 0 (SOME (Var 0)) e :: pols) + | DPolicy (PolQuery e) => (vals, queryProp [] 0 (SOME (Var 0)) e :: pols) | _ => (vals, pols) @@ -761,16 +920,16 @@ val (vals, pols) = foldl decl ([], []) file in - 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 + 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."; + Print.preface ("The state satisifes this predicate:", p_prop p)) + end) vals end end
--- a/src/mono_reduce.sml Sun Apr 04 17:44:12 2010 -0400 +++ b/src/mono_reduce.sml Tue Apr 06 09:51:36 2010 -0400 @@ -193,6 +193,12 @@ else No + | (PPrim (Prim.String s), EStrcat (_, (EPrim (Prim.String s'), _))) => + if String.isSuffix s' s then + Maybe + else + No + | (PPrim p, EPrim p') => if Prim.equal (p, p') then Yes env
--- a/src/monoize.sml Sun Apr 04 17:44:12 2010 -0400 +++ b/src/monoize.sml Tue Apr 06 09:51:36 2010 -0400 @@ -2580,6 +2580,8 @@ "octet_length" else "length")), loc), fm) + | L.ECApp ((L.EFfi ("Basis", "sql_known"), _), _) => + ((L'.EFfi ("Basis", "sql_known"), loc), fm) | (L.ECApp ( (L.ECApp (
--- a/tests/policy.ur Sun Apr 04 17:44:12 2010 -0400 +++ b/tests/policy.ur Tue Apr 06 09:51:36 2010 -0400 @@ -8,13 +8,31 @@ PRIMARY KEY Id, CONSTRAINT Fruit FOREIGN KEY Fruit REFERENCES fruit(Id) -policy query_policy (SELECT fruit.Id, fruit.Nam, fruit.Weight +(* Everyone may knows IDs and names. *) +policy query_policy (SELECT fruit.Id, fruit.Nam FROM fruit) + +(* The weight is sensitive information; you must know the secret. *) +policy query_policy (SELECT fruit.Weight + FROM fruit + WHERE known(fruit.Secret)) + policy query_policy (SELECT order.Id, order.Fruit, order.Qty FROM order, fruit WHERE order.Fruit = fruit.Id AND order.Qty = 13) +fun fname r = + x <- queryX (SELECT fruit.Weight + FROM fruit + WHERE fruit.Nam = {[r.Nam]} + AND fruit.Secret = {[r.Secret]}) + (fn r => <xml>Weight is {[r.Fruit.Weight]}</xml>); + + return <xml><body> + {x} + </body></xml> + fun main () = x1 <- queryX (SELECT fruit.Id, fruit.Nam FROM fruit) @@ -29,4 +47,10 @@ return <xml><body> <ul>{x1}</ul> <ul>{x2}</ul> + + <form> + Fruit name: <textbox{#Nam}/><br/> + Secret: <textbox{#Secret}/><br/> + <submit action={fname}/> + </form> </body></xml>