Against a real network
The stack is tested against QEMU's user network, slirp, the network sysk meets: live, and from recordings of it that replay anywhere. No guest runs. QEMU joins slirp and a socket on one hub, so every frame slirp sends arrives at the tests as a datagram, and every frame the stack sends reaches slirp. slirp checks every checksum, so a frame it answers was right.
The wire
The stack is sysp, built to C by sysp, with a few lines of C that only move records between standard input and output and host-step (borrowed until sysi runs all of sysp). The build, the shim and the records are sysp's host harness, which every part's host program shares (sysp 051): a record is a kind byte, a 32-bit little-endian length, then its bytes, its header's size said once in sysp's tools/harness.sysp, which the host lists among its sources (sysp 073). Racket starts it, starts QEMU, and passes frames between the two, writing every step down.
A session, recorded
A recording is a session as data: each command given to the stack, each frame either way, each report, in order. Select a row to see it whole.
The caller is a few lines of Racket in tools/record.rkt, the part sysk's server for /net will play: it gives commands, and sends again when the stack says it is asking for an address. In the UDP session, slirp asks for the guest's address itself before it delivers the datagram: a frame sysn did not write, answered as any host would.
Replayed exactly
make test replays every recording against a fresh stack: the recorded commands and slirp's frames go in, and the frames and reports that come out must be the recorded ones, in order. The stack has no clock and no randomness: the time is given to it, and a session writes down every time it gave, (now 1500000000), so a replay gives the same; TCP's key is fixed for the tests (sysn 003). So the same frames in always give the same frames out. The live tests check this of every live session too: a session run now must replay as itself.
make test runs each test file through the suite's tools/tested.rkt (sysx 101; sysn 017), which notes every file a test reads and keeps a pass with their hashes: a test file whose files all read as they did when it last passed is not run again, as Go's test cache does. The host program the tests build counts by its sources, and tests/docs-test.rkt starts tools/docs.rkt through tested-racket, so what that racket reads counts too. SYSX_TESTED=all runs every test.
For TCP the session is also the host's end of the connection, either way, and it can let time pass at once and lose a frame on purpose: in tcp-loss the stack's answer never reaches slirp, the clock goes to the deadline the stack gave, and the tick sends it again (TCP). In dns the stack asks slirp's server, 10.0.2.3, for example.com's address, and slirp asks the host's resolver; the answer the recording holds is whatever the internet said that day, and the live test asks only that an answer comes back and replays (DNS).
Hostile frames
Every frame slirp sent in a recording becomes dozens of tests, each changed the way a broken or hostile network would change it, with the stack's answer known beforehand:
| Change | Expect | |
|---|---|---|
| cut short | short | at every length below the packet's own: never read past the end |
| padding changed or cut | as before | bytes past the packet's total length are not part of it |
| another hardware address | not-ours | one bit of the destination flipped |
| another type | protocol | IPv6's type, 0x86dd |
| TTL or data changed | bad-sum | the IPv4 header's checksum, then ICMP's or UDP's |
| version 6, a 16-byte header | malformed | with the header's checksum made right again, so the check itself is what is tested |
| more fragments, an offset | fragment | the stack takes no fragments |
| GRE | protocol | an IPv4 protocol the stack does not take |
| to 10.0.2.99 | not-ours | another IPv4 address |
| a total past the end | short | a header that claims more bytes than came |
| four option bytes | as before | IPv4 options are skipped |
| UDP checksum 0 | as before | 0 means none was computed |
| ARP: 7-byte addresses, operation 3, another target | malformed, protocol, not-ours | |
| TCP: a data offset of 16 bytes, or past the segment; an option past the header, or of length 1 | malformed | with the checksum made right again (sysn 003) |
| TCP: the checksum changed | bad-sum | over the pseudo-header too |
| TCP: any segment for no conversation | a reset | compared without the IPv4 identification, which grows with every frame sent |
| RFC 5961 on an open conversation: resets, a SYN, an ACK of what was never sent, eleven challenges in 5 s | challenge ACK, window, throttled | segments made in tools/segment.rkt; TCP says why |
| 200 SYNs from 200 ports, then 200 ACKs with guessed cookies | a cookie each, then a reset each | every conversation still free after (sysn 008) |
| a returned cookie when every conversation is taken by peers that answered | full |
At the end, every reason has been counted at least once: the counts a server will show as files are tested too.
The host program
host/host.sysp is the stack's caller on the host: it takes one record and writes records back, and every report is one s-expression, the value the stack returned, as the stack's own types name it, written with sysl/text (sysn 007). It is proven like the stack, and sends nothing the stack did not write.
| Record | Kind | Holds |
|---|---|---|
| in | f | a frame that arrived |
| in | k, q, y | DNS (sysn 010): pick a query's id and port; ask: the server (4), sport (2), id (2), the name; read an answer: the id (2), the name's length (1), the name, the message |
| in | r | answer a frame with a destination unreachable: the code (1 byte, 2 or 3), then the frame (sysn 009) |
| in | p | a ping: to (4 bytes), id (2), seq (2), then the data |
| in | u | a datagram to send: to (4), sport (2), dport (2), then the data |
| in | c | the counts |
| in | n | the time: 8 bytes of ns, for every call after it |
| in | a, o | announce a TCP port (2); connect: to (4), port (2) |
| in | w, x, z, s | write to conversation (1) the bytes after it, kept until acknowledged; close it; abort it; its status |
| in | t, d | tick every conversation that is due; when the next is |
| in | h | a checksum (sysn 014): the length of each piece (1), then the message, summed in pieces of that length and whole: (sum (pieces "220d") (whole "220d")) |
| in | v | a frame, decoded for a person (sysn 015): the report is sysn/frame's value, (frame (dst …) (src …) (type arp) …) |
| out | f | a frame to send, as many as there are |
| out | e | the report: (echo (from 10.0.2.2) (id 1) (seq 1) (ttl 255)) |
For TCP the host program is what netd is (sysn 012): it keeps each conversation's bytes until the peer acknowledges them, letting go as many as each segment frees, and after every segment it sends what the windows now allow, until the stack writes nothing.
RFC 9293's diagram, case by case
tests/con-test.rkt drives the host program with segments made in tools/segment.rkt, no slirp, one case for every edge of the diagram but LISTEN's: both ways of opening, a simultaneous open, every way of closing, a reset in syn-rcvd, a cookie returned with data and a FIN, cookies forged, misbound or too old, the MSS a cookie says, a full table and one with a conversation in time-wait to give up, a SYN that starts a time-wait conversation again, fin-wait-2 given up after a silent minute (sysn 008), out-of-order and overlapping segments, a segment sent again at the deadline with the timeout doubled, giving up after 100 s, time-wait's end, a shut window probed. Each case starts a fresh stack at 1 s by the time it gives, and reads the state back with (status (c 0)).
tests/dns-test.rkt gives the host program DNS answers made by hand (sysn 010): the query written for a name, byte by byte; names that are not host names refused; an id and port picked anew after every frame; an A record, a CNAME chain, no address, a failure, a truncated answer; someone else's answer; pointers that loop, point forward or past the end; records, labels and counts that do not fit; a name of more than 255 bytes; and an answer cut at every length, always read as bad. And the resolver's guarantees (sysn 028): a CNAME chain that loops ends in none, a count of 65,535 over four records is malformed at once, the same answer twenty times for the same bytes, and no loop in net/dns.sysp without a fixed bound.
tests/icmp-test.rkt does the same for ICMP errors (sysn 009): the unreachable the stack writes when asked, checked byte by byte and its checksum; the packets RFC 1122 says no error may answer, each refused; a port unreachable ending a conversation in syn-sent, and soft once open; an error about no byte in flight dropped; fragmentation needed lowering the MSS; a time exceeded for a datagram; and an error cut at every length, always dropped.
tests/sum-test.rkt takes the checksum in pieces (sysn 014), the way sysn/sum takes a file: every message up to 70 bytes, cut in pieces of 1 to 9 bytes and whole, against RFC 1071 and ones-sum, so a word cut between two pieces is summed as one; RFC 1071's own example; and a recorded IPv4 header, which carries its checksum and gives 0000. The host makes the state for each record, so host-step allocates: kept in the host, the state's invariant went with every branch, and the step's proof grew twentyfold.
tests/frame-test.rkt decodes frames for a person (sysn 015): every frame of every recording, read back as one value whose addresses, type and length are the bytes' own, and every IPv4 packet's sum right; the ping recording's first frame, the stack's ARP request, exactly; every echo reply and TCP segment, field by field; a TCP segment cut at every length, as netd keeps the start of a frame, always one value and (cut) while its headers are not all there; a type the stack does not know, by its number; and a frame of 1,024 bytes, the longest the command takes. And the DNS message a datagram to or from port 53 carries (sysn 023): the recorded query and answer exactly; the answer cut at every length; a CNAME pointing into the question, a name pointing at itself, a label past the message; 50 records, which end in (more); the longest names in the question and in CNAMEs; and 300 random messages, each frame one value with its own length.