mode_core.bend

bend-osdev-mode-core@0.1.0.0 · 310 lines · 51 definitions

1# bend-osdev-mode-core: what the block-cipher modes of operation over any
2# 128-bit block cipher share (bend-osdev-cbc, -xts, -ccm, -cmac, -pkcs7,
3# and the ciphers that plug into them). This file holds it: the 128-bit block, the
4# package's error type, and the byte-level helpers the modes are built from.
5#
6# The block cipher is a parameter. Every mode takes it as template arguments:
7#   ~K: Data                          the cipher's key (an expanded key schedule)
8#   ~enc: K -> CmBlock -> CmBlock     encryption of one block
9#   ~dec: K -> CmBlock -> CmBlock     decryption of one block (CBC, XTS only)
10# and the key itself as +k: K. The modes never look inside K, so they run on
11# any cipher with 128-bit blocks; aes.bend supplies AES-128 and AES-256.
12#
13# A CmBlock is four 32-bit words, big-endian: w0 holds bytes 0 to 3 of the
14# block, byte 0 in its top 8 bits. Every value of the type is a block (there is
15# no out-of-range byte), so a cipher's "decryption inverts encryption" can be
16# stated for every block. The type is open: a cipher adapter may build and
17# match blocks directly.
18import Base
19import bend-osdev-bytes@0.1.1.0/bytes.bend as B
20import bend-osdev-word64@0.1.1.0/word64.bend as W
21
22type CmBlock is Data:
23  CmBlock{w0: U32, w1: U32, w2: U32, w3: U32}
24
25# Every failure a mode can report
26type CmError is Data:
27  CmBadKeyLength{got: Nat}
28  CmBadIvLength{got: Nat}
29  CmBadTweakLength{got: Nat}
30  CmBadNonceLength{got: Nat}
31  CmBadTagLength{got: Nat}
32  CmBadBlockSize{got: Nat}
33  CmNotBlockMultiple{len: Nat}
34  CmTooShort{len: Nat}
35  CmTooLong{len: Nat}
36  CmBadPadding{}
37  CmTagMismatch{}
38
39# Blocks
40
41def CmBlock.zero() -> CmBlock:
42  CmBlock{0, 0, 0, 0}
43
44def CmBlock.xor(a: CmBlock, b: CmBlock) -> CmBlock:
45  match a b:
46    case CmBlock{a0, a1, a2, a3} CmBlock{b0, b1, b2, b3}:
47      CmBlock{U32.xor(a0, b0), U32.xor(a1, b1), U32.xor(a2, b2), U32.xor(a3, b3)}
48
49# Each block of xs encrypted under k and decrypted again: xs itself for
50# every list exactly where decryption undoes encryption at k, which is how
51# the round-trip laws (LAWS.bend) take that property of the cipher
52def CmBlock.dec_enc(~K: Data, ~enc: K -> CmBlock -> CmBlock, ~dec: K -> CmBlock -> CmBlock, +k: K, xs: List<&2, CmBlock>) -> List<&2, CmBlock>:
53  match xs:
54    case Nil{}:
55      Nil{}
56    case Con{x, t}:
57      Con{dec(k, enc(k, x)), CmBlock.dec_enc(~K, ~enc, ~dec, k, t)}
58
59# Bytes and words (internal). Words are split into bytes and joined back by
60# bit slicing (bend-osdev-word64's W64.bits), not by shifts and masks, so that
61# the round trips can be proved for every word.
62
63# a byte (the low 8 bits of x), as bend-osdev-bytes masks it
64def cm.byte(x: U32) -> U32:
65  B.byte(x)
66
67def cm.bits8(b: U32) -> Word(8n):
68  match b:
69    case U32{w}:
70      W.W64.bits.lo(8n, 24n, w)
71
72def cm.of8(s: Word(8n)) -> U32:
73  U32{W.W64.bits.cat(8n, 24n, s, Word.zero(24n))}
74
75# the word with bytes a, b, c, d, most significant first
76def cm.word(a: U32, b: U32, c: U32, d: U32) -> U32:
77  U32{W.W64.bits.cat(8n, 24n, cm.bits8(d), W.W64.bits.cat(8n, 16n, cm.bits8(c), W.W64.bits.cat(8n, 8n, cm.bits8(b), cm.bits8(a))))}
78
79# the bytes of w, most significant first
80def cm.b0(w: U32) -> U32:
81  match w:
82    case U32{x}:
83      cm.of8(W.W64.bits.hi(8n, 8n, W.W64.bits.hi(8n, 16n, W.W64.bits.hi(8n, 24n, x))))
84
85def cm.b1(w: U32) -> U32:
86  match w:
87    case U32{x}:
88      cm.of8(W.W64.bits.lo(8n, 8n, W.W64.bits.hi(8n, 16n, W.W64.bits.hi(8n, 24n, x))))
89
90def cm.b2(w: U32) -> U32:
91  match w:
92    case U32{x}:
93      cm.of8(W.W64.bits.lo(8n, 16n, W.W64.bits.hi(8n, 24n, x)))
94
95def cm.b3(w: U32) -> U32:
96  match w:
97    case U32{x}:
98      cm.of8(W.W64.bits.lo(8n, 24n, x))
99
100# the four bytes of w, most significant first, in front of rest
101def cm.unword(+w: U32, rest: List<&2, U32>) -> List<&2, U32>:
102  Con{cm.b0(w), Con{cm.b1(w), Con{cm.b2(w), Con{cm.b3(w), rest}}}}
103
104def cm.w0(b: CmBlock) -> U32:
105  match b:
106    case CmBlock{w0, w1, w2, w3}:
107      w0
108
109def cm.w1(b: CmBlock) -> U32:
110  match b:
111    case CmBlock{w0, w1, w2, w3}:
112      w1
113
114def cm.w2(b: CmBlock) -> U32:
115  match b:
116    case CmBlock{w0, w1, w2, w3}:
117      w2
118
119def cm.w3(b: CmBlock) -> U32:
120  match b:
121    case CmBlock{w0, w1, w2, w3}:
122      w3
123
124# the 16 bytes of a block in front of rest (always 16 cells, whatever b is)
125def cm.bytes_onto(+b: CmBlock, rest: List<&2, U32>) -> List<&2, U32>:
126  cm.unword(cm.w0(b), cm.unword(cm.w1(b), cm.unword(cm.w2(b), cm.unword(cm.w3(b), rest))))
127
128def cm.bytes_of(b: CmBlock) -> List<&2, U32>:
129  cm.bytes_onto(b, Nil{})
130
131def cm.block16(a0: U32, a1: U32, a2: U32, a3: U32, a4: U32, a5: U32, a6: U32, a7: U32, a8: U32, a9: U32, a10: U32, a11: U32, a12: U32, a13: U32, a14: U32, a15: U32) -> CmBlock:
132  CmBlock{cm.word(a0, a1, a2, a3), cm.word(a4, a5, a6, a7), cm.word(a8, a9, a10, a11), cm.word(a12, a13, a14, a15)}
133
134def cm.block_of.full(xs: List<&2, U32>) -> CmBlock:
135  match xs:
136    case Con{a0, Con{a1, Con{a2, Con{a3, Con{a4, Con{a5, Con{a6, Con{a7, Con{a8, Con{a9, Con{a10, Con{a11, Con{a12, Con{a13, Con{a14, Con{a15, t}}}}}}}}}}}}}}}}:
137      cm.block16(a0, a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a11, a12, a13, a14, a15)
138    case _:
139      CmBlock.zero()
140
141# the block of the first 16 bytes of xs, zero-filled if xs is shorter
142def cm.block_of(xs: List<&2, U32>) -> CmBlock:
143  cm.block_of.full(B.append(B.take(16n, xs), B.zeros(16n)))
144
145# A byte string as its whole blocks and the 0 to 15 bytes after them
146type CmSplit is Data:
147  CmSplit{blocks: List<&2, CmBlock>, tail: List<&2, U32>}
148
149def cm.split.cons(b: CmBlock, s: CmSplit) -> CmSplit:
150  match s:
151    case CmSplit{bs, t}:
152      CmSplit{Con{b, bs}, t}
153
154def cm.split(+xs: List<&2, U32>) -> CmSplit:
155  match xs:
156    case Con{a0, Con{a1, Con{a2, Con{a3, Con{a4, Con{a5, Con{a6, Con{a7, Con{a8, Con{a9, Con{a10, Con{a11, Con{a12, Con{a13, Con{a14, Con{a15, t}}}}}}}}}}}}}}}}:
157      cm.split.cons(cm.block16(a0, a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a11, a12, a13, a14, a15), cm.split(t))
158    case _:
159      CmSplit{Nil{}, xs}
160
161def cm.split.blocks(s: CmSplit) -> List<&2, CmBlock>:
162  match s:
163    case CmSplit{bs, t}:
164      bs
165
166def cm.split.tail(s: CmSplit) -> List<&2, U32>:
167  match s:
168    case CmSplit{bs, t}:
169      t
170
171# the bytes of the blocks bs, in front of rest
172def cm.join_onto(bs: List<&2, CmBlock>, rest: List<&2, U32>) -> List<&2, U32>:
173  match bs:
174    case Nil{}:
175      rest
176    case Con{b, t}:
177      cm.bytes_onto(b, cm.join_onto(t, rest))
178
179def cm.join(bs: List<&2, CmBlock>) -> List<&2, U32>:
180  cm.join_onto(bs, Nil{})
181
182# byte-wise XOR, as long as the shorter list
183def cm.xor_bytes(xs: List<&2, U32>, ys: List<&2, U32>) -> List<&2, U32>:
184  match xs ys:
185    case Con{a, s} Con{b, t}:
186      Con{cm.byte(U32.xor(a, b)), cm.xor_bytes(s, t)}
187    case _ _:
188      Nil{}
189
190# the OR of the byte-wise XORs: 0 exactly when the lists agree, computed
191# without stopping at the first difference
192# The same, tail-recursive. Bend 2.0.37's runtime overflows its stack at some
193# tens of thousands of nested non-tail calls, so the structural forms above,
194# which the proofs reason about, cannot run on long messages; the modes run
195# these instead, and PROOF.bend proves each equal to its structural form for
196# every input.
197
198# the blocks of bs in reverse order, in front of acc
199def cm.blocks.rev_onto(bs: List<&2, CmBlock>, acc: List<&2, CmBlock>) -> List<&2, CmBlock>:
200  match bs:
201    case Nil{}:
202      acc
203    case Con{b, t}:
204      cm.blocks.rev_onto(t, Con{b, acc})
205
206def cm.blocks.len.go(bs: List<&2, CmBlock>, n: Nat) -> Nat:
207  match bs:
208    case Nil{}:
209      n
210    case Con{b, t}:
211      cm.blocks.len.go(t, 1n+n)
212
213# the number of blocks (List.length)
214def cm.blocks.len(bs: List<&2, CmBlock>) -> Nat:
215  cm.blocks.len.go(bs, 0n)
216
217# xs, then ys (List.append)
218def cm.blocks.append(xs: List<&2, CmBlock>, ys: List<&2, CmBlock>) -> List<&2, CmBlock>:
219  cm.blocks.rev_onto(cm.blocks.rev_onto(xs, Nil{}), ys)
220
221# the blocks split so far are kept reversed in acc (cm.split)
222def cm.split.go(+xs: List<&2, U32>, acc: List<&2, CmBlock>) -> CmSplit:
223  match xs:
224    case Con{a0, Con{a1, Con{a2, Con{a3, Con{a4, Con{a5, Con{a6, Con{a7, Con{a8, Con{a9, Con{a10, Con{a11, Con{a12, Con{a13, Con{a14, Con{a15, t}}}}}}}}}}}}}}}}:
225      cm.split.go(t, Con{cm.block16(a0, a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a11, a12, a13, a14, a15), acc})
226    case _:
227      CmSplit{cm.blocks.rev_onto(acc, Nil{}), xs}
228
229def cm.split.fast(+xs: List<&2, U32>) -> CmSplit:
230  cm.split.go(xs, Nil{})
231
232# the bytes of the blocks rs (last first) in front of acc
233def cm.join.go(rs: List<&2, CmBlock>, acc: List<&2, U32>) -> List<&2, U32>:
234  match rs:
235    case Nil{}:
236      acc
237    case Con{b, t}:
238      cm.join.go(t, cm.bytes_onto(b, acc))
239
240# cm.join_onto
241def cm.join_onto.fast(bs: List<&2, CmBlock>, rest: List<&2, U32>) -> List<&2, U32>:
242  cm.join.go(cm.blocks.rev_onto(bs, Nil{}), rest)
243
244def cm.xor_bytes.go(xs: List<&2, U32>, ys: List<&2, U32>, acc: List<&2, U32>) -> List<&2, U32>:
245  match xs ys:
246    case Con{a, s} Con{b, t}:
247      cm.xor_bytes.go(s, t, Con{cm.byte(U32.xor(a, b)), acc})
248    case _ _:
249      B.rev(acc)
250
251# cm.xor_bytes
252def cm.xor_bytes.fast(xs: List<&2, U32>, ys: List<&2, U32>) -> List<&2, U32>:
253  cm.xor_bytes.go(xs, ys, Nil{})
254
255def cm.diff(xs: List<&2, U32>, ys: List<&2, U32>, acc: U32) -> U32:
256  match xs ys:
257    case Con{a, s} Con{b, t}:
258      cm.diff(s, t, U32.or(acc, cm.byte(U32.xor(a, b))))
259    case Nil{} Nil{}:
260      acc
261    case _ _:
262      1
263
264# equality of two byte lists with no early exit of the same length (a tag check)
265def cm.ct_eq(xs: List<&2, U32>, ys: List<&2, U32>) -> Bool:
266  U32.is_eq(cm.diff(xs, ys, 0), 0)
267
268# 0 for a 0 bit, all ones for a 1 bit (the low bit of b)
269def cm.mask(b: U32) -> U32:
270  U32.sub(0, U32.and(1, b))
271
272# Checks, as steps of a Result block
273
274def cm.check(ok: Bool, e: CmError) -> Result<&2, &2, CmError, Unit>:
275  match ok:
276    case True{}:
277      Done{Unit{}}
278    case False{}:
279      Fail{e}
280
281# a 16-byte value as a block, or the error e
282def cm.need_block.pick(ok: Bool, xs: List<&2, U32>, e: CmError) -> Result<&2, &2, CmError, CmBlock>:
283  match ok:
284    case True{}:
285      Done{cm.block_of(xs)}
286    case False{}:
287      Fail{e}
288
289def cm.need_block(+xs: List<&2, U32>, e: CmError) -> Result<&2, &2, CmError, CmBlock>:
290  cm.need_block.pick(Nat.is_eq(B.len(xs), 16n), xs, e)
291
292# Blocks as byte strings
293
294def CmBlock.to_octets(b: CmBlock) -> B.Octets:
295  B.Octets.of_list(cm.bytes_of(b))
296
297def CmBlock.of_octets.pick(ok: Bool, xs: List<&2, U32>) -> Maybe<&2, CmBlock>:
298  match ok:
299    case True{}:
300      Some{cm.block_of(xs)}
301    case False{}:
302      None{}
303
304# a 16-byte string as a block; None for any other length
305def CmBlock.of_octets(o: B.Octets) -> Maybe<&2, CmBlock>:
306  +xs = B.Octets.to_list(o)
307  CmBlock.of_octets.pick(Nat.is_eq(B.len(xs), 16n), xs)
308
309def CmBlock.hex(b: CmBlock) -> String:
310  B.hex(cm.bytes_of(b))