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.
7	import Base
8	
9	type AaPerms is Data:
10	  AaPerms{bits: List<&2, Bool>}
11	
12	# Operations on the bit lists
13	
14	def 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
24	def 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
34	def 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
42	def 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
52	def 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
62	def 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	
69	def 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	
82	def AaPerms.none() -> AaPerms:
83	  AaPerms{Nil{}}
84	
85	def AaPerms.bit(i: Nat) -> AaPerms:
86	  AaPerms{AaBits.bit(i)}
87	
88	def AaPerms.of_bits(bs: List<&2, Bool>) -> AaPerms:
89	  AaPerms{bs}
90	
91	def AaPerms.bits(p: AaPerms) -> List<&2, Bool>:
92	  match p:
93	    case AaPerms{bs}:
94	      bs
95	
96	def AaPerms.union(a: AaPerms, b: AaPerms) -> AaPerms:
97	  match a b:
98	    case AaPerms{x} AaPerms{y}:
99	      AaPerms{AaBits.or(x, y)}
100	
101	def AaPerms.minus(a: AaPerms, b: AaPerms) -> AaPerms:
102	  match a b:
103	    case AaPerms{x} AaPerms{y}:
104	      AaPerms{AaBits.minus(x, y)}
105	
106	def AaPerms.any(a: AaPerms) -> Bool:
107	  match a:
108	    case AaPerms{x}:
109	      AaBits.any(x)
110	
111	def AaPerms.covers(a: AaPerms, r: AaPerms) -> Bool:
112	  match a r:
113	    case AaPerms{x} AaPerms{y}:
114	      AaBits.covers(x, y)
115	
116	def AaPerms.meets(a: AaPerms, b: AaPerms) -> Bool:
117	  match a b:
118	    case AaPerms{x} AaPerms{y}:
119	      AaBits.meets(x, y)
120	
121	def AaPerms.has(a: AaPerms, i: Nat) -> Bool:
122	  match a:
123	    case AaPerms{x}:
124	      AaBits.has(x, i)
125	
126	def 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
130	def 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	
141	def 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	
146	type AaQual is Data:
147	  AaQual{audit: Bool, deny: Bool, owner: Bool}
148	
149	def AaQual.none() -> AaQual:
150	  AaQual{False{}, False{}, False{}}
151	
152	def AaQual.audit(q: AaQual) -> Bool:
153	  match q:
154	    case AaQual{a, d, o}:
155	      a
156	
157	def AaQual.deny(q: AaQual) -> Bool:
158	  match q:
159	    case AaQual{a, d, o}:
160	      d
161	
162	def 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	
170	type AaGrant is Data:
171	  AaGrant{audit: Bool, deny: Bool, perms: AaPerms}
172	
173	def AaGrant.of(q: AaQual, p: AaPerms) -> AaGrant:
174	  match q:
175	    case AaQual{a, d, o}:
176	      AaGrant{a, d, p}
177	
178	def 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)}