1	# PKCS #7 padding (RFC 5652, section 6.3): a message is padded to a whole
2	# number of blocks by appending p bytes of value p, 1 <= p <= the block size,
3	# so a message that already fills its blocks gains a whole block of padding.
4	# The block size is a parameter (1 to 255); CBC uses 16.
5	import Base
6	import bend-osdev-bytes@0.1.1.0/bytes.bend as B
7	import bend-osdev-mode-core@0.1.0.0/mode_core.bend as M
8	
9	# n bytes of value v
10	def pkcs7.fill(n: Nat, +v: U32) -> List<&2, U32>:
11	  match n:
12	    case 0n:
13	      Nil{}
14	    case 1n+p:
15	      Con{v, pkcs7.fill(p, v)}
16	
17	def pkcs7.size_ok(+bs: Nat) -> Bool:
18	  Bool.and(Nat.is_lt(0n, bs), Nat.is_lt(bs, 256n))
19	
20	# m and its padding (on Octets, so that a long message is not walked as a
21	# list: Bend 2.0.37's runtime overflows its stack on deep structural
22	# recursion)
23	def pkcs7.pad.oct(+bs: Nat, +m: B.Octets) -> B.Octets:
24	  +p = Nat.sub(bs, Nat.mod(B.Octets.len(m), bs))
25	  B.Octets.append(m, B.Octets.of_list(pkcs7.fill(p, U32.from_nat(p))))
26	
27	def Pkcs7.pad.go(ok: Bool, +bs: Nat, m: B.Octets) -> Result<&2, &2, M.CmError, B.Octets>:
28	  match ok:
29	    case True{}:
30	      Done{pkcs7.pad.oct(bs, m)}
31	    case False{}:
32	      Fail{M.CmBadBlockSize{bs}}
33	
34	# m padded to a whole number of bs-byte blocks
35	def Pkcs7.pad(+bs: Nat, m: B.Octets) -> Result<&2, &2, M.CmError, B.Octets>:
36	  Pkcs7.pad.go(pkcs7.size_ok(bs), bs, m)
37	
38	# Unpadding. The checks do not stop at the first bad byte, but the result
39	# (padding good or bad) is visible to the caller: see the README on padding
40	# oracles.
41	
42	# 0 when every byte of xs is v
43	def pkcs7.diff(xs: List<&2, U32>, +v: U32, acc: U32) -> U32:
44	  match xs:
45	    case Nil{}:
46	      acc
47	    case Con{h, t}:
48	      pkcs7.diff(t, v, U32.or(acc, U32.xor(M.cm.byte(h), v)))
49	
50	# the last byte, or d if there is none
51	def pkcs7.last(m: Maybe<&2, U32>, d: U32) -> U32:
52	  match m:
53	    case Some{b}:
54	      b
55	    case None{}:
56	      d
57	
58	def pkcs7.strip(ok: Bool, +n: Nat, +p: Nat, m: B.Octets) -> Result<&2, &2, M.CmError, B.Octets>:
59	  match ok:
60	    case True{}:
61	      Done{B.Octets.take(Nat.sub(n, p), m)}
62	    case False{}:
63	      Fail{M.CmBadPadding{}}
64	
65	# the value p of the last byte must be 1 to bs, and the last p bytes all p
66	# (on Octets of n bytes, so that only those p bytes become a list)
67	def pkcs7.unpad.oct(+bs: Nat, +m: B.Octets, +n: Nat) -> Result<&2, &2, M.CmError, B.Octets>:
68	  +v = pkcs7.last(B.Octets.at(m, Nat.sub(n, 1n)), 0)
69	  +p = U32.to_nat(v)
70	  +good = Bool.and(Nat.is_lt(0n, p), Bool.and(Nat.is_le(p, bs), U32.is_eq(pkcs7.diff(B.Octets.to_list(B.Octets.drop(Nat.sub(n, p), m)), v, 0), 0)))
71	  pkcs7.strip(good, n, p, m)
72	
73	def Pkcs7.unpad.go(ok: Bool, +bs: Nat, +m: B.Octets) -> Result<&2, &2, M.CmError, B.Octets>:
74	  match ok:
75	    case True{}:
76	      +n = B.Octets.len(m)
77	      do Result<&2, &2, M.CmError, B.Octets>:
78	        M.cm.check(Nat.is_lt(0n, n), M.CmTooShort{n})
79	        M.cm.check(Nat.is_eq(Nat.mod(n, bs), 0n), M.CmNotBlockMultiple{n})
80	        pkcs7.unpad.oct(bs, m, n)
81	    case False{}:
82	      Fail{M.CmBadBlockSize{bs}}
83	
84	# m without its padding; m must be a non-empty whole number of blocks
85	def Pkcs7.unpad(+bs: Nat, m: B.Octets) -> Result<&2, &2, M.CmError, B.Octets>:
86	  Pkcs7.unpad.go(pkcs7.size_ok(bs), bs, m)