Mercurial > urweb

comparison src/iflow.sml @ 1280:3d06e0f7a6f3

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Initial version of equalKnown working for secret
author Adam Chlipala <adam@chlipala.net>
date Tue, 27 Jul 2010 11:42:30 -0400
parents 9d65866ab9ab
children 60e19545841b
comparison
equal deleted inserted replaced
1279:4c367c8f5b2d 1280:3d06e0f7a6f3
1226 val addPath : check -> unit 1226 val addPath : check -> unit
1227 1227
1228 val allowSend : atom list * exp list -> unit 1228 val allowSend : atom list * exp list -> unit
1229 val send : check -> unit 1229 val send : check -> unit
1230 1230
1231 val allowEqualKnown : { table : string, field : string } -> unit
1232 val mayTest : prop -> bool
1233
1231 val allowInsert : atom list -> unit 1234 val allowInsert : atom list -> unit
1232 val insert : ErrorMsg.span -> unit 1235 val insert : ErrorMsg.span -> unit
1233 1236
1234 val allowDelete : atom list -> unit 1237 val allowDelete : atom list -> unit
1235 val delete : ErrorMsg.span -> unit 1238 val delete : ErrorMsg.span -> unit
1504 1507
1505 val deletable = ref ([] : atom list list) 1508 val deletable = ref ([] : atom list list)
1506 fun allowDelete v = deletable := v :: !deletable 1509 fun allowDelete v = deletable := v :: !deletable
1507 val delete = doable deletable 1510 val delete = doable deletable
1508 1511
1512 val testable = ref ([] : { table : string, field : string } list)
1513 fun allowEqualKnown v = testable := v :: !testable
1514 fun mayTest p =
1515 case p of
1516 Reln (Eq, [e1, e2]) =>
1517 let
1518 val (_, hs, _) = !hyps
1519
1520 fun tableInHyps (tab, x) = List.exists (fn AReln (Sql tab', [Var x']) => tab' = tab andalso x' = x
1521 | _ => false) hs
1522
1523 fun allowed (tab, v) =
1524 case tab of
1525 Proj (Var tab, fd) =>
1526 List.exists (fn {table = tab', field = fd'} =>
1527 fd' = fd
1528 andalso tableInHyps (tab', tab)) (!testable)
1529 andalso Cc.check (db, AReln (Known, [v]))
1530 | _ => false
1531 in
1532 if allowed (e1, e2) orelse allowed (e2, e1) then
1533 (Cc.assert (db, AReln (Eq, [e1, e2]));
1534 true)
1535 else
1536 false
1537 end
1538 | _ => false
1539
1509 fun reset () = (Cc.clear db; 1540 fun reset () = (Cc.clear db;
1510 path := []; 1541 path := [];
1511 hyps := (0, [], ref false); 1542 hyps := (0, [], ref false);
1512 nvar := 0; 1543 nvar := 0;
1513 sendable := []; 1544 sendable := [];
1545 testable := [];
1514 insertable := []; 1546 insertable := [];
1515 updatable := []; 1547 updatable := [];
1516 deletable := []) 1548 deletable := [])
1517 1549
1518 fun havocReln r = 1550 fun havocReln r =
1658 Env : exp list, 1690 Env : exp list,
1659 NextVar : unit -> exp, 1691 NextVar : unit -> exp,
1660 Add : atom -> unit, 1692 Add : atom -> unit,
1661 Save : unit -> 'a, 1693 Save : unit -> 'a,
1662 Restore : 'a -> unit, 1694 Restore : 'a -> unit,
1663 Cont : queryMode 1695 Cont : queryMode,
1696 Send : exp -> unit
1664 } 1697 }
1665 1698
1666 fun doQuery (arg : 'a doQuery) (e as (_, loc)) = 1699 fun doQuery (arg : 'a doQuery) (e as (_, loc)) =
1667 let 1700 let
1668 fun default () = ErrorMsg.errorAt loc "Information flow checker can't parse SQL query" 1701 fun default () = ErrorMsg.errorAt loc "Information flow checker can't parse SQL query"
1697 val expIn = expIn (#NextVar arg) (#Env arg) rvOf 1730 val expIn = expIn (#NextVar arg) (#Env arg) rvOf
1698 1731
1699 val saved = #Save arg () 1732 val saved = #Save arg ()
1700 fun addFrom () = app (fn (t, v) => #Add arg (AReln (Sql t, [rvOf v]))) (#From r) 1733 fun addFrom () = app (fn (t, v) => #Add arg (AReln (Sql t, [rvOf v]))) (#From r)
1701 1734
1702 fun usedFields e = 1735 fun leavesE e =
1703 case e of 1736 case e of
1704 SqConst _ => [] 1737 Const _ => []
1705 | SqTrue => [] 1738 | Var _ => []
1706 | SqFalse => [] 1739 | Lvar _ => []
1707 | Null => [] 1740 | Func (_, es) => List.concat (map leavesE es)
1708 | SqNot e => usedFields e 1741 | Recd xes => List.concat (map (leavesE o #2) xes)
1709 | Field (v, f) => [(false, Proj (rvOf v, f))] 1742 | Proj _ => [e]
1710 | Computed _ => [] 1743
1711 | Binop (_, e1, e2) => usedFields e1 @ usedFields e2 1744 fun leavesP p =
1712 | SqKnown _ => [] 1745 case p of
1713 | Inj e => 1746 True => []
1714 (case deinj (#Env arg) e of 1747 | False => []
1715 NONE => (ErrorMsg.errorAt loc "Expression injected into SQL is too complicated"; 1748 | Unknown => []
1716 []) 1749 | And (p1, p2) => leavesP p1 @ leavesP p2
1717 | SOME e => [(true, e)]) 1750 | Or (p1, p2) => leavesP p1 @ leavesP p2
1718 | SqFunc (_, e) => usedFields e 1751 | Reln (_, es) => List.concat (map leavesE es)
1719 | Unmodeled => [] 1752 | Cond (e, p) => e :: leavesP p
1720 1753
1721 fun normal' () = 1754 fun normal' () =
1722 case #Cont arg of 1755 case #Cont arg of
1723 SomeCol k => 1756 SomeCol k =>
1724 let 1757 let
1767 let 1800 let
1768 val p = case expIn e of 1801 val p = case expIn e of
1769 inl e => Reln (Eq, [e, Func (DtCon0 "Basis.bool.True", [])]) 1802 inl e => Reln (Eq, [e, Func (DtCon0 "Basis.bool.True", [])])
1770 | inr p => p 1803 | inr p => p
1771 1804
1805 fun getConjuncts p =
1806 case p of
1807 And (p1, p2) => getConjuncts p1 @ getConjuncts p2
1808 | _ => [p]
1809
1772 val saved = #Save arg () 1810 val saved = #Save arg ()
1811
1812 val conjs = getConjuncts p
1813 val conjs = List.filter (not o St.mayTest) conjs
1773 in 1814 in
1815 app (fn p => app (#Send arg) (leavesP p)) conjs;
1774 decomp {Save = #Save arg, Restore = #Restore arg, Add = #Add arg} 1816 decomp {Save = #Save arg, Restore = #Restore arg, Add = #Add arg}
1775 p (fn () => final () handle Cc.Contradiction => ()); 1817 p (fn () => final () handle Cc.Contradiction => ());
1776 #Restore arg saved 1818 #Restore arg saved
1777 end) 1819 end)
1778 handle Cc.Contradiction => () 1820 handle Cc.Contradiction => ()
2074 doQuery {Env = env, 2116 doQuery {Env = env,
2075 NextVar = Var o St.nextVar, 2117 NextVar = Var o St.nextVar,
2076 Add = fn a => St.assert [a], 2118 Add = fn a => St.assert [a],
2077 Save = St.stash, 2119 Save = St.stash,
2078 Restore = St.reinstate, 2120 Restore = St.reinstate,
2121 Send = fn e => St.send (e, loc),
2079 Cont = AllCols (fn x => 2122 Cont = AllCols (fn x =>
2080 (St.assert [AReln (Eq, [r, x])]; 2123 (St.assert [AReln (Eq, [r, x])];
2081 evalExp (acc :: r :: env) b k))} q 2124 evalExp (acc :: r :: env) b k))} q
2082 end) 2125 end)
2083 | EDml e => 2126 | EDml e =>
2446 fun doQ k = doQuery {Env = [], 2489 fun doQ k = doQuery {Env = [],
2447 NextVar = rv, 2490 NextVar = rv,
2448 Add = fn a => atoms := a :: !atoms, 2491 Add = fn a => atoms := a :: !atoms,
2449 Save = fn () => !atoms, 2492 Save = fn () => !atoms,
2450 Restore = fn ls => atoms := ls, 2493 Restore = fn ls => atoms := ls,
2494 Send = fn _ => (),
2451 Cont = SomeCol (fn r => k (rev (!atoms), r))} 2495 Cont = SomeCol (fn r => k (rev (!atoms), r))}
2452 2496
2453 fun untab (tab, nams) = List.filter (fn AReln (Sql tab', [Lvar lv]) => 2497 fun untab (tab, nams) = List.filter (fn AReln (Sql tab', [Lvar lv]) =>
2454 tab' <> tab 2498 tab' <> tab
2455 orelse List.all (fn Lvar lv' => lv' <> lv 2499 orelse List.all (fn Lvar lv' => lv' <> lv
2481 val outs = [Lvar 0] 2525 val outs = [Lvar 0]
2482 in 2526 in
2483 St.allowSend ([p], outs) 2527 St.allowSend ([p], outs)
2484 end 2528 end
2485 | _ => ()) 2529 | _ => ())
2530 | PolEqualKnown {table = tab, field = nm} =>
2531 (case #1 tab of
2532 EPrim (Prim.String tab) => St.allowEqualKnown {table = String.extract (tab, 3, NONE),
2533 field = nm}
2534 | _ => ErrorMsg.errorAt loc "Table for 'equalKnown' policy isn't fully resolved.")
2486 end 2535 end
2487 2536
2488 | _ => () 2537 | _ => ()
2489 in 2538 in
2490 app decl file 2539 app decl file