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). 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, 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.
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 |
| TCP | 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 |
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. It is proven like the stack, and sends nothing the stack did not write.
| Record | Kind | Holds |
|---|---|---|
| in | f | a frame that arrived |
| 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 |
| out | f | a frame to send, when there is one |
| out | e | the report: (echo (from 10.0.2.2) (id 1) (seq 1) (ttl 255)) |