archive.bend

bend-kit-archive@0.5.1.0 · 373 lines · 56 definitions

1# ZIP archives read over Bytes: stored and DEFLATE entries, checked against their CRC-32 and sizes. Source: https://github.com/paymog/bend-kit/tree/main/archive
2import Base
3import bend-kit-bytes@0.3.3.0/bytes.bend as Bytes
4import bend-kit-zlib@0.5.1.0/zlib.bend as Zlib
5import bend-kit-hash@0.3.0.2/hash.bend as Hash
6
7# One member: its name and contents as raw bytes, its method (0 stored, 8 DEFLATE), and its CRC-32.
8type Entry is Type:
9  Entry{name: Bytes.Bytes, data: Bytes.Bytes, method: U32, crc: U32}
10
11# A checked central directory entry. name and data are byte offsets into the input;
12# packed is the stored or compressed length, size the length after decoding.
13type Header is Data:
14  Header{name: U32, name_len: U32, method: U32, crc: U32, packed: U32, size: U32, data: U32}
15
16# The methods read: 0 (stored) and 8 (DEFLATE).
17def supported(+method: U32) -> Bool:
18  Bool.or(U32.is_eq(method, 0), U32.is_eq(method, 8))
19
20def crc.bytes(b: Bytes.Bytes) -> Bytes.Bytes & U32:
21  Hash.crc32(b)
22
23def crc.value(r: Bytes.Bytes & U32) -> U32:
24  (b, crc) = r
25  crc
26
27def crc32(b: Bytes.Bytes) -> U32:
28  crc.value(crc.bytes(b))
29
30# n bytes from i as a list. Callers keep i + n within the buffer.
31def grab.go(k: Nat, r: Array<U32> & U32, +j: U32, acc: List<&2, U32>) -> Array<U32> & List<&2, U32>:
32  match k:
33    case 0n:
34      (a, v) = r
35      (a, acc)
36    case 1n+p:
37      (a, +v) = r
38      grab.go(p, Bytes.peek(a, (j - 1 : U32)), (j - 1 : U32), Con{v, acc})
39
40def grab(a: Array<U32>, +i: U32, +n: U32) -> Array<U32> & List<&2, U32>:
41  +j = (i + n - 1 : U32)
42  grab.go(U32.to_nat(n), Bytes.peek(a, j), j, Nil{})
43
44def at(xs: List<&2, U32>, +i: U32) -> U32:
45  match xs:
46    case Nil{}:
47      0
48    case Con{h, t}:
49      Bool.pick(U32, U32.is_zero(i), h, at(t, (i - 1 : U32)))
50
51# Little-endian fields of a grabbed record.
52def u16(+xs: List<&2, U32>, +o: U32) -> U32:
53  (at(xs, o) .|. (at(xs, (o + 1 : U32)) << 8n) : U32)
54
55def u32(+xs: List<&2, U32>, +o: U32) -> U32:
56  (u16(xs, o) .|. (u16(xs, (o + 2 : U32)) << 16n) : U32)
57
58# The first failed check's message, outermost first.
59def why(+ok: Bool, +msg: String, +rest: Maybe<&2, String>) -> Maybe<&2, String>:
60  Bool.pick(Maybe<&2, String>, ok, rest, Some{msg})
61
62# General purpose flags: encrypted (bit 0), strong encryption (bit 6), masked headers (bit 13).
63def encrypted(+flags: U32) -> Bool:
64  Bool.not(U32.is_zero((flags .&. 8257 : U32)))
65
66# Do n bytes at x and at y match? r holds the previous byte's answer.
67def same.at3(r: Array<U32> & U32, +u: U32) -> Array<U32> & Bool:
68  (a, +v) = r
69  (a, U32.is_eq(u, v))
70
71def same.at2(r: Array<U32> & U32, +y: U32) -> Array<U32> & Bool:
72  (a, +u) = r
73  same.at3(Bytes.peek(a, y), u)
74
75def same.go(n: Nat, r: Array<U32> & Bool, +x: U32, +y: U32) -> Array<U32> & Bool:
76  match n:
77    case 0n:
78      r
79    case 1n+q:
80      (a, ok) = r
81      match ok:
82        case False{}:
83          (a, False{})
84        case True{}:
85          same.go(q, same.at2(Bytes.peek(a, x), y), (x + 1 : U32), (y + 1 : U32))
86
87# End of central directory (APPNOTE 4.3.16): the last signature whose comment length reaches the end exactly.
88def eocd.of(r: Array<U32> & List<&2, U32>, +len: U32, +p: U32) -> Array<U32> & Bool:
89  (a, +x) = r
90  (a, Bool.and(U32.is_eq(u32(x, 0), 101010256), U32.is_eq(u16(x, 20), (len - p - 22 : U32))))
91
92def eocd.win(a: Array<U32>, +len: U32, +p: U32) -> Array<U32> & Bool:
93  eocd.of(grab(a, p, 22), len, p)
94
95# f counts the positions left below p; a comment is at most 65535 bytes.
96def eocd.go(f: Nat, r: Array<U32> & Bool, +len: U32, +p: U32) -> Array<U32> & Maybe<&2, U32>:
97  match f:
98    case 0n:
99      (a, hit) = r
100      (a, Bool.pick(Maybe<&2, U32>, hit, Some{p}, None{}))
101    case 1n+q:
102      (a, hit) = r
103      match hit:
104        case True{}:
105          (a, Some{p})
106        case False{}:
107          eocd.go(q, eocd.win(a, len, (p - 1 : U32)), len, (p - 1 : U32))
108
109def cd.fin.end(ok: Bool, acc: List<&2, Header>) -> Result<&1, &1, U32 & String, List<&2, Header>>:
110  match ok:
111    case True{}:
112      Done{List.reverse(&2, Header, acc)}
113    case False{}:
114      Fail{(22, "central directory size does not match its entries")}
115
116def cd.fin(res: Result<&1, &1, U32 & String, U32 & List<&2, Header>>, +end: U32) -> Result<&1, &1, U32 & String, List<&2, Header>>:
117  match res:
118    case Fail{e}:
119      Fail{e}
120    case Done{(+p, acc)}:
121      cd.fin.end(U32.is_eq(p, end), acc)
122
123def lh.push(ok: Bool, a: Array<U32>, +hd: Header, +next: U32, acc: List<&2, Header>) -> Array<U32> & Result<&1, &1, U32 & String, U32 & List<&2, Header>>:
124  match ok:
125    case False{}:
126      (a, Fail{(22, "local header name differs from the central directory")})
127    case True{}:
128      (a, Done{(next, Con{hd, acc})})
129
130def lh.same(r: Array<U32> & Bool, +hd: Header, +next: U32, acc: List<&2, Header>) -> Array<U32> & Result<&1, &1, U32 & String, U32 & List<&2, Header>>:
131  (a, ok) = r
132  lh.push(ok, a, hd, next, acc)
133
134def lh.name(err: Maybe<&2, String>, a: Array<U32>, +lname: U32, +hd: Header, +next: U32, acc: List<&2, Header>) -> Array<U32> & Result<&1, &1, U32 & String, U32 & List<&2, Header>>:
135  match err:
136    case Some{m}:
137      (a, Fail{(22, m)})
138    case None{}:
139      Header{+name, +nlen, method, crc, packed, size, data} = hd
140      lh.same(same.go(U32.to_nat(nlen), (a, True{}), name, lname), hd, next, acc)
141
142# Local file header (APPNOTE 4.3.7): it must agree with the central directory, and its data must end before the directory.
143def lh.err(+l: List<&2, U32>, +method: U32, +nlen: U32, +packed: U32, +cdoff: U32, +lname: U32, +extra: U32) -> Maybe<&2, String>:
144  +data = (lname + extra : U32)
145  why(U32.is_eq(u32(l, 0), 67324752), "bad local header signature",
146    why(Bool.not(encrypted(u16(l, 6))), "encrypted entries are unsupported",
147      why(U32.is_eq(u16(l, 8), method), "local header method differs from the central directory",
148        why(U32.is_eq(u16(l, 26), nlen), "local header name differs from the central directory",
149          why(Bytes.fits(cdoff, lname, extra), "local header runs past the central directory",
150            why(Bytes.fits(cdoff, data, packed), "entry data runs past the central directory", None{}))))))
151
152def lh.head(r: Array<U32> & List<&2, U32>, +h: List<&2, U32>, +p: U32, +next: U32, +cdoff: U32, acc: List<&2, Header>) -> Array<U32> & Result<&1, &1, U32 & String, U32 & List<&2, Header>>:
153  (a, +l) = r
154  +nlen = u16(h, 28)
155  +method = u16(h, 10)
156  +packed = u32(h, 20)
157  +lname = (u32(h, 42) + 30 : U32)
158  +extra = (u16(l, 26) + u16(l, 28) : U32)
159  lh.name(lh.err(l, method, nlen, packed, cdoff, lname, extra), a, lname, Header{(p + 46 : U32), nlen, method, u32(h, 16), packed, u32(h, 24), (lname + extra : U32)}, next, acc)
160
161def lh.at(ok: Bool, a: Array<U32>, +h: List<&2, U32>, +p: U32, +next: U32, +cdoff: U32, acc: List<&2, Header>) -> Array<U32> & Result<&1, &1, U32 & String, U32 & List<&2, Header>>:
162  match ok:
163    case False{}:
164      (a, Fail{(22, "local header is out of bounds")})
165    case True{}:
166      lh.head(grab(a, u32(h, 42), 30), h, p, next, cdoff, acc)
167
168# Central directory file header (APPNOTE 4.3.12) at p, with the directory ending at end.
169def cd.err(+h: List<&2, U32>, +p: U32, +end: U32) -> Maybe<&2, String>:
170  +method = u16(h, 10)
171  +packed = u32(h, 20)
172  +size = u32(h, 24)
173  +rest = (u16(h, 28) + u16(h, 30) + u16(h, 32) : U32)
174  +zip64 = Bool.or(Bool.or(U32.is_eq(packed, 4294967295), U32.is_eq(size, 4294967295)), U32.is_eq(u32(h, 42), 4294967295))
175  why(U32.is_eq(u32(h, 0), 33639248), "bad central directory header signature",
176    why(Bool.not(encrypted(u16(h, 8))), "encrypted entries are unsupported",
177      why(supported(method), "unsupported compression method " ++ U32.show(method),
178        why(Bool.not(zip64), "ZIP64 is unsupported",
179          why(U32.is_eq(u16(h, 34), 0), "multi-disk ZIP is unsupported",
180            why(Bytes.fits(end, (p + 46 : U32), rest), "central directory header runs past the directory",
181              why(Bool.or(U32.is_eq(method, 8), U32.is_eq(packed, size)), "stored entry sizes differ", None{})))))))
182
183def cd.head.of(err: Maybe<&2, String>, a: Array<U32>, +h: List<&2, U32>, +p: U32, +cdoff: U32, acc: List<&2, Header>) -> Array<U32> & Result<&1, &1, U32 & String, U32 & List<&2, Header>>:
184  match err:
185    case Some{m}:
186      (a, Fail{(22, m)})
187    case None{}:
188      +next = (p + 46 + u16(h, 28) + u16(h, 30) + u16(h, 32) : U32)
189      lh.at(Bytes.fits(cdoff, u32(h, 42), 30), a, h, p, next, cdoff, acc)
190
191def cd.head(r: Array<U32> & List<&2, U32>, +p: U32, +end: U32, +cdoff: U32, acc: List<&2, Header>) -> Array<U32> & Result<&1, &1, U32 & String, U32 & List<&2, Header>>:
192  (a, +h) = r
193  cd.head.of(cd.err(h, p, end), a, h, p, cdoff, acc)
194
195def cd.entry(ok: Bool, a: Array<U32>, +p: U32, +end: U32, +cdoff: U32, acc: List<&2, Header>) -> Array<U32> & Result<&1, &1, U32 & String, U32 & List<&2, Header>>:
196  match ok:
197    case False{}:
198      (a, Fail{(22, "central directory is truncated")})
199    case True{}:
200      cd.head(grab(a, p, 46), p, end, cdoff, acc)
201
202# k entries left; r holds the next header's offset and the headers so far, reversed.
203def cd.go(k: Nat, r: Array<U32> & Result<&1, &1, U32 & String, U32 & List<&2, Header>>, +end: U32, +cdoff: U32) -> Array<U32> & Result<&1, &1, U32 & String, List<&2, Header>>:
204  match k:
205    case 0n:
206      (a, res) = r
207      (a, cd.fin(res, end))
208    case 1n+q:
209      (a, res) = r
210      match res:
211        case Fail{e}:
212          (a, Fail{e})
213        case Done{(+p, acc)}:
214          cd.go(q, cd.entry(Bytes.fits(end, p, 46), a, p, end, cdoff, acc), end, cdoff)
215
216def eocd.err(+x: List<&2, U32>, +e: U32) -> Maybe<&2, String>:
217  +zip64 = Bool.or(Bool.or(U32.is_eq(u16(x, 10), 65535), U32.is_eq(u32(x, 12), 4294967295)), U32.is_eq(u32(x, 16), 4294967295))
218  why(Bool.and(Bool.and(U32.is_eq(u16(x, 4), 0), U32.is_eq(u16(x, 6), 0)), U32.is_eq(u16(x, 8), u16(x, 10))), "multi-disk ZIP is unsupported",
219    why(Bool.not(zip64), "ZIP64 is unsupported",
220      why(Bytes.fits(e, u32(x, 16), u32(x, 12)), "central directory is out of bounds", None{})))
221
222def eocd.checked(err: Maybe<&2, String>, a: Array<U32>, +x: List<&2, U32>) -> Array<U32> & Result<&1, &1, U32 & String, List<&2, Header>>:
223  match err:
224    case Some{m}:
225      (a, Fail{(22, m)})
226    case None{}:
227      +off = u32(x, 16)
228      cd.go(U32.to_nat(u16(x, 10)), (a, Done{(off, Nil{})}), (off + u32(x, 12) : U32), off)
229
230def eocd.parse(r: Array<U32> & List<&2, U32>, +e: U32) -> Array<U32> & Result<&1, &1, U32 & String, List<&2, Header>>:
231  (a, +x) = r
232  eocd.checked(eocd.err(x, e), a, x)
233
234def eocd.found(r: Array<U32> & Maybe<&2, U32>) -> Array<U32> & Result<&1, &1, U32 & String, List<&2, Header>>:
235  (a, m) = r
236  match m:
237    case None{}:
238      (a, Fail{(22, "no end of central directory record")})
239    case Some{+e}:
240      eocd.parse(grab(a, e, 22), e)
241
242def headers.at(short: Bool, a: Array<U32>, +len: U32) -> Array<U32> & Result<&1, &1, U32 & String, List<&2, Header>>:
243  match short:
244    case True{}:
245      (a, Fail{(22, "input is shorter than an end of central directory record")})
246    case False{}:
247      +p = (len - 22 : U32)
248      eocd.found(eocd.go(U32.to_nat(U32.min(p, 65535)), eocd.win(a, len, p), len, p))
249
250def headers.fin(+len: U32, r: Array<U32> & Result<&1, &1, U32 & String, List<&2, Header>>) -> Bytes.Bytes & Result<&1, &1, U32 & String, List<&2, Header>>:
251  (a, res) = r
252  (Bytes.Bytes{len, a}, res)
253
254# The input back, and its central directory with every bound, local header, and method checked. Pure: no data is decoded.
255def headers(input: Bytes.Bytes) -> Bytes.Bytes & Result<&1, &1, U32 & String, List<&2, Header>>:
256  Bytes.Bytes{+len, buf} = input
257  headers.fin(len, headers.at(U32.is_lt(len, 22), buf, len))
258
259def inflated(r: Result<&1, &1, U32 & String, Bytes.Bytes>) -> Result<&1, &1, U32 & String, Bytes.Bytes>:
260  match r:
261    case Fail{e}:
262      (+code, msg) = e
263      Fail{Bool.pick(U32 & String, U32.is_eq(code, 27), (22, "entry size differs from the central directory"), (code, "DEFLATE entry: " ++ msg))}
264    case Done{b}:
265      Done{b}
266
267# Output past size is refused inside libz, so a bomb never grows beyond its declared size.
268def inflate.of(+size: U32, b: Bytes.Bytes) -> IO(Result<&1, &1, U32 & String, Bytes.Bytes>):
269  do IO<Result<&1, &1, U32 & String, Bytes.Bytes>>:
270    r : Result<&1, &1, U32 & String, Bytes.Bytes> <- Zlib.libz.inflate.raw(size, b)
271    return inflated(r)
272
273def decode(stored: Bool, +size: U32, raw: Bytes.Bytes) -> IO(Result<&1, &1, U32 & String, Bytes.Bytes>):
274  match stored:
275    case True{}:
276      IO.pure(Result<&1, &1, U32 & String, Bytes.Bytes>, Done{raw})
277    case False{}:
278      inflate.of(size, raw)
279
280def check.crc.of(ok: Bool, b: Bytes.Bytes) -> Result<&1, &1, U32 & String, Bytes.Bytes>:
281  match ok:
282    case True{}:
283      Done{b}
284    case False{}:
285      Fail{(22, "entry CRC-32 does not match")}
286
287def check.crc(r: Bytes.Bytes & U32, +crc: U32) -> Result<&1, &1, U32 & String, Bytes.Bytes>:
288  (b, +c) = r
289  check.crc.of(U32.is_eq(c, crc), b)
290
291def check.len.of(ok: Bool, b: Bytes.Bytes, +crc: U32) -> Result<&1, &1, U32 & String, Bytes.Bytes>:
292  match ok:
293    case False{}:
294      Fail{(22, "entry size differs from the central directory")}
295    case True{}:
296      check.crc(crc.bytes(b), crc)
297
298def check.len(r: Bytes.Bytes & U32, +size: U32, +crc: U32) -> Result<&1, &1, U32 & String, Bytes.Bytes>:
299  (b, +n) = r
300  check.len.of(U32.is_eq(n, size), b, crc)
301
302def check(+size: U32, +crc: U32, r: Result<&1, &1, U32 & String, Bytes.Bytes>) -> Result<&1, &1, U32 & String, Bytes.Bytes>:
303  match r:
304    case Fail{e}:
305      Fail{e}
306    case Done{b}:
307      check.len(Bytes.length(b), size, crc)
308
309def one.put(r: Result<&1, &1, U32 & String, Bytes.Bytes>, nm: Bytes.Bytes, +method: U32, +crc: U32, +left: U32, +size: U32, acc: List<&1, Entry>) -> Result<&1, &1, U32 & String, U32 & List<&1, Entry>>:
310  match r:
311    case Fail{e}:
312      Fail{e}
313    case Done{b}:
314      Done{((left - size : U32), Con{Entry{nm, b, method, crc}, acc})}
315
316def one.data(r: Bytes.Bytes & Bytes.Bytes, nm: Bytes.Bytes, +method: U32, +crc: U32, +size: U32, +left: U32, acc: List<&1, Entry>) -> IO(Bytes.Bytes & Result<&1, &1, U32 & String, U32 & List<&1, Entry>>):
317  (input, raw) = r
318  do IO<Bytes.Bytes & Result<&1, &1, U32 & String, U32 & List<&1, Entry>>>:
319    out : Result<&1, &1, U32 & String, Bytes.Bytes> <- decode(U32.is_eq(method, 0), size, raw)
320    return (input, one.put(check(size, crc, out), nm, method, crc, left, size, acc))
321
322def one.name(r: Bytes.Bytes & Bytes.Bytes, +method: U32, +crc: U32, +packed: U32, +size: U32, +data: U32, +left: U32, acc: List<&1, Entry>) -> IO(Bytes.Bytes & Result<&1, &1, U32 & String, U32 & List<&1, Entry>>):
323  (input, nm) = r
324  one.data(Bytes.slice(input, data, packed), nm, method, crc, size, left, acc)
325
326# left: the output still allowed under the caller's max.
327def one.cap(over: Bool, input: Bytes.Bytes, +hd: Header, +left: U32, acc: List<&1, Entry>) -> IO(Bytes.Bytes & Result<&1, &1, U32 & String, U32 & List<&1, Entry>>):
328  match over:
329    case True{}:
330      IO.pure(Bytes.Bytes & Result<&1, &1, U32 & String, U32 & List<&1, Entry>>, (input, Fail{(27, "archive output is larger than max")}))
331    case False{}:
332      Header{+name, +nlen, +method, +crc, +packed, +size, +data} = hd
333      one.name(Bytes.slice(input, name, nlen), method, crc, packed, size, data, left, acc)
334
335def one(+hd: Header, input: Bytes.Bytes, +left: U32, acc: List<&1, Entry>) -> IO(Bytes.Bytes & Result<&1, &1, U32 & String, U32 & List<&1, Entry>>):
336  Header{name, nlen, method, crc, packed, +size, data} = hd
337  one.cap(U32.is_lt(left, size), input, hd, left, acc)
338
339def run.fin(res: Result<&1, &1, U32 & String, U32 & List<&1, Entry>>) -> Result<&1, &1, U32 & String, List<&1, Entry>>:
340  match res:
341    case Fail{e}:
342      Fail{e}
343    case Done{(left, acc)}:
344      Done{List.reverse(&1, Entry, acc)}
345
346def run(xs: List<&2, Header>, st: Bytes.Bytes & Result<&1, &1, U32 & String, U32 & List<&1, Entry>>) -> IO(Result<&1, &1, U32 & String, List<&1, Entry>>):
347  match xs:
348    case Nil{}:
349      (input, res) = st
350      IO.pure(Result<&1, &1, U32 & String, List<&1, Entry>>, run.fin(res))
351    case Con{hd, t}:
352      (input, res) = st
353      match res:
354        case Fail{e}:
355          IO.pure(Result<&1, &1, U32 & String, List<&1, Entry>>, Fail{e})
356        case Done{(+left, acc)}:
357          do IO<Result<&1, &1, U32 & String, List<&1, Entry>>>:
358            next : Bytes.Bytes & Result<&1, &1, U32 & String, U32 & List<&1, Entry>> <- one(hd, input, left, acc)
359            run(t, next)
360
361def read.of(r: Bytes.Bytes & Result<&1, &1, U32 & String, List<&2, Header>>, +max: U32) -> IO(Result<&1, &1, U32 & String, List<&1, Entry>>):
362  (input, res) = r
363  match res:
364    case Fail{e}:
365      IO.pure(Result<&1, &1, U32 & String, List<&1, Entry>>, Fail{e})
366    case Done{xs}:
367      run(xs, (input, Done{(max, Nil{})}))
368
369# Every entry of a ZIP archive, in central directory order, or the first problem found.
370# Stored (0) and DEFLATE (8) entries only; no ZIP64, encryption, or multi-disk archives.
371# Output past max bytes in total fails with 27 (EFBIG). Malformed ZIP fails with 22 (EINVAL); libz load and allocation errors keep their host codes.
372def read(max: U32, input: Bytes.Bytes) -> IO(Result<&1, &1, U32 & String, List<&1, Entry>>):
373  read.of(headers(input), max)