perm.bend

bend-osdev-apparmor@0.1.0.0 · 183 lines · 29 definitions

1# bend-osdev-apparmor: permission sets, rule qualifiers, and the grants a
2# matching rule contributes.
3#
4# An AaPerms is a set of permissions of one rule kind, as a list of bits: bit
5# i is permission i of that kind (file: r w a l k m x; signal: send receive;
6# ...). A missing bit is clear, so sets of different lengths combine.
7import Base
8
9type AaPerms is Data:
10  AaPerms{bits: List<&2, Bool>}
11
12# Operations on the bit lists
13
14def AaBits.or(a: List<&2, Bool>, b: List<&2, Bool>) -> List<&2, Bool>:
15  match a b:
16    case Nil{} _:
17      b
18    case Con{x, xs} Nil{}:
19      Con{x, xs}
20    case Con{x, xs} Con{y, ys}:
21      Con{Bool.or(x, y), AaBits.or(xs, ys)}
22
23# a without b
24def AaBits.minus(a: List<&2, Bool>, b: List<&2, Bool>) -> List<&2, Bool>:
25  match a b:
26    case Nil{} _:
27      Nil{}
28    case Con{x, xs} Nil{}:
29      Con{x, xs}
30    case Con{x, xs} Con{y, ys}:
31      Con{Bool.and(x, Bool.not(y)), AaBits.minus(xs, ys)}
32
33# some bit is set
34def AaBits.any(a: List<&2, Bool>) -> Bool:
35  match a:
36    case Nil{}:
37      False{}
38    case Con{x, xs}:
39      Bool.or(x, AaBits.any(xs))
40
41# every bit of r is in a
42def AaBits.covers(a: List<&2, Bool>, r: List<&2, Bool>) -> Bool:
43  match a r:
44    case _ Nil{}:
45      True{}
46    case Nil{} Con{y, ys}:
47      Bool.not(AaBits.any(Con{y, ys}))
48    case Con{x, xs} Con{y, ys}:
49      Bool.and(Bool.or(x, Bool.not(y)), AaBits.covers(xs, ys))
50
51# some bit is in both
52def AaBits.meets(a: List<&2, Bool>, b: List<&2, Bool>) -> Bool:
53  match a b:
54    case Nil{} _:
55      False{}
56    case Con{x, xs} Nil{}:
57      False{}
58    case Con{x, xs} Con{y, ys}:
59      Bool.or(Bool.and(x, y), AaBits.meets(xs, ys))
60
61# bit i alone
62def AaBits.bit(i: Nat) -> List<&2, Bool>:
63  match i:
64    case 0n:
65      [True{}]
66    case 1n+j:
67      Con{False{}, AaBits.bit(j)}
68
69def AaBits.has(a: List<&2, Bool>, i: Nat) -> Bool:
70  match a:
71    case Nil{}:
72      False{}
73    case Con{x, xs}:
74      match i:
75        case 0n:
76          x
77        case 1n+j:
78          AaBits.has(xs, j)
79
80# The set type
81
82def AaPerms.none() -> AaPerms:
83  AaPerms{Nil{}}
84
85def AaPerms.bit(i: Nat) -> AaPerms:
86  AaPerms{AaBits.bit(i)}
87
88def AaPerms.of_bits(bs: List<&2, Bool>) -> AaPerms:
89  AaPerms{bs}
90
91def AaPerms.bits(p: AaPerms) -> List<&2, Bool>:
92  match p:
93    case AaPerms{bs}:
94      bs
95
96def AaPerms.union(a: AaPerms, b: AaPerms) -> AaPerms:
97  match a b:
98    case AaPerms{x} AaPerms{y}:
99      AaPerms{AaBits.or(x, y)}
100
101def AaPerms.minus(a: AaPerms, b: AaPerms) -> AaPerms:
102  match a b:
103    case AaPerms{x} AaPerms{y}:
104      AaPerms{AaBits.minus(x, y)}
105
106def AaPerms.any(a: AaPerms) -> Bool:
107  match a:
108    case AaPerms{x}:
109      AaBits.any(x)
110
111def AaPerms.covers(a: AaPerms, r: AaPerms) -> Bool:
112  match a r:
113    case AaPerms{x} AaPerms{y}:
114      AaBits.covers(x, y)
115
116def AaPerms.meets(a: AaPerms, b: AaPerms) -> Bool:
117  match a b:
118    case AaPerms{x} AaPerms{y}:
119      AaBits.meets(x, y)
120
121def AaPerms.has(a: AaPerms, i: Nat) -> Bool:
122  match a:
123    case AaPerms{x}:
124      AaBits.has(x, i)
125
126def AaPerms.add(a: AaPerms, i: Nat) -> AaPerms:
127  AaPerms.union(a, AaPerms.bit(i))
128
129# the permissions as text: the letter of each set bit, in order
130def AaPerms.show.go(bs: List<&2, Bool>, ls: List<&2, String>) -> String:
131  match bs:
132    case Nil{}:
133      ""
134    case Con{b, rest}:
135      match ls:
136        case Nil{}:
137          ""
138        case Con{l, more}:
139          String.append(Bool.pick(String, b, l, ""), AaPerms.show.go(rest, more))
140
141def AaPerms.show(p: AaPerms, letters: List<&2, String>) -> String:
142  AaPerms.show.go(AaPerms.bits(p), letters)
143
144# Rule qualifiers: audit, deny (allow is the default) and owner
145
146type AaQual is Data:
147  AaQual{audit: Bool, deny: Bool, owner: Bool}
148
149def AaQual.none() -> AaQual:
150  AaQual{False{}, False{}, False{}}
151
152def AaQual.audit(q: AaQual) -> Bool:
153  match q:
154    case AaQual{a, d, o}:
155      a
156
157def AaQual.deny(q: AaQual) -> Bool:
158  match q:
159    case AaQual{a, d, o}:
160      d
161
162def AaQual.owner(q: AaQual) -> Bool:
163  match q:
164    case AaQual{a, d, o}:
165      o
166
167# What a rule that matches a request contributes: its permissions, allowed or
168# denied, audited or not
169
170type AaGrant is Data:
171  AaGrant{audit: Bool, deny: Bool, perms: AaPerms}
172
173def AaGrant.of(q: AaQual, p: AaPerms) -> AaGrant:
174  match q:
175    case AaQual{a, d, o}:
176      AaGrant{a, d, p}
177
178def AaGrant.append(xs: List<&2, AaGrant>, ys: List<&2, AaGrant>) -> List<&2, AaGrant>:
179  match xs:
180    case Nil{}:
181      ys
182    case Con{h, t}:
183      Con{h, AaGrant.append(t, ys)}