dns.bend
bend-kit-dns@0.3.2.1 · 615 lines · 0 definitions
1# DNS codec and host lookup. Source: https://github.com/paymog/bend-kit/tree/main/dns
2import Base
3# bend-kit-wire@0.4.0.3
4import bend-kit-wire@0.4.0.3/wire.bend as Wire
5
6# query, answer, and resolve.pure are pure; PROOF.bend covers them, not effs/.
7# resolve uses the OS resolver (IPv4 A only, same Maybe<String> as before).
8# import bend-kit-dns@0.3.2.0/dns.bend as Dns
9
10type Cur is Data:
11 Cur{v: U32, rest: String}
12
13type RR is Data:
14 RRBad{}
15 RRA{ip: String}
16 RRSkip{rest: String}
17
18def u8(s: String) -> Maybe<&2, Cur>:
19 match s:
20 case SNil{}:
21 None{}
22 case SCon{Chr{c}, t}:
23 Some{Cur{c, t}}
24
25def u16.lo(hi: U32, m: Maybe<&2, Cur>) -> Maybe<&2, Cur>:
26 match m:
27 case None{}:
28 None{}
29 case Some{Cur{lo, r}}:
30 Some{Cur{(hi * 256 + lo : U32), r}}
31
32def u16.go(m: Maybe<&2, Cur>) -> Maybe<&2, Cur>:
33 match m:
34 case None{}:
35 None{}
36 case Some{Cur{hi, r}}:
37 u16.lo(hi, u8(r))
38
39def u16(s: String) -> Maybe<&2, Cur>:
40 u16.go(u8(s))
41
42def skip.if(+s: String, +n: Nat, short: Bool) -> Maybe<&2, String>:
43 match short:
44 case True{}:
45 None{}
46 case False{}:
47 Some{String.drop(s, n)}
48
49def skip(+s: String, +n: Nat) -> Maybe<&2, String>:
50 skip.if(s, n, Nat.is_lt(String.length(s), n))
51
52def then(m: Maybe<&2, String>, n: Nat) -> Maybe<&2, String>:
53 match m:
54 case None{}:
55 None{}
56 case Some{r}:
57 skip(r, n)
58
59def push16(+n: U32, acc: String) -> String:
60 SCon{Chr{U32.and(n, 255)}, SCon{Chr{U32.shrn(n, 8n)}, acc}}
61
62# Query
63# -----
64
65def label.ok(+l: String) -> Bool:
66 +n = String.length(l)
67 Bool.and(Nat.is_lt(0n, n), Nat.is_le(n, 63n))
68
69def label.ascii(s: String) -> Bool:
70 match s:
71 case SNil{}:
72 True{}
73 case SCon{Chr{c}, t}:
74 Bool.and(U32.is_lt(c, 128), label.ascii(t))
75
76def labels.ok(xs: List<&2, String>) -> Bool:
77 match xs:
78 case Nil{}:
79 True{}
80 case Con{+l, t}:
81 Bool.and(Bool.and(label.ok(l), label.ascii(l)), labels.ok(t))
82
83def labels.put(xs: List<&2, String>, acc: String) -> String:
84 match xs:
85 case Nil{}:
86 acc
87 case Con{+l, t}:
88 labels.put(t, String.reverse(l) ++ SCon{Chr{U32.from_nat(String.length(l))}, acc})
89
90def query.if(+id: U32, xs: List<&2, String>, ok: Bool) -> Maybe<&2, String>:
91 match ok:
92 case False{}:
93 None{}
94 case True{}:
95 # header: id, RD, QDCOUNT 1; question: QNAME, QTYPE A, QCLASS IN
96 Some{String.reverse(push16(1, push16(1, SCon{Chr{0}, labels.put(xs, push16(0, push16(0, push16(0, push16(1, push16(256, push16(id, SNil{})))))))})))}
97
98def query.labels(+id: U32, +xs: List<&2, String>) -> Maybe<&2, String>:
99 query.if(id, xs, labels.ok(xs))
100
101def strip_dot.if(+s: String, dot: Bool) -> String:
102 match dot:
103 case True{}:
104 String.reverse(String.drop(String.reverse(s), 1n))
105 case False{}:
106 s
107
108def strip_dot(+s: String) -> String:
109 strip_dot.if(s, String.ends_with(s, "."))
110
111# RFC 1035 §4.1: a standard query for the A record of name.
112def query(id: U32, name: String) -> Maybe<&2, String>:
113 query.labels(id, String.split(strip_dot(name), '.'))
114
115# Answer
116# ------
117
118# §4.1.4: a name is labels ending in a zero octet, or a two-octet pointer.
119def name.skip(fuel: Nat, s: String) -> Maybe<&2, String>:
120 match fuel:
121 case 0n:
122 None{}
123 case 1n+f:
124 match s:
125 case SNil{}:
126 None{}
127 case SCon{Chr{+l}, +t}:
128 Bool.pick(Maybe<&2, String>, U32.is_eq(l, 0), Some{t}, Bool.pick(Maybe<&2, String>, U32.is_le(192, l), skip(t, 1n), Bool.pick(Maybe<&2, String>, U32.is_le(64, l), None{}, name.skip(f, String.drop(t, U32.to_nat(l))))))
129
130def name.then(m: Maybe<&2, String>, n: Nat) -> Maybe<&2, String>:
131 match m:
132 case None{}:
133 None{}
134 case Some{+r}:
135 then(name.skip(String.length(r), r), n)
136
137def dotted(s: String) -> String:
138 match s:
139 case SNil{}:
140 ""
141 case SCon{Chr{c}, t}:
142 match t:
143 case SNil{}:
144 U32.show(c)
145 case SCon{_, _}:
146 U32.show(c) ++ "." ++ dotted(t)
147
148def rr.f(+r: String, +len: U32, a: Bool) -> RR:
149 match a:
150 case True{}:
151 RRA{dotted(String.take(r, 4n))}
152 case False{}:
153 RRSkip{String.drop(r, U32.to_nat(len))}
154
155def rr.data(+r: String, +len: U32, a: Bool, short: Bool) -> RR:
156 match short:
157 case True{}:
158 RRBad{}
159 case False{}:
160 rr.f(r, len, a)
161
162def rr.e(+ty: U32, +cl: U32, m: Maybe<&2, Cur>) -> RR:
163 match m:
164 case None{}:
165 RRBad{}
166 case Some{Cur{+len, +r}}:
167 rr.data(r, len, Bool.and(Bool.and(U32.is_eq(ty, 1), U32.is_eq(cl, 1)), U32.is_eq(len, 4)), Nat.is_lt(String.length(r), U32.to_nat(len)))
168
169def rr.d(ty: U32, cl: U32, m: Maybe<&2, String>) -> RR:
170 match m:
171 case None{}:
172 RRBad{}
173 case Some{r}:
174 rr.e(ty, cl, u16(r))
175
176def rr.c(ty: U32, m: Maybe<&2, Cur>) -> RR:
177 match m:
178 case None{}:
179 RRBad{}
180 case Some{Cur{cl, r}}:
181 rr.d(ty, cl, skip(r, 4n))
182
183def rr.b(m: Maybe<&2, Cur>) -> RR:
184 match m:
185 case None{}:
186 RRBad{}
187 case Some{Cur{ty, r}}:
188 rr.c(ty, u16(r))
189
190def rr.a(m: Maybe<&2, String>) -> RR:
191 match m:
192 case None{}:
193 RRBad{}
194 case Some{r}:
195 rr.b(u16(r))
196
197# §4.1.3: NAME, TYPE, CLASS, TTL, RDLENGTH, RDATA.
198def rr(+s: String) -> RR:
199 rr.a(name.skip(String.length(s), s))
200
201# fuel = records left. The first A record wins; CNAMEs before it are skipped.
202def answers.scan(fuel: Nat, r: RR) -> Maybe<&2, String>:
203 match fuel:
204 case 0n:
205 None{}
206 case 1n+f:
207 match r:
208 case RRBad{}:
209 None{}
210 case RRA{ip}:
211 Some{ip}
212 case RRSkip{s}:
213 answers.scan(f, rr(s))
214
215def questions(fuel: Nat, m: Maybe<&2, String>) -> Maybe<&2, String>:
216 match fuel:
217 case 0n:
218 m
219 case 1n+f:
220 questions(f, name.then(m, 4n))
221
222def body.go(an: U32, m: Maybe<&2, String>) -> Maybe<&2, String>:
223 match m:
224 case None{}:
225 None{}
226 case Some{s}:
227 answers.scan(U32.to_nat(an), rr(s))
228
229def body.an(qd: U32, m: Maybe<&2, Cur>) -> Maybe<&2, String>:
230 match m:
231 case None{}:
232 None{}
233 case Some{Cur{an, r}}:
234 body.go(an, questions(U32.to_nat(qd), skip(r, 4n)))
235
236def body.qd(m: Maybe<&2, Cur>) -> Maybe<&2, String>:
237 match m:
238 case None{}:
239 None{}
240 case Some{Cur{qd, r}}:
241 body.an(qd, u16(r))
242
243# §4.1.1: QR set, opcode QUERY, not truncated, RCODE 0.
244def flags.ok(+f: U32) -> Bool:
245 Bool.and(Bool.and(U32.is_eq(U32.and(f, 32768), 32768), U32.is_eq(U32.and(f, 30720), 0)), Bool.and(U32.is_eq(U32.and(f, 512), 0), U32.is_eq(U32.and(f, 15), 0)))
246
247def head.flags.if(r: String, ok: Bool) -> Maybe<&2, String>:
248 match ok:
249 case False{}:
250 None{}
251 case True{}:
252 body.qd(u16(r))
253
254def head.flags(m: Maybe<&2, Cur>) -> Maybe<&2, String>:
255 match m:
256 case None{}:
257 None{}
258 case Some{Cur{+f, r}}:
259 head.flags.if(r, flags.ok(f))
260
261def head.id.if(r: String, ok: Bool) -> Maybe<&2, String>:
262 match ok:
263 case False{}:
264 None{}
265 case True{}:
266 head.flags(u16(r))
267
268def head.id(id: U32, m: Maybe<&2, Cur>) -> Maybe<&2, String>:
269 match m:
270 case None{}:
271 None{}
272 case Some{Cur{got, r}}:
273 head.id.if(r, U32.is_eq(id, got))
274
275# The IPv4 address the response gives for the query with this id.
276def answer(id: U32, msg: String) -> Maybe<&2, String>:
277 head.id(id, u16(msg))
278
279# resolv.conf
280# -----------
281
282def nameservers.add(+line: String, rest: List<&2, String>, hit: Bool) -> List<&2, String>:
283 match hit:
284 case False{}:
285 rest
286 case True{}:
287 Con{String.trim(String.drop(line, 10n)), rest}
288
289def nameservers.go(xs: List<&2, String>) -> List<&2, String>:
290 match xs:
291 case Nil{}:
292 Nil{}
293 case Con{+line, t}:
294 nameservers.add(line, nameservers.go(t), String.starts_with(line, "nameserver"))
295
296# Every nameserver line, in file order.
297def nameservers(conf: String) -> List<&2, String>:
298 nameservers.go(String.lines(conf))
299
300def nameserver.first(xs: List<&2, String>) -> Maybe<&2, String>:
301 match xs:
302 case Nil{}:
303 None{}
304 case Con{n, t}:
305 Some{n}
306
307# The first nameserver line of a resolv.conf.
308def nameserver(conf: String) -> Maybe<&2, String>:
309 nameserver.first(nameservers(conf))
310
311# Resolve
312# -------
313
314def none() -> IO(Maybe<&2, String>):
315 IO.pure(Maybe<&2, String>, None{})
316
317def ipv4.go(s: String) -> Bool:
318 match s:
319 case SNil{}:
320 True{}
321 case SCon{Chr{+c}, t}:
322 Bool.and(Bool.or(U32.is_eq(c, 46), Bool.and(U32.is_le(48, c), U32.is_le(c, 57))), ipv4.go(t))
323
324# Digits and dots; TCP.connect rejects anything else that is not an address.
325def ipv4(+s: String) -> Bool:
326 Bool.and(Bool.not(String.is_empty(s)), ipv4.go(s))
327
328# One attempt's outcome: try again, or this answer (None: no address).
329type Try is Data:
330 Again{}
331 Got{ip: Maybe<&2, String>}
332
333def try.pure(s: Socket, t: Try) -> IO(Socket & Try):
334 IO.pure(Socket & Try, (s, t))
335
336# A datagram from anyone but the nameserver's port 53 is ignored (retried).
337def try.from(s: Socket, +ns: String, id: U32, hpd: String & U32 & String) -> IO(Socket & Try):
338 (h, +p, d) = hpd
339 try.pure(s, Bool.pick(Try, Bool.and(String.eq(h, ns), U32.is_eq(p, 53)), Got{answer(id, d)}, Again{}))
340
341def try.back(ns: String, id: U32, m: Socket & Result<&1, &1, U32 & String, String & U32 & String>) -> IO(Socket & Try):
342 (s, r) = m
343 match r:
344 case Fail{e}:
345 try.pure(s, Again{})
346 case Done{hpd}:
347 try.from(s, ns, id, hpd)
348
349# §4.2.1 and resolv.conf defaults: 5 s per attempt.
350def try.sent(ns: String, id: U32, m: Socket & Result<&1, &1, U32 & String, Unit>) -> IO(Socket & Try):
351 (s, r) = m
352 match r:
353 case Fail{e}:
354 try.pure(s, Again{})
355 case Done{u}:
356 do IO<Socket & Try>:
357 back : Socket & Result<&1, &1, U32 & String, String & U32 & String> <- Wire.recv_from(s, 512, 5000)
358 try.back(ns, id, back)
359
360def try.once(s: Socket, +ns: String, id: U32, q: String) -> IO(Socket & Try):
361 do IO<Socket & Try>:
362 sent : Socket & Result<&1, &1, U32 & String, Unit> <- Wire.send_to(s, ns, 53, q)
363 try.sent(ns, id, sent)
364
365def try.close(s: Socket, r: Maybe<&2, String>) -> IO(Maybe<&2, String>):
366 do IO<Maybe<&2, String>>:
367 Socket.close(s)
368 return r
369
370def tries.end(st: Socket & Try) -> IO(Maybe<&2, String>):
371 (s, t) = st
372 match t:
373 case Got{ip}:
374 try.close(s, ip)
375 case Again{}:
376 try.close(s, None{})
377
378# fuel: attempts left (resolv.conf's default is 2).
379def tries(fuel: Nat, +ns: String, +id: U32, +q: String, st: Socket & Try) -> IO(Maybe<&2, String>):
380 match fuel:
381 case 0n:
382 tries.end(st)
383 case 1n+f:
384 (s, t) = st
385 match t:
386 case Got{ip}:
387 try.close(s, ip)
388 case Again{}:
389 do IO<Maybe<&2, String>>:
390 next : Socket & Try <- try.once(s, ns, id, q)
391 tries(f, ns, id, q, next)
392
393def resolve.sock(ns: String, id: U32, q: String, r: Result<&1, &1, U32 & String, Socket>) -> IO(Maybe<&2, String>):
394 match r:
395 case Fail{e}:
396 none()
397 case Done{s}:
398 tries(2n, ns, id, q, (s, Again{}))
399
400def resolve.q(ns: String, id: U32, q: Maybe<&2, String>) -> IO(Maybe<&2, String>):
401 match q:
402 case None{}:
403 none()
404 case Some{bytes}:
405 do IO<Maybe<&2, String>>:
406 u : Result<&1, &1, U32 & String, Socket> <- UDP.bind(0)
407 resolve.sock(ns, id, bytes, u)
408
409# §7.3: a random id makes forged answers harder to land.
410def resolve.id(name: String, ns: String, r: Result<&1, &1, U32 & String, U32>) -> IO(Maybe<&2, String>):
411 match r:
412 case Fail{e}:
413 none()
414 case Done{x}:
415 +id = U32.and(x, 65535)
416 resolve.q(ns, id, query(id, name))
417
418def resolve.ns(name: String, ns: Maybe<&2, String>) -> IO(Maybe<&2, String>):
419 match ns:
420 case None{}:
421 none()
422 case Some{n}:
423 do IO<Maybe<&2, String>>:
424 r : Result<&1, &1, U32 & String, U32> <- IO.random_u32()
425 resolve.id(name, n, r)
426
427# Ask one nameserver. Tests use this; resolve reads /etc/resolv.conf.
428def resolve.at(+host: String, ns: String) -> IO(Maybe<&2, String>):
429 resolve.ns(host, Some{ns})
430
431def conf.text(r: Result<&1, &1, U32 & String, String>) -> String:
432 match r:
433 case Fail{e}:
434 ""
435 case Done{s}:
436 s
437
438# ponytail: 3 nameservers; a longer resolv.conf ignores the rest
439def resolve.n3(+name: String, xs: List<&2, String>) -> IO(Maybe<&2, String>):
440 match xs:
441 case Nil{}:
442 none()
443 case Con{+ns, t}:
444 resolve.at(name, ns)
445
446def resolve.n2b(+name: String, rest: List<&2, String>, ip: Maybe<&2, String>) -> IO(Maybe<&2, String>):
447 match ip:
448 case Some{s}:
449 IO.pure(Maybe<&2, String>, Some{s})
450 case None{}:
451 resolve.n3(name, rest)
452
453def resolve.n2(+name: String, xs: List<&2, String>) -> IO(Maybe<&2, String>):
454 match xs:
455 case Nil{}:
456 none()
457 case Con{+ns, t}:
458 do IO<Maybe<&2, String>>:
459 ip : Maybe<&2, String> <- resolve.at(name, ns)
460 resolve.n2b(name, t, ip)
461
462def resolve.n1b(+name: String, rest: List<&2, String>, ip: Maybe<&2, String>) -> IO(Maybe<&2, String>):
463 match ip:
464 case Some{s}:
465 IO.pure(Maybe<&2, String>, Some{s})
466 case None{}:
467 resolve.n2(name, rest)
468
469def resolve.list(+name: String, xs: List<&2, String>) -> IO(Maybe<&2, String>):
470 match xs:
471 case Nil{}:
472 none()
473 case Con{+ns, t}:
474 do IO<Maybe<&2, String>>:
475 ip : Maybe<&2, String> <- resolve.at(name, ns)
476 resolve.n1b(name, t, ip)
477
478def resolve.read(name: String, m: File & Result<&1, &1, U32 & String, String>) -> IO(Maybe<&2, String>):
479 (f, r) = m
480 do IO<Maybe<&2, String>>:
481 File.close(f)
482 resolve.list(name, nameservers(conf.text(r)))
483
484def resolve.conf(name: String, r: Result<&1, &1, U32 & String, File>) -> IO(Maybe<&2, String>):
485 match r:
486 case Fail{e}:
487 none()
488 case Done{f}:
489 do IO<Maybe<&2, String>>:
490 m : File & Result<&1, &1, U32 & String, String> <- File.read(f, 65536)
491 resolve.read(name, m)
492
493def resolve.dns(name: String) -> IO(Maybe<&2, String>):
494 do IO<Maybe<&2, String>>:
495 f : Result<&1, &1, U32 & String, File> <- File.open("/etc/resolv.conf", "r")
496 resolve.conf(name, f)
497
498
499def hosts.pick(found: Maybe<&2, String>, now: Maybe<&2, String>) -> Maybe<&2, String>:
500 match found:
501 case Some{s}:
502 Some{s}
503 case None{}:
504 now
505
506def hosts.hit(+ip: String, hit: Bool) -> Maybe<&2, String>:
507 match hit:
508 case True{}:
509 Some{ip}
510 case False{}:
511 None{}
512
513def hosts.names(xs: List<&2, String>, +name: String, +ip: String, found: Maybe<&2, String>) -> Maybe<&2, String>:
514 match xs:
515 case Nil{}:
516 found
517 case Con{+n, t}:
518 hosts.names(t, name, ip, hosts.pick(found, hosts.hit(ip, String.eq(String.to_lower(n), name))))
519
520def hosts.ip(+name: String, +ip: String, ns: List<&2, String>, ok: Bool) -> Maybe<&2, String>:
521 match ok:
522 case False{}:
523 None{}
524 case True{}:
525 hosts.names(ns, name, ip, None{})
526
527def hosts.line(+name: String, xs: List<&2, String>) -> Maybe<&2, String>:
528 match xs:
529 case Nil{}:
530 None{}
531 case Con{+ip, ns}:
532 hosts.ip(name, ip, ns, ipv4(ip))
533
534def hosts.sp(+c: U32, tab: Bool) -> U32:
535 match tab:
536 case True{}:
537 32
538 case False{}:
539 c
540
541def hosts.flat(s: String) -> String:
542 match s:
543 case SNil{}:
544 ""
545 case SCon{Chr{+c}, t}:
546 SCon{Chr{hosts.sp(c, U32.is_eq(c, 9))}, hosts.flat(t)}
547
548def hosts.scan(xs: List<&2, String>, +name: String, found: Maybe<&2, String>) -> Maybe<&2, String>:
549 match xs:
550 case Nil{}:
551 found
552 case Con{line, t}:
553 hosts.scan(t, name, hosts.pick(found, hosts.line(name, String.split(hosts.flat(line), ' '))))
554
555# First IPv4 address for name in an /etc/hosts file. The name is already lowercase.
556def hosts(+name: String, text: String) -> Maybe<&2, String>:
557 hosts.scan(String.lines(text), name, None{})
558
559def resolve.from(+name: String, m: Maybe<&2, String>) -> IO(Maybe<&2, String>):
560 match m:
561 case Some{ip}:
562 IO.pure(Maybe<&2, String>, Some{ip})
563 case None{}:
564 resolve.dns(name)
565
566def resolve.text(+name: String, r: Result<&1, &1, U32 & String, String>) -> IO(Maybe<&2, String>):
567 match r:
568 case Fail{e}:
569 resolve.dns(name)
570 case Done{s}:
571 resolve.from(name, hosts(name, s))
572
573def resolve.opened(+name: String, m: File & Result<&1, &1, U32 & String, String>) -> IO(Maybe<&2, String>):
574 (f, r) = m
575 do IO<Maybe<&2, String>>:
576 File.close(f)
577 resolve.text(name, r)
578
579def resolve.hosts(+name: String, r: Result<&1, &1, U32 & String, File>) -> IO(Maybe<&2, String>):
580 match r:
581 case Fail{e}:
582 resolve.dns(name)
583 case Done{f}:
584 do IO<Maybe<&2, String>>:
585 m : File & Result<&1, &1, U32 & String, String> <- File.read(f, 65536)
586 resolve.opened(name, m)
587
588def lookup(host: String) -> IO(Result<&1, &1, U32 & String, String>):
589 import "./effs/dns.c"
590 import "./effs/dns.js"
591
592def resolve.got(r: Result<&1, &1, U32 & String, String>) -> IO(Maybe<&2, String>):
593 match r:
594 case Fail{e}:
595 none()
596 case Done{ip}:
597 IO.pure(Maybe<&2, String>, Some{ip})
598
599def resolve.os(+name: String) -> IO(Maybe<&2, String>):
600 do IO<Maybe<&2, String>>:
601 r : Result<&1, &1, U32 & String, String> <- lookup(name)
602 resolve.got(r)
603
604# An IPv4 address for host: literals as is, localhost (RFC 6761), /etc/hosts, else UDP DNS.
605# ponytail: no AAAA, no TCP retry on TC
606def resolve.ask(+name: String) -> IO(Maybe<&2, String>):
607 do IO<Maybe<&2, String>>:
608 f : Result<&1, &1, U32 & String, File> <- File.open("/etc/hosts", "r")
609 resolve.hosts(name, f)
610
611def resolve.pure(+host: String) -> IO(Maybe<&2, String>):
612 Bool.pick(IO(Maybe<&2, String>), ipv4(host), IO.pure(Maybe<&2, String>, Some{host}), Bool.pick(IO(Maybe<&2, String>), String.eq(host, "localhost"), IO.pure(Maybe<&2, String>, Some{"127.0.0.1"}), resolve.ask(String.to_lower(host))))
613
614def resolve(+host: String) -> IO(Maybe<&2, String>):
615 Bool.pick(IO(Maybe<&2, String>), ipv4(host), IO.pure(Maybe<&2, String>, Some{host}), Bool.pick(IO(Maybe<&2, String>), String.eq(host, "localhost"), IO.pure(Maybe<&2, String>, Some{"127.0.0.1"}), resolve.os(String.to_lower(host))))