Skip to content

Commit 866b6d1

Browse files
ssoelvstenssoelvsten
committed
Clean up 'declassifyUtil' into a new module
1 parent 10d6e22 commit 866b6d1

File tree

8 files changed

+128
-122
lines changed

8 files changed

+128
-122
lines changed

‎lib/DeclassifyUtil.trp‎

Lines changed: 110 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,110 @@
1+
import List
2+
3+
let (* Mutually recursive deep declassification of tuples, lists, ... *)
4+
5+
(* Declassification for (most) tuples *)
6+
fun declassify2 ((x,y), a, lev) =
7+
( declassifyDeep (x, a, lev)
8+
, declassifyDeep (y, a, lev))
9+
10+
and declassify3 ((x,y,z), a, lev) =
11+
( declassifyDeep (x, a, lev)
12+
, declassifyDeep (y, a, lev)
13+
, declassifyDeep (z, a, lev))
14+
15+
and declassify4 ((x,y,z,w), a, lev) =
16+
( declassifyDeep (x, a, lev)
17+
, declassifyDeep (y, a, lev)
18+
, declassifyDeep (z, a, lev)
19+
, declassifyDeep (w, a, lev))
20+
21+
and declassify5 ((x1,x2,x3,x4,x5), a, lev) =
22+
( declassifyDeep (x1, a, lev)
23+
, declassifyDeep (x2, a, lev)
24+
, declassifyDeep (x3, a, lev)
25+
, declassifyDeep (x4, a, lev)
26+
, declassifyDeep (x5, a, lev)
27+
)
28+
29+
and declassify6 ((x1,x2,x3,x4,x5,x6), a, lev) =
30+
( declassifyDeep (x1, a, lev)
31+
, declassifyDeep (x2, a, lev)
32+
, declassifyDeep (x3, a, lev)
33+
, declassifyDeep (x4, a, lev)
34+
, declassifyDeep (x5, a, lev)
35+
, declassifyDeep (x6, a, lev)
36+
)
37+
38+
and declassify7 ((x1,x2,x3,x4,x5,x6,x7), a, lev) =
39+
( declassifyDeep (x1, a, lev)
40+
, declassifyDeep (x2, a, lev)
41+
, declassifyDeep (x3, a, lev)
42+
, declassifyDeep (x4, a, lev)
43+
, declassifyDeep (x5, a, lev)
44+
, declassifyDeep (x6, a, lev)
45+
, declassifyDeep (x7, a, lev)
46+
)
47+
48+
and declassify8 ((x1,x2,x3,x4,x5,x6,x7,x8), a, lev) =
49+
( declassifyDeep (x1, a, lev)
50+
, declassifyDeep (x2, a, lev)
51+
, declassifyDeep (x3, a, lev)
52+
, declassifyDeep (x4, a, lev)
53+
, declassifyDeep (x5, a, lev)
54+
, declassifyDeep (x6, a, lev)
55+
, declassifyDeep (x7, a, lev)
56+
, declassifyDeep (x8, a, lev)
57+
)
58+
59+
and declassify9 ((x1,x2,x3,x4,x5,x6,x7,x8,x9), a, lev) =
60+
( declassifyDeep (x1, a, lev)
61+
, declassifyDeep (x2, a, lev)
62+
, declassifyDeep (x3, a, lev)
63+
, declassifyDeep (x4, a, lev)
64+
, declassifyDeep (x5, a, lev)
65+
, declassifyDeep (x6, a, lev)
66+
, declassifyDeep (x7, a, lev)
67+
, declassifyDeep (x8, a, lev)
68+
, declassifyDeep (x9, a, lev)
69+
)
70+
71+
(* Declassification for lists *)
72+
and declassifyList (xs, a, lev) =
73+
List.map (fn x => declassifyDeep (x, a, lev) ) xs
74+
75+
(* TODO: Declassification of records? *)
76+
77+
(** Deep declassification of value `x` to `level` via the given `authority`. *)
78+
and declassifyDeep (x, authority, level) =
79+
let (* Declassify the blocking label before touching the value. *)
80+
val _ = blockdeclto (authority, level)
81+
82+
(* declassification is a 2-step process:
83+
*
84+
* 1. We pattern match on the given value and figure out which function to apply;
85+
* this choice of the function needs to be declassified itself.
86+
*
87+
* 2. We proceed onto the application of the function. *)
88+
val x' = declassify (x, authority, level)
89+
90+
val f = case x' of (_,_) => declassify2
91+
| (_,_,_) => declassify3
92+
| (_,_,_,_) => declassify4
93+
| (_,_,_,_,_) => declassify5
94+
| (_,_,_,_,_,_) => declassify6
95+
| (_,_,_,_,_,_,_) => declassify7
96+
| (_,_,_,_,_,_,_,_) => declassify8
97+
| (_,_,_,_,_,_,_,_,_) => declassify9
98+
| (_::_) => declassifyList
99+
| _ => declassify
100+
101+
in f(x', authority, level)
102+
end
103+
104+
(*--- Module ---*)
105+
val DeclassifyUtil = {
106+
declassifyDeep
107+
}
108+
109+
in [ ("DeclassifyUtil", DeclassifyUtil) ]
110+
end

‎lib/Makefile‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -6,6 +6,7 @@ build:
66
$(COMPILER) ./Number.trp -l
77
$(COMPILER) ./List.trp -l
88
$(COMPILER) ./ListPair.trp -l
9+
$(COMPILER) ./DeclassifyUtil.trp -l
910
$(COMPILER) ./String.trp -l
1011
$(COMPILER) ./Hash.trp -l
1112
$(COMPILER) ./Unit.trp -l
@@ -14,7 +15,6 @@ build:
1415
$(COMPILER) ./HashSet.trp -l
1516
# Old stuff, here be dragons...
1617
$(COMPILER) ./timeout.trp -l
17-
$(COMPILER) ./declassifyutil.trp -l
1818

1919
clean:
2020
rm -rf out

‎lib/README.md‎

Lines changed: 10 additions & 9 deletions
Original file line numberDiff line numberDiff line change
@@ -6,15 +6,16 @@ reviewed rigorously rather than depend on the monitor.
66

77
## Modules
88

9-
- `Hash` : Hash functions for values of all types.
10-
- `HashMap` : Map from keys to values via their hash.
11-
- `HashSet` : Set of elements via their hash.
12-
- `List` : Operations for lists, i.e. `[]` and `x::xs`.
13-
- `ListPair` : Operations for list of pairs, i.e. `(x,y)::xs`.
14-
- `Number` : Operations for numbers, i.e. integer and floats.
15-
- `StencilVector` : Memory-efficient implementation of small (sparse) arrays.
16-
- `String` : Operations for strings
17-
- `Unit` : Unit testing.
9+
- `DeclassifyUtil` : Helper functions for declassification.
10+
- `Hash` : Hash functions for values of all types.
11+
- `HashMap` : Map from keys to values via their hash.
12+
- `HashSet` : Set of elements via their hash.
13+
- `List` : Operations for lists, i.e. `[]` and `x::xs`.
14+
- `ListPair` : Operations for list of pairs, i.e. `(x,y)::xs`.
15+
- `Number` : Operations for numbers, i.e. integer and floats.
16+
- `StencilVector` : Memory-efficient implementation of small (sparse) arrays.
17+
- `String` : Operations for strings
18+
- `Unit` : Unit testing.
1819

1920
## How to add a new file
2021

‎lib/declassifyutil.trp‎

Lines changed: 0 additions & 102 deletions
This file was deleted.

‎tests/rt/neg/ifc/pini_d.trp‎

Lines changed: 4 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,5 @@
1-
import declassifyutil
1+
import DeclassifyUtil
2+
23
(* testing various corner cases of declassification *)
34
let val secretAlice = 1 raisedTo `<alice;#root-integrity>`
45
val secretBob = 1 raisedTo `<bob;#root-integrity>`
@@ -9,8 +10,8 @@ let val secretAlice = 1 raisedTo `<alice;#root-integrity>`
910
val (a,b) = if secretAlice > 0 then (1,2) else (3,4)
1011
val (x,y) = if secretBob > 0 then (5,6) else (7,8)
1112
val _ = blockdecl authority
12-
val (a1, b1) = declassifydeep ( (a,b), aliceAuth, `{}` )
13+
val (a1, b1) = DeclassifyUtil.declassifyDeep ( (a,b), aliceAuth, `{}` )
1314
val _ = if secretBob > secretAlice then () else ()
1415
in
1516
adv a1
16-
end
17+
end

‎tests/rt/pos/ifc/decl2.trp‎

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -1,10 +1,10 @@
1-
import declassifyutil
1+
import DeclassifyUtil
22
import List
33

44
let val x = 42 raisedTo `<alice&bob;#root-integrity>`
55
val y = 100 raisedTo `<alice&bob;#root-integrity>`
66
val tuple = (x,y,10)
77
val ls = List.map (fn x => x) [x,y,10]
8-
val z = declassifydeep (ls, authority, `{}`)
8+
val z = DeclassifyUtil.declassifyDeep (ls, authority, `{}`)
99
in z
1010
end

‎tests/rt/pos/ifc/pini.trp‎

Lines changed: 1 addition & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -1,5 +1,3 @@
1-
import declassifyutil
2-
31
let val secret = 1 raisedTo `<alice;#root-integrity>`
42
val aliceAuth = attenuate (authority, `<alice;#root-integrity>`)
53
(* val t = if secret > 0 then (1,2) else (3,4) *)
@@ -8,4 +6,4 @@ let val secret = 1 raisedTo `<alice;#root-integrity>`
86
val _ = pinipop c
97
in
108
adv 0
11-
end
9+
end

‎tests/rt/pos/ifc/tuples03.trp‎

Lines changed: 0 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -1,5 +1,3 @@
1-
import declassifyutil
2-
31
let val x = 42 raisedTo `<alice&bob;#root-integrity>`
42
val y = 100 raisedTo `<alice&bob;#root-integrity>`
53

0 commit comments

Comments
 (0)