Mercurial > urweb

comparison src/iflow.sml @ 1207:ae3036773768

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Introduced the known() predicate
author Adam Chlipala <adamc@hcoop.net>
date Tue, 06 Apr 2010 09:51:36 -0400
parents 772760df4c4c
children b5a4c5407ae0
comparison
equal deleted inserted replaced
1206:772760df4c4c 1207:ae3036773768
27 27
28 structure Iflow :> IFLOW = struct 28 structure Iflow :> IFLOW = struct
29 29
30 open Mono 30 open Mono
31 31
32 structure IS = IntBinarySet
32 structure IM = IntBinaryMap 33 structure IM = IntBinaryMap
33 34
34 structure SS = BinarySetFn(struct 35 structure SS = BinarySetFn(struct
35 type ord_key = string 36 type ord_key = string
36 val compare = String.compare 37 val compare = String.compare
62 | Recd of (string * exp) list 63 | Recd of (string * exp) list
63 | Proj of exp * string 64 | Proj of exp * string
64 | Finish 65 | Finish
65 66
66 datatype reln = 67 datatype reln =
67 Sql of string 68 Known
69 | Sql of string
68 | Eq 70 | Eq
69 71
70 datatype prop = 72 datatype prop =
71 True 73 True
72 | False 74 | False
73 | Unknown 75 | Unknown
74 | And of prop * prop 76 | And of prop * prop
75 | Or of prop * prop 77 | Or of prop * prop
76 | Reln of reln * exp list 78 | Reln of reln * exp list
77 | Select of int * lvar * lvar * prop * exp 79 | Select of int * lvar * lvar * prop * exp
80
81 local
82 open Print
83 val string = PD.string
84 in
85
86 fun p_exp e =
87 case e of
88 Const p => Prim.p_t p
89 | Var n => string ("x" ^ Int.toString n)
90 | Lvar n => string ("X" ^ Int.toString n)
91 | Func (f, es) => box [string (f ^ "("),
92 p_list p_exp es,
93 string ")"]
94 | Recd xes => box [string "{",
95 p_list (fn (x, e) => box [string "x",
96 space,
97 string "=",
98 space,
99 p_exp e]) xes,
100 string "}"]
101 | Proj (e, x) => box [p_exp e,
102 string ("." ^ x)]
103 | Finish => string "FINISH"
104
105 fun p_reln r es =
106 case r of
107 Known =>
108 (case es of
109 [e] => box [string "known(",
110 p_exp e,
111 string ")"]
112 | _ => raise Fail "Iflow.p_reln: Known")
113 | Sql s => box [string (s ^ "("),
114 p_list p_exp es,
115 string ")"]
116 | Eq =>
117 (case es of
118 [e1, e2] => box [p_exp e1,
119 space,
120 string "=",
121 space,
122 p_exp e2]
123 | _ => raise Fail "Iflow.p_reln: Eq")
124
125 fun p_prop p =
126 case p of
127 True => string "True"
128 | False => string "False"
129 | Unknown => string "??"
130 | And (p1, p2) => box [string "(",
131 p_prop p1,
132 string ")",
133 space,
134 string "&&",
135 space,
136 string "(",
137 p_prop p2,
138 string ")"]
139 | Or (p1, p2) => box [string "(",
140 p_prop p1,
141 string ")",
142 space,
143 string "||",
144 space,
145 string "(",
146 p_prop p2,
147 string ")"]
148 | Reln (r, es) => p_reln r es
149 | Select (n1, n2, n3, p, e) => box [string ("select(x" ^ Int.toString n1
150 ^ ",X" ^ Int.toString n2
151 ^ ",X" ^ Int.toString n3
152 ^ "){"),
153 p_prop p,
154 string "}{",
155 p_exp e,
156 string "}"]
157
158 end
78 159
79 local 160 local
80 val count = ref 1 161 val count = ref 1
81 in 162 in
82 fun newLvar () = 163 fun newLvar () =
286 true 367 true
287 else 368 else
288 (restore saved; 369 (restore saved;
289 (*raise Imply (Reln (Eq, es1), Reln (Eq, es2));*) 370 (*raise Imply (Reln (Eq, es1), Reln (Eq, es2));*)
290 eq (x1, y2) andalso eq (y1, x2)) 371 eq (x1, y2) andalso eq (y1, x2))
372 end
373 | _ => false)
374 | (Known, Known) =>
375 (case (es1, es2) of
376 ([e1], [e2]) =>
377 let
378 fun walk e2 =
379 eq (e1, e2) orelse
380 case e2 of
381 Proj (e2, _) => walk e2
382 | _ => false
383 in
384 walk e2
291 end 385 end
292 | _ => false) 386 | _ => false)
293 | _ => false 387 | _ => false
294 388
295 fun imply (p1, p2) = 389 fun imply (p1, p2) =
342 | Exp of Mono.exp 436 | Exp of Mono.exp
343 437
344 fun chunkify e = 438 fun chunkify e =
345 case #1 e of 439 case #1 e of
346 EPrim (Prim.String s) => [String s] 440 EPrim (Prim.String s) => [String s]
347 | EStrcat (e1, e2) => chunkify e1 @ chunkify e2 441 | EStrcat (e1, e2) =>
442 let
443 val chs1 = chunkify e1
444 val chs2 = chunkify e2
445 in
446 case chs2 of
447 String s2 :: chs2' =>
448 (case List.last chs1 of
449 String s1 => List.take (chs1, length chs1 - 1) @ String (s1 ^ s2) :: chs2'
450 | _ => chs1 @ chs2)
451 | _ => chs1 @ chs2
452 end
348 | _ => [Exp e] 453 | _ => [Exp e]
349 454
350 type 'a parser = chunk list -> ('a * chunk list) option 455 type 'a parser = chunk list -> ('a * chunk list) option
351 456
352 fun always v chs = SOME (v, chs) 457 fun always v chs = SOME (v, chs)
382 487
383 fun alt p1 p2 chs = 488 fun alt p1 p2 chs =
384 case p1 chs of 489 case p1 chs of
385 NONE => p2 chs 490 NONE => p2 chs
386 | v => v 491 | v => v
492
493 fun altL ps =
494 case rev ps of
495 [] => (fn _ => NONE)
496 | p :: ps =>
497 foldl (fn (p1, p2) => alt p1 p2) p ps
387 498
388 fun opt p chs = 499 fun opt p chs =
389 case p chs of 500 case p chs of
390 NONE => SOME (NONE, chs) 501 NONE => SOME (NONE, chs)
391 | SOME (v, chs) => SOME (SOME v, chs) 502 | SOME (v, chs) => SOME (SOME v, chs)
423 val debug = ref false 534 val debug = ref false
424 535
425 fun log name p chs = 536 fun log name p chs =
426 (if !debug then 537 (if !debug then
427 case chs of 538 case chs of
428 String s :: [] => print (name ^ ": " ^ s ^ "\n") 539 String s :: _ => print (name ^ ": " ^ s ^ "\n")
429 | _ => print (name ^ ": blocked!\n") 540 | _ => print (name ^ ": blocked!\n")
430 else 541 else
431 (); 542 ();
432 p chs) 543 p chs)
433 544
434 fun list p chs = 545 fun list p chs =
435 (alt (wrap (follow p (follow (ws (const ",")) (list p))) 546 altL [wrap (follow p (follow (ws (const ",")) (list p)))
436 (fn (v, ((), ls)) => v :: ls)) 547 (fn (v, ((), ls)) => v :: ls),
437 (alt (wrap (ws p) (fn v => [v])) 548 wrap (ws p) (fn v => [v]),
438 (always []))) chs 549 always []] chs
439 550
440 val ident = keep (fn ch => Char.isAlphaNum ch orelse ch = #"_") 551 val ident = keep (fn ch => Char.isAlphaNum ch orelse ch = #"_")
441 552
442 val t_ident = wrap ident (fn s => if String.isPrefix "T_" s then 553 val t_ident = wrap ident (fn s => if String.isPrefix "T_" s then
443 String.extract (s, 2, NONE) 554 String.extract (s, 2, NONE)
459 570
460 datatype sqexp = 571 datatype sqexp =
461 SqConst of Prim.t 572 SqConst of Prim.t
462 | Field of string * string 573 | Field of string * string
463 | Binop of Rel * sqexp * sqexp 574 | Binop of Rel * sqexp * sqexp
464 575 | SqKnown of sqexp
465 val sqbrel = alt (wrap (const "=") (fn () => Exps (fn (e1, e2) => Reln (Eq, [e1, e2])))) 576 | Inj of Mono.exp
466 (alt (wrap (const "AND") (fn () => Props And)) 577
467 (wrap (const "OR") (fn () => Props Or))) 578 val sqbrel = altL [wrap (const "=") (fn () => Exps (fn (e1, e2) => Reln (Eq, [e1, e2]))),
579 wrap (const "AND") (fn () => Props And),
580 wrap (const "OR") (fn () => Props Or)]
468 581
469 datatype ('a, 'b) sum = inl of 'a | inr of 'b 582 datatype ('a, 'b) sum = inl of 'a | inr of 'b
470 583
471 fun int chs = 584 fun int chs =
472 case chs of 585 case chs of
485 end 598 end
486 | _ => NONE 599 | _ => NONE
487 600
488 val prim = wrap (follow (wrap int Prim.Int) (opt (const "::int8"))) #1 601 val prim = wrap (follow (wrap int Prim.Int) (opt (const "::int8"))) #1
489 602
603 fun known' chs =
604 case chs of
605 Exp (EFfi ("Basis", "sql_known"), _) :: chs => SOME ((), chs)
606 | _ => NONE
607
608 fun sqlify chs =
609 case chs of
610 Exp (EFfiApp ("Basis", f, [e]), _) :: chs =>
611 if String.isPrefix "sqlify" f then
612 SOME (e, chs)
613 else
614 NONE
615 | _ => NONE
616
490 fun sqexp chs = 617 fun sqexp chs =
491 log "sqexp" 618 log "sqexp"
492 (alt 619 (altL [wrap prim SqConst,
493 (wrap prim SqConst) 620 wrap sitem Field,
494 (alt 621 wrap known SqKnown,
495 (wrap sitem Field) 622 wrap sqlify Inj,
496 (wrap 623 wrap (follow (ws (const "("))
497 (follow (ws (const "(")) 624 (follow (wrap
498 (follow (wrap 625 (follow sqexp
499 (follow sqexp 626 (alt
500 (alt 627 (wrap
501 (wrap 628 (follow (ws sqbrel)
502 (follow (ws sqbrel) 629 (ws sqexp))
503 (ws sqexp)) 630 inl)
504 inl) 631 (always (inr ()))))
505 (always (inr ())))) 632 (fn (e1, sm) =>
506 (fn (e1, sm) => 633 case sm of
507 case sm of 634 inl (bo, e2) => Binop (bo, e1, e2)
508 inl (bo, e2) => Binop (bo, e1, e2) 635 | inr () => e1))
509 | inr () => e1)) 636 (const ")")))
510 (const ")"))) 637 (fn ((), (e, ())) => e)])
511 (fn ((), (e, ())) => e)))) 638 chs
512 chs 639
513 640 and known chs = wrap (follow known' (follow (const "(") (follow sqexp (const ")"))))
514 val select = wrap (follow (const "SELECT ") (list sitem)) 641 (fn ((), ((), (e, ()))) => e) chs
515 (fn ((), ls) => ls) 642
643 val select = log "select"
644 (wrap (follow (const "SELECT ") (list sitem))
645 (fn ((), ls) => ls))
516 646
517 val fitem = wrap (follow uw_ident 647 val fitem = wrap (follow uw_ident
518 (follow (const " AS ") 648 (follow (const " AS ")
519 t_ident)) 649 t_ident))
520 (fn (t, ((), f)) => (t, f)) 650 (fn (t, ((), f)) => (t, f))
521 651
522 val from = wrap (follow (const "FROM ") (list fitem)) 652 val from = log "from"
523 (fn ((), ls) => ls) 653 (wrap (follow (const "FROM ") (list fitem))
654 (fn ((), ls) => ls))
524 655
525 val wher = wrap (follow (ws (const "WHERE ")) sqexp) 656 val wher = wrap (follow (ws (const "WHERE ")) sqexp)
526 (fn ((), ls) => ls) 657 (fn ((), ls) => ls)
527 658
528 val query = wrap (follow (follow select from) (opt wher)) 659 val query = log "query"
529 (fn ((fs, ts), wher) => {Select = fs, From = ts, Where = wher}) 660 (wrap (follow (follow select from) (opt wher))
530 661 (fn ((fs, ts), wher) => {Select = fs, From = ts, Where = wher}))
531 fun queryProp rv oe e = 662
663 fun queryProp env rv oe e =
532 case parse query e of 664 case parse query e of
533 NONE => (print "Crap\n"; Unknown) 665 NONE => (print ("Warning: Information flow checker can't parse SQL query at "
666 ^ ErrorMsg.spanToString (#2 e) ^ "\n");
667 Unknown)
534 | SOME r => 668 | SOME r =>
535 let 669 let
536 val p = 670 val p =
537 foldl (fn ((t, v), p) => 671 foldl (fn ((t, v), p) =>
538 And (p, 672 And (p,
551 | Binop (bo, e1, e2) => 685 | Binop (bo, e1, e2) =>
552 inr (case (bo, expIn e1, expIn e2) of 686 inr (case (bo, expIn e1, expIn e2) of
553 (Exps f, inl e1, inl e2) => f (e1, e2) 687 (Exps f, inl e1, inl e2) => f (e1, e2)
554 | (Props f, inr p1, inr p2) => f (p1, p2) 688 | (Props f, inr p1, inr p2) => f (p1, p2)
555 | _ => Unknown) 689 | _ => Unknown)
690 | SqKnown e =>
691 inr (case expIn e of
692 inl e => Reln (Known, [e])
693 | _ => Unknown)
694 | Inj e =>
695 let
696 fun deinj (e, _) =
697 case e of
698 ERel n => List.nth (env, n)
699 | EField (e, f) => Proj (deinj e, f)
700 | _ => raise Fail "Iflow: non-variable injected into query"
701 in
702 inl (deinj e)
703 end
556 704
557 val p = case #Where r of 705 val p = case #Where r of
558 NONE => p 706 NONE => p
559 | SOME e => 707 | SOME e =>
560 case expIn e of 708 case expIn e of
705 853
706 val (b, st') = evalExp (Var acc :: Var r :: env) (b, st') 854 val (b, st') = evalExp (Var acc :: Var r :: env) (b, st')
707 855
708 val r' = newLvar () 856 val r' = newLvar ()
709 val acc' = newLvar () 857 val acc' = newLvar ()
710 val qp = queryProp r' NONE q 858 val qp = queryProp env r' NONE q
711 859
712 val doSubExp = subExp (r, r') o subExp (acc, acc') 860 val doSubExp = subExp (r, r') o subExp (acc, acc')
713 val doSubProp = subProp (r, r') o subProp (acc, acc') 861 val doSubProp = subProp (r, r') o subProp (acc, acc')
714 862
715 val p = doSubProp (#2 st') 863 val p = doSubProp (#2 st')
735 | ESpawn _ => default () 883 | ESpawn _ => default ()
736 end 884 end
737 885
738 fun check file = 886 fun check file =
739 let 887 let
888 val exptd = foldl (fn ((d, _), exptd) =>
889 case d of
890 DExport (_, _, n, _, _, _) => IS.add (exptd, n)
891 | _ => exptd) IS.empty file
892
740 fun decl ((d, _), (vals, pols)) = 893 fun decl ((d, _), (vals, pols)) =
741 case d of 894 case d of
742 DVal (x, _, _, e, _) => 895 DVal (_, n, _, e, _) =>
743 let 896 let
744 fun deAbs (e, env, nv) = 897 val isExptd = IS.member (exptd, n)
898
899 fun deAbs (e, env, nv, p) =
745 case #1 e of 900 case #1 e of
746 EAbs (_, _, _, e) => deAbs (e, Var nv :: env, nv + 1) 901 EAbs (_, _, _, e) => deAbs (e, Var nv :: env, nv + 1,
747 | _ => (e, env, nv) 902 if isExptd then
748 903 And (p, Reln (Known, [Var nv]))
749 val (e, env, nv) = deAbs (e, [], 1) 904 else
750 905 p)
751 val (e, (_, p, sent)) = evalExp env (e, (nv, True, [])) 906 | _ => (e, env, nv, p)
907
908 val (e, env, nv, p) = deAbs (e, [], 1, True)
909
910 val (e, (_, p, sent)) = evalExp env (e, (nv, p, []))
752 in 911 in
753 ((x, e, p, sent) :: vals, pols) 912 (sent @ vals, pols)
754 end 913 end
755 914
756 | DPolicy (PolQuery e) => (vals, queryProp 0 (SOME (Var 0)) e :: pols) 915 | DPolicy (PolQuery e) => (vals, queryProp [] 0 (SOME (Var 0)) e :: pols)
757 916
758 | _ => (vals, pols) 917 | _ => (vals, pols)
759 918
760 val () = reset () 919 val () = reset ()
761 920
762 val (vals, pols) = foldl decl ([], []) file 921 val (vals, pols) = foldl decl ([], []) file
763 in 922 in
764 app (fn (name, _, _, sent) => 923 app (fn (loc, e, p) =>
765 app (fn (loc, e, p) => 924 let
766 let 925 val p = And (p, Reln (Eq, [Var 0, e]))
767 val p = And (p, Reln (Eq, [Var 0, e])) 926 in
768 in 927 if List.exists (fn pol => imply (p, pol)) pols then
769 if List.exists (fn pol => imply (p, pol)) pols then 928 ()
770 () 929 else
771 else 930 (ErrorMsg.errorAt loc "The information flow policy may be violated here.";
772 ErrorMsg.errorAt loc "The information flow policy may be violated here." 931 Print.preface ("The state satisifes this predicate:", p_prop p))
773 end) sent) vals 932 end) vals
774 end 933 end
775 934
776 end 935 end