(scratch) test: track RFC 4787, and state its requirements as executable contracts

.cargo/mutants.toml

@@ -0,0 +1,35 @@
+# Configuration for cargo-mutants (https://mutants.rs).
+#
+# Mutation testing is a flashlight, not a gate: it is run by hand over a crate
+# or a diff, and the product is the list of survivors rather than the score.
+# Nothing in CI depends on this file.
+#
+# Two categories are excluded because a survivor there is noise rather than a
+# finding. Both are excluded here rather than with `#[mutants::skip]` so that
+# production crates take no dependency on the tool and the reasoning stays in
+# one place.
+
+exclude_re = [
+    # Printers. The standing rule is "don't test printers": asserting on
+    # rendered output is sisyphean, produces low signal, and breaks whenever
+    # anyone adjusts a column. A mutated `fmt` that no test notices is telling
+    # us the rule is being followed.
+    "<impl Display for",
+    "<impl Debug for",
+    "<impl std::fmt::Display for",
+    "<impl std::fmt::Debug for",
+
+    # Test-support code inside the crate under test. The workspace convention
+    # puts bolero generators in a `contract` module next to the type they
+    # generate, so cargo-mutants finds them and mutates the test harness at
+    # itself. A generator that draws a different distribution is not a defect
+    # in the code under test; the properties are what judge it.
+    "contract::",
+]
+
+exclude_globs = [
+    # Privileged sysfs manipulation. Exercising the write path needs root and a
+    # real sysfs, and the read path is thin enough that a property would assert
+    # little beyond what the type system already does.
+    "sysfs/**",
+]

.duvet/.gitignore

@@ -0,0 +1 @@
+reports/

.duvet/config.toml

@@ -0,0 +1,46 @@
+# duvet: specification compliance coverage.
+#
+# `duvet report` matches citations in the source -- `//= <url>` followed by the requirement text --
+# against the requirements duvet extracts from the specification, so a requirement with nothing
+# implementing it, or an implementation with nothing testing it, is visible.
+#
+# Everything under .duvet/ is committed except `reports/`. That is not incidental: `duvet report`
+# reads the specification from `.duvet/specifications/` and only reaches the network when it is
+# missing, so vendoring the text is what lets the report run in a nix build sandbox at all. It also
+# means an errata, a reformat, or a fetch that quietly returns something else arrives as a
+# reviewable diff rather than as a change in results nobody can explain.
+'$schema' = "https://awslabs.github.io/duvet/config/v0.4.0.json"
+
+# Every crate in the workspace. The generated default is `src/**/*.rs`, which matches nothing here.
+[[source]]
+pattern = "*/src/**/*.rs"
+
+# RFC 4884 is the first specification tracked, because the code already cites it: the
+# "original datagram" length checks in net/src/headers/embedded.rs were found to contradict it.
+[[specification]]
+source = "https://www.rfc-editor.org/rfc/rfc4884"
+
+# RFC 5382 states 10 numbered requirements (REQ-1 .. REQ-10) for how a NAT must treat TCP. It
+# constrains values this codebase already has and chose without reference to it -- notably the
+# idle timeouts in nat/src/masquerade/nf.rs. Tracked second for that reason.
+[[specification]]
+source = "https://www.rfc-editor.org/rfc/rfc5382"
+
+[report.html]
+enabled = true
+
+# The snapshot is the regression gate. It is line-oriented and diffs cleanly, and its unit is a
+# sentence somebody else wrote -- which, unlike a mutant's file:line, does not move when a function
+# is reformatted.
+[report.snapshot]
+enabled = true
+
+# RFC 4787 is the UDP counterpart of RFC 5382 and states 14 numbered requirements. Tracked third
+# because masquerade translates UDP on the same path it translates TCP, so its mapping and timeout
+# requirements land on code that already carries RFC 5382 citations.
+#
+# Cited as the individual RFC, never as BCP 127. That composite concatenates RFC 4787, RFC 6888 and
+# RFC 7857, whose section numbers collide, and duvet silently keeps only the last -- 42 requirements
+# where the three separately yield 129. See development/code/spec-compliance.md.
+[[specification]]
+source = "https://www.rfc-editor.org/rfc/rfc4787"

.duvet/requirements/www.rfc-editor.org/rfc/rfc4787/section-10.toml

@@ -0,0 +1,44 @@
+target = "https://www.rfc-editor.org/rfc/rfc4787#section-10"
+
+# Fragmentation of Outgoing Packets
+#
+#    When the MTU of the adjacent link is too small, fragmentation of
+#    packets going from the internal side to the external side of the NAT
+#    may occur.  This can occur if the NAT is doing Point-to-Point over
+#    Ethernet (PPPoE), or if the NAT has been configured with a small MTU
+#    to reduce serialization delay when sending large packets and small
+#    higher-priority packets, or for other reasons.
+# 
+#    It is worth noting that many IP stacks do not use Path MTU Discovery
+#    with UDP packets.
+# 
+#    The packet could have its Don't Fragment bit set to 1 (DF=1) or 0
+#    (DF=0).
+# 
+#    REQ-13:  If the packet received on an internal IP address has DF=1,
+#       the NAT MUST send back an ICMP message "Fragmentation needed and
+#       DF set" to the host, as described in [RFC0792].
+# 
+#       a) If the packet has DF=0, the NAT MUST fragment the packet and
+#          SHOULD send the fragments in order.
+# 
+#    Justification:  This is as per RFC 792.
+# 
+#       a) This is the same function a router performs in a similar
+#          situation [RFC1812].
+
+[[spec]]
+level = "MUST"
+quote = '''
+REQ-13:  If the packet received on an internal IP address has DF=1,
+the NAT MUST send back an ICMP message "Fragmentation needed and
+DF set" to the host, as described in [RFC0792].
+'''
+
+[[spec]]
+level = "MUST"
+quote = '''
+a) If the packet has DF=0, the NAT MUST fragment the packet and
+SHOULD send the fragments in order.
+'''
+

.duvet/requirements/www.rfc-editor.org/rfc/rfc4787/section-11.toml

@@ -0,0 +1,51 @@
+target = "https://www.rfc-editor.org/rfc/rfc4787#section-11"
+
+# Receiving Fragmented Packets
+#
+#    For a variety of reasons, a NAT may receive a fragmented packet.  The
+#    IP packet containing the header could arrive in any fragment,
+#    depending on network conditions, packet ordering, and the
+#    implementation of the IP stack that generated the fragments.
+# 
+#    A NAT that is capable only of receiving fragments in order (that is,
+#    with the header in the first packet) and forwarding each of the
+#    fragments to the internal host is described as "Received Fragments
+#    Ordered".
+# 
+#    A NAT that is capable of receiving fragments in or out of order and
+#    forwarding the individual fragments (or a reassembled packet) to the
+#    internal host is referred to as "Receive Fragments Out of Order".
+#    See the Security Considerations section of this document for a
+#    discussion of this behavior.
+# 
+#    A NAT that is neither of these is referred to as "Receive Fragments
+#    None".
+# 
+#    REQ-14:  A NAT MUST support receiving in-order and out-of-order
+#       fragments, so it MUST have "Received Fragment Out of Order"
+#       behavior.
+# 
+#       a) A NAT's out-of-order fragment processing mechanism MUST be
+#          designed so that fragmentation-based DoS attacks do not
+#          compromise the NAT's ability to process in-order and
+#          unfragmented IP packets.
+# 
+#    Justification:  See Security Considerations.
+
+[[spec]]
+level = "MUST"
+quote = '''
+REQ-14:  A NAT MUST support receiving in-order and out-of-order
+fragments, so it MUST have "Received Fragment Out of Order"
+behavior.
+'''
+
+[[spec]]
+level = "MUST"
+quote = '''
+a) A NAT's out-of-order fragment processing mechanism MUST be
+designed so that fragmentation-based DoS attacks do not
+compromise the NAT's ability to process in-order and
+unfragmented IP packets.
+'''
+