The stack · one file per protocol

A frame, layer by layer

A frame is a run of bytes with headers nested in it: Ethernet's, then ARP's or IPv4's, then ICMP's, UDP's or TCP's, then data. Each protocol is one file of net/ (TCP is two: TCP; DNS, above UDP, has its own page: DNS), and each takes its own header, checks it, and hands what it carries to the next. Here are the frames of the recordings, every byte labelled.

The bytes

Pick a frame: those slirp sent, and those sysn sent back. Select a byte to see the field it belongs to and what the stack does with it. Bytes past the packet's own length are padding, to Ethernet's 60-byte minimum, and not part of it.

Reading untrusted bytes

Every number is read and written through sysl/bytes, the suite's numbers in buffers, most significant byte first (network order): bytes-get-be16, -be32, -be48 and their writers (sysn 007; sysf reads its disk the same way). Each reads only within its buffer, by its precondition, so a caller has to prove the bytes are there before it reads them: that is how a frame cut short at any length is caught, as short, and never read past. A read gives a word, the bits as they are; a length or a port is made a number with as i64, whose range, 0 to 65535, sysp knows. UDP's header is said once more simply, since sysn 034: declared as a layout (sysp 104), (layout udp 8 (sport be16 0) (dport be16 2) (length be16 4) (sum be16 6)), from which sysp makes the struct Udp, udp-put and udp-get, proven to write and read exactly those bytes: a get after a put gives the header back, and no header has two writings. What the fields mean, a length within the packet and a sum that checks, is still the protocol's to say. Here is UDP taking a datagram, its header read by udp-get:

Addresses are words, bit patterns: an IPv4 address is a w32, a hardware address the low 48 bits of a w64, so masking an address with the subnet's is one &. Lengths, ports and counts are numbers, whose arithmetic is exact and whose overflow would be an error.

ICMP errors

Since sysn 009 the stack writes a destination unreachable, but only when its caller asks: the caller knows which UDP ports are held and which protocols it serves, and it has the clock to say how many errors to send (RFC 1812 4.3.2.8). net-unreachable quotes the packet, as much as fits a 576-byte datagram, and refuses what RFC 1122 3.2.2 says no error may answer:

An error that arrives quotes the header of a packet the stack sent and the first 8 bytes it carried: enough for the ports and, for TCP, the sequence number. take-icmp-error checks the quote is whole and ours, and then:

The checksum, worked

IPv4, ICMP, UDP and TCP each carry the Internet checksum: the ones' complement sum of 16-bit words, carries added back in. A sender puts the complement of the sum in the field, so an intact message sums to 0xffff. Here is the selected frame's IPv4 header, summed as ones-sum sums it:

The sum of up to 32,767 words fits in 32 bits, and two folds bring it to 16: fold says so in its contract, and the verifier proves it. UDP's and TCP's sums start from a pseudo-header, the addresses, the protocol and the length, so a datagram or a segment delivered to the wrong host fails it.

The same sum is a command at sysk's shell (sysn 014): sysn/sum FILE says the checksum of a file, the value its field would hold, so a file that holds a header with its checksum intact gives 0000. The file server sends a file a payload at a time, and a 16-bit word can be cut between two payloads. sum-add keeps a word's first byte in the state until its second comes, where BSD's in_cksum swaps the next buffer's bytes and Linux rotates its partial sum: one comparison a byte, and nothing for the verifier to reason about but the state's bounds. Folding after every word keeps the sum below 2¹⁶, so a file of any length is summed.

/% echo (milk eggs) > /shopping
/% sysn/sum /shopping
(sum "0d21")
job ended

A frame, decoded at the shell

sysn/frame FILE says what a frame holds, field by field, as one value (sysn 015): net/frame.sysp reads Ethernet's header, then ARP's or IPv4's, then ICMP's, UDP's or TCP's, each a function that hands the next its offset and where the packet ends, as Plan 9's snoopy hands each protocol's module what it carries. TCP's flags are letters, as tcpdump writes them. It takes the file whole, through sysk's runner (sysk 090), up to 1,024 bytes: the frame, the value and the runner's two messages fit a job's 4,096 bytes of heap.

Something to read comes from netd: each conversation in /net has a file last, the first 160 bytes of the last frame that came for it, as they came. Only frames the conversation already receives: a holder sees its own traffic and nobody else's, so last needs no right beyond holding the conversation. Every frame of the card would be capture, which sysk's authority.md keeps for an operator, recorded in an audit. A conversation lives while it is held, and the shell runs one job at a time, so no job can read a conversation's last yet: while a ping runs, sysn/frame is refused as busy, and after it the conversation is gone. last waits for jobs side by side (sysk's directions.md); the shell's own ls sees it meanwhile. Here is what frame says of the ping recording's first echo reply, of a TCP segment, and of that segment cut at 40 bytes, inside its TCP header, through the host program (tests/frame-test.rkt):

(frame (dst 52:54:00:12:34:56) (src 52:55:0a:00:02:02) (type ipv4)
  (from 10.0.2.2) (to 10.0.2.15) (ttl 255) (proto icmp) (sum ok)
  (icmp echo-reply) (code 0) (id 1) (seq 1) (bytes 60))
(frame (dst 52:54:00:12:34:56) (src 52:55:0a:00:02:02) (type ipv4)
  (from 10.0.2.2) (to 10.0.2.15) (ttl 64) (proto tcp) (sum ok)
  (sport 52121) (dport 63044) (seq 64001) (ack 3443826884) (flags SA)
  (window 65535) (data 0) (bytes 60))
(frame (dst 52:54:00:12:34:56) (src 52:55:0a:00:02:02) (type ipv4)
  (from 10.0.2.2) (to 10.0.2.15) (ttl 64) (proto tcp) (sum ok) (cut)
  (bytes 40))

A frame netd keeps is cut at 160 bytes, so the decoder says (cut) where a header, or the packet its length claims, is not all there, and decodes what is, as Wireshark marks a packet the capture cut short; a whole packet too short for the header it says it carries is (short).

A UDP datagram to or from port 53 carries a DNS message, and the decoder says it too (sysn 023), as snoopy's and tcpdump's DNS printers do inside the frame rather than as a command of its own: nothing on the system holds a DNS message but the frame that brought it. It says the message's id, whether it is a query or a reply and the reply's rcode, the first question's name and type, then each answer record: an address with its TTL, a CNAME's name, the type of any other. The recorded answer from slirp's resolver (DNS), the IPv4 and UDP fields left out:

(frame ... (sport 53) (dport 54115) (length 69)
  (dns (id 33844) (reply) (rcode 0) (name example.com) (qtype a)
    (a 104.20.23.154 276) (a 172.66.147.243 276))
  (bytes 103))

A name is read as the resolver reads one (RFC 9267): a pointer must point before the last place a pointer led, a label must fit the message, and a name stops at 255 bytes, so a name that loops or overruns is said as far as it holds. A byte that is not a letter, digit, hyphen or underscore is written ?, so a name is always one word. The value has 512 bytes: a name stops at a label's end 64 bytes before them, and records stop with (more) when the next might not fit, so what closes the value always has room. A record that does not fit its message ends them, said (bad) when the packet is whole.

Nothing is read outside the frame, whatever it holds: each header's fields are read only after the frame is shown to be long enough for them, and a length the frame claims is believed only as far as the frame goes. tests/frame-test.rkt decodes every recorded frame and every cut of one, and DNS messages that loop, overrun, hold the longest names, more records than fit, and random bytes (Tested).

Each protocol, a file

IPv4 checks in a fixed order, and the first that fails names the drop. Options are skipped (the header's length says where the payload starts), and a packet cut by the frame, or padded by it, is measured by its own total length. The checks are a function of their own, ip-head, apart from where the packet goes next (take-packet): proven together, they were most of the stack's proof work (221 million of z3's units of work), and apart they cost a quarter of a million (sysn 011).