summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--src/iflow.sig5
-rw-r--r--src/iflow.sml89
-rw-r--r--tests/policy.ur13
3 files changed, 76 insertions, 31 deletions
diff --git a/src/iflow.sig b/src/iflow.sig
index bc481022..f85322ef 100644
--- a/src/iflow.sig
+++ b/src/iflow.sig
@@ -42,6 +42,11 @@ signature IFLOW = sig
Known
| Sql of string
| Eq
+ | Ne
+ | Lt
+ | Le
+ | Gt
+ | Ge
datatype prop =
True
diff --git a/src/iflow.sml b/src/iflow.sml
index 58b38e6c..4dfa4e8d 100644
--- a/src/iflow.sml
+++ b/src/iflow.sml
@@ -68,6 +68,11 @@ datatype reln =
Known
| Sql of string
| Eq
+ | Ne
+ | Lt
+ | Le
+ | Gt
+ | Ge
datatype prop =
True
@@ -92,7 +97,7 @@ fun p_exp e =
p_list p_exp es,
string ")"]
| Recd xes => box [string "{",
- p_list (fn (x, e) => box [string "x",
+ p_list (fn (x, e) => box [string x,
space,
string "=",
space,
@@ -102,6 +107,15 @@ fun p_exp e =
string ("." ^ x)]
| Finish => string "FINISH"
+fun p_bop s es =
+ case es of
+ [e1, e2] => box [p_exp e1,
+ space,
+ string s,
+ space,
+ p_exp e2]
+ | _ => raise Fail "Iflow.p_bop"
+
fun p_reln r es =
case r of
Known =>
@@ -113,14 +127,12 @@ fun p_reln r es =
| 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")
+ | Eq => p_bop "=" es
+ | Ne => p_bop "<>" es
+ | Lt => p_bop "<" es
+ | Le => p_bop "<=" es
+ | Gt => p_bop ">" es
+ | Ge => p_bop ">=" es
fun p_prop p =
case p of
@@ -660,8 +672,9 @@ val t_ident = wrap ident (fn s => if String.isPrefix "T_" s then
String.extract (s, 2, NONE)
else
raise Fail "Iflow: Bad table variable")
-val uw_ident = wrap ident (fn s => if String.isPrefix "uw_" s then
- String.extract (s, 3, NONE)
+val uw_ident = wrap ident (fn s => if String.isPrefix "uw_" s andalso size s >= 4 then
+ str (Char.toUpper (String.sub (s, 3)))
+ ^ String.extract (s, 4, NONE)
else
raise Fail "Iflow: Bad uw_* variable")
@@ -681,7 +694,14 @@ datatype sqexp =
| SqKnown of sqexp
| Inj of Mono.exp
-val sqbrel = altL [wrap (const "=") (fn () => Exps (fn (e1, e2) => Reln (Eq, [e1, e2]))),
+fun cmp s r = wrap (const s) (fn () => Exps (fn (e1, e2) => Reln (r, [e1, e2])))
+
+val sqbrel = altL [cmp "=" Eq,
+ cmp "<>" Ne,
+ cmp "<=" Le,
+ cmp "<" Lt,
+ cmp ">=" Ge,
+ cmp ">" Gt,
wrap (const "AND") (fn () => Props And),
wrap (const "OR") (fn () => Props Or)]
@@ -788,7 +808,7 @@ fun queryProp env rv oe e =
case parse query e of
NONE => (print ("Warning: Information flow checker can't parse SQL query at "
^ ErrorMsg.spanToString (#2 e) ^ "\n");
- Unknown)
+ (Unknown, []))
| SOME r =>
let
val p =
@@ -826,6 +846,14 @@ fun queryProp env rv oe e =
inl (deinj e)
end
+ fun usedFields e =
+ case e of
+ SqConst _ => []
+ | Field (v, f) => [Proj (Proj (Lvar rv, v), f)]
+ | Binop (_, e1, e2) => usedFields e1 @ usedFields e2
+ | SqKnown _ => []
+ | Inj _ => []
+
val p = case #Where r of
NONE => p
| SOME e =>
@@ -833,13 +861,17 @@ fun queryProp env rv oe e =
inr p' => And (p, p')
| _ => p
in
- case oe of
- NONE => p
- | SOME oe =>
- And (p, foldl (fn ((v, f), p) =>
- Or (p,
- Reln (Eq, [oe, Proj (Proj (Lvar rv, v), f)])))
- False (#Select r))
+ (case oe of
+ NONE => p
+ | SOME oe =>
+ And (p, foldl (fn ((v, f), p) =>
+ Or (p,
+ Reln (Eq, [oe, Proj (Proj (Lvar rv, v), f)])))
+ False (#Select r)),
+
+ case #Where r of
+ NONE => []
+ | SOME e => usedFields e)
end
fun evalExp env (e as (_, loc), st as (nv, p, sent)) =
@@ -979,18 +1011,21 @@ fun evalExp env (e as (_, loc), st as (nv, p, sent)) =
val r' = newLvar ()
val acc' = newLvar ()
- val qp = queryProp env r' NONE q
+ val (qp, used) = queryProp env r' NONE q
val doSubExp = subExp (r, r') o subExp (acc, acc')
val doSubProp = subProp (r, r') o subProp (acc, acc')
val p = doSubProp (#2 st')
- val p = And (p, qp)
- val p = Select (r, r', acc', p, doSubExp b)
+ val p' = And (p, qp)
+ val p = Select (r, r', acc', p', doSubExp b)
+
+ val sent = map (fn (loc, e, p) => (loc,
+ doSubExp e,
+ And (qp, doSubProp p))) (#3 st')
+ val sent = map (fn e => (loc, e, p')) used @ sent
in
- (Var r, (#1 st + 1, And (#2 st, p), map (fn (loc, e, p) => (loc,
- doSubExp e,
- And (qp, doSubProp p))) (#3 st')))
+ (Var r, (#1 st + 1, And (#2 st, p), sent))
end
| EDml _ => default ()
| ENextval _ => default ()
@@ -1036,7 +1071,7 @@ fun check file =
(sent @ vals, pols)
end
- | DPolicy (PolQuery e) => (vals, queryProp [] 0 (SOME (Var 0)) e :: pols)
+ | DPolicy (PolQuery e) => (vals, #1 (queryProp [] 0 (SOME (Var 0)) e) :: pols)
| _ => (vals, pols)
diff --git a/tests/policy.ur b/tests/policy.ur
index 6f2d2d5b..40850393 100644
--- a/tests/policy.ur
+++ b/tests/policy.ur
@@ -13,7 +13,7 @@ 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
+policy query_policy (SELECT fruit.Weight, fruit.Secret
FROM fruit
WHERE known(fruit.Secret))
@@ -26,7 +26,12 @@ fun fname r =
x <- queryX (SELECT fruit.Weight
FROM fruit
WHERE fruit.Nam = {[r.Nam]}
- AND fruit.Secret = {[r.Secret]})
+ AND fruit.Secret = {[r.Secret]}
+ AND fruit.Weight <> 3.14
+ AND fruit.Weight < 100.0
+ AND fruit.Weight <= 200.1
+ AND fruit.Weight > 1.23
+ AND fruit.Weight >= 1.24)
(fn r => <xml>Weight is {[r.Fruit.Weight]}</xml>);
return <xml><body>
@@ -36,8 +41,7 @@ fun fname r =
fun main () =
x1 <- queryX (SELECT fruit.Id, fruit.Nam
FROM fruit
- WHERE fruit.Nam = "apple"
- AND fruit.Weight = 1.23)
+ WHERE fruit.Nam = "apple")
(fn x => <xml><li>{[x.Fruit.Id]}: {[x.Fruit.Nam]}</li></xml>);
x2 <- queryX (SELECT fruit.Nam, order.Qty
@@ -48,6 +52,7 @@ fun main () =
return <xml><body>
<ul>{x1}</ul>
+
<ul>{x2}</ul>
<form>
generated by cgit v1.2.3 (git 2.39.1) at 2024-11-05 13:59:18 +0000