comparison src/iflow.sml @ 1241:58f5ac1bb849

Check for implicit flows via expressions injected into SQL
author Adam Chlipala <adamc@hcoop.net>
date Thu, 15 Apr 2010 14:21:12 -0400
parents 30f789d5e2ad
children 4ed556678214
comparison
equal deleted inserted replaced
1240:beb67ff4c8a0 1241:58f5ac1bb849
1455 ls 1455 ls
1456 else 1456 else
1457 x :: ls 1457 x :: ls
1458 end 1458 end
1459 1459
1460 fun deinj env e =
1461 case #1 e of
1462 ERel n => SOME (List.nth (env, n))
1463 | EField (e, f) =>
1464 (case deinj env e of
1465 NONE => NONE
1466 | SOME e => SOME (Proj (e, f)))
1467 | _ => NONE
1468
1460 fun expIn rv env rvOf = 1469 fun expIn rv env rvOf =
1461 let 1470 let
1462 fun expIn e = 1471 fun expIn e =
1463 let 1472 let
1464 fun default () = inl (rv ()) 1473 fun default () = inl (rv ())
1480 | SqKnown e => 1489 | SqKnown e =>
1481 (case expIn e of 1490 (case expIn e of
1482 inl e => inr (Reln (Known, [e])) 1491 inl e => inr (Reln (Known, [e]))
1483 | _ => inr Unknown) 1492 | _ => inr Unknown)
1484 | Inj e => 1493 | Inj e =>
1485 let 1494 inl (case deinj env e of
1486 fun deinj e = 1495 NONE => rv ()
1487 case #1 e of 1496 | SOME e => e)
1488 ERel n => List.nth (env, n)
1489 | EField (e, f) => Proj (deinj e, f)
1490 | _ => rv ()
1491 in
1492 inl (deinj e)
1493 end
1494 | SqFunc (f, e) => 1497 | SqFunc (f, e) =>
1495 (case expIn e of 1498 (case expIn e of
1496 inl e => inl (Func (Other f, [e])) 1499 inl e => inl (Func (Other f, [e]))
1497 | _ => default ()) 1500 | _ => default ())
1498 1501
1532 Env : exp list, 1535 Env : exp list,
1533 NextVar : unit -> exp, 1536 NextVar : unit -> exp,
1534 Add : atom -> unit, 1537 Add : atom -> unit,
1535 Save : unit -> 'a, 1538 Save : unit -> 'a,
1536 Restore : 'a -> unit, 1539 Restore : 'a -> unit,
1537 UsedExp : exp -> unit, 1540 UsedExp : bool * exp -> unit,
1538 Cont : queryMode 1541 Cont : queryMode
1539 } 1542 }
1540 1543
1541 fun doQuery (arg : 'a doQuery) e = 1544 fun doQuery (arg : 'a doQuery) (e as (_, loc)) =
1542 let 1545 let
1543 fun default () = print ("Warning: Information flow checker can't parse SQL query at " 1546 fun default () = ErrorMsg.errorAt loc "Information flow checker can't parse SQL query"
1544 ^ ErrorMsg.spanToString (#2 e) ^ "\n")
1545 in 1547 in
1546 case parse query e of 1548 case parse query e of
1547 NONE => default () 1549 NONE => default ()
1548 | SOME q => 1550 | SOME q =>
1549 let 1551 let
1576 fun addFrom () = app (fn (t, v) => #Add arg (AReln (Sql t, [rvOf v]))) (#From r) 1578 fun addFrom () = app (fn (t, v) => #Add arg (AReln (Sql t, [rvOf v]))) (#From r)
1577 1579
1578 fun usedFields e = 1580 fun usedFields e =
1579 case e of 1581 case e of
1580 SqConst _ => [] 1582 SqConst _ => []
1581 | Field (v, f) => [(v, f)] 1583 | Field (v, f) => [(false, Proj (rvOf v, f))]
1582 | Computed _ => [] 1584 | Computed _ => []
1583 | Binop (_, e1, e2) => removeDups (usedFields e1 @ usedFields e2) 1585 | Binop (_, e1, e2) => usedFields e1 @ usedFields e2
1584 | SqKnown _ => [] 1586 | SqKnown _ => []
1585 | Inj _ => [] 1587 | Inj e =>
1588 (case deinj (#Env arg) e of
1589 NONE => (ErrorMsg.errorAt loc "Expression injected into SQL is too complicated";
1590 [])
1591 | SOME e => [(true, e)])
1586 | SqFunc (_, e) => usedFields e 1592 | SqFunc (_, e) => usedFields e
1587 | Count => [] 1593 | Count => []
1588 1594
1589 fun doUsed () = case #Where r of 1595 fun doUsed () = case #Where r of
1590 NONE => () 1596 NONE => ()
1591 | SOME e => 1597 | SOME e =>
1592 #UsedExp arg (Recd (ListUtil.mapi 1598 app (#UsedExp arg) (usedFields e)
1593 (fn (n, (v, f)) => (Int.toString n,
1594 Proj (rvOf v, f)))
1595 (usedFields e)))
1596 1599
1597 fun normal' () = 1600 fun normal' () =
1598 case #Cont arg of 1601 case #Cont arg of
1599 SomeCol k => 1602 SomeCol k =>
1600 let 1603 let
1848 doQuery {Env = env, 1851 doQuery {Env = env,
1849 NextVar = Var o St.nextVar, 1852 NextVar = Var o St.nextVar,
1850 Add = fn a => St.assert [a], 1853 Add = fn a => St.assert [a],
1851 Save = St.stash, 1854 Save = St.stash,
1852 Restore = St.reinstate, 1855 Restore = St.reinstate,
1853 UsedExp = fn e => St.send false (e, loc), 1856 UsedExp = fn (b, e) => St.send b (e, loc),
1854 Cont = AllCols (fn _ => evalExp 1857 Cont = AllCols (fn _ => evalExp
1855 (acc :: r :: env) 1858 (acc :: r :: env)
1856 b (fn _ => default ()))} q 1859 b (fn _ => default ()))} q
1857 else 1860 else
1858 doQuery {Env = env, 1861 doQuery {Env = env,
1859 NextVar = Var o St.nextVar, 1862 NextVar = Var o St.nextVar,
1860 Add = fn a => St.assert [a], 1863 Add = fn a => St.assert [a],
1861 Save = St.stash, 1864 Save = St.stash,
1862 Restore = St.reinstate, 1865 Restore = St.reinstate,
1863 UsedExp = fn e => St.send false (e, loc), 1866 UsedExp = fn (b, e) => St.send b (e, loc),
1864 Cont = AllCols (fn x => 1867 Cont = AllCols (fn x =>
1865 (St.assert [AReln (Eq, [r, x])]; 1868 (St.assert [AReln (Eq, [r, x])];
1866 evalExp (acc :: r :: env) b k))} q 1869 evalExp (acc :: r :: env) b k))} q
1867 end) 1870 end)
1868 | EDml e => 1871 | EDml e =>