pkcs7.bend

bend-osdev-pkcs7@0.1.0.0 · 86 lines · 11 definitions

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.
5import Base
6import bend-osdev-bytes@0.1.1.0/bytes.bend as B
7import bend-osdev-mode-core@0.1.0.0/mode_core.bend as M
8
9# n bytes of value v
10def 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
17def 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)
23def 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
27def 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
35def 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
43def 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
51def pkcs7.last(m: Maybe<&2, U32>, d: U32) -> U32:
52  match m:
53    case Some{b}:
54      b
55    case None{}:
56      d
57
58def 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)
67def 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
73def 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
85def Pkcs7.unpad(+bs: Nat, m: B.Octets) -> Result<&2, &2, M.CmError, B.Octets>:
86  Pkcs7.unpad.go(pkcs7.size_ok(bs), bs, m)