Mercurial > urweb
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 => |