diff --git a/acl-filter/src/fuzz.rs b/acl-filter/src/fuzz.rs index 156fbe82c9..04fc51239a 100644 --- a/acl-filter/src/fuzz.rs +++ b/acl-filter/src/fuzz.rs @@ -127,6 +127,22 @@ fn resolved_action(rule: Option, default: Option) -> A rule.map_or_else(|| default.unwrap_or(AclAction::Allow), |v| v.action) } +/// The action the configuration alone says applies to a packet. +/// +/// The three steps above composed: first matching rule, else the peering's default, else allow. +/// Exported for `nf_fuzz`, which asks the same oracle the same question about a real packet -- so +/// that the network function is compared against this oracle rather than against a second copy of +/// it. +pub(crate) fn oracle_resolved_action( + overlay: &ValidatedOverlay, + packet: &PacketSummary, +) -> AclAction { + resolved_action( + oracle_lookup(overlay, packet), + oracle_default_action(overlay, packet.src_vni, packet.dst_vni), + ) +} + // ------------------------------------------------------------------------------------------------- // Properties. diff --git a/acl-filter/src/lib.rs b/acl-filter/src/lib.rs index 3e17f71453..d4fe2c6f40 100644 --- a/acl-filter/src/lib.rs +++ b/acl-filter/src/lib.rs @@ -26,6 +26,8 @@ mod fuzz; #[cfg(test)] mod fuzz_gen; #[cfg(test)] +mod nf_fuzz; +#[cfg(test)] mod tests; pub use access::{ diff --git a/acl-filter/src/nf_fuzz.rs b/acl-filter/src/nf_fuzz.rs new file mode 100644 index 0000000000..3e5b7ddd0a --- /dev/null +++ b/acl-filter/src/nf_fuzz.rs @@ -0,0 +1,342 @@ +// SPDX-License-Identifier: Apache-2.0 +// Copyright Open Network Fabric Authors + +//! The ACL properties, carried from the lookup to the network function. +//! +//! `fuzz.rs` already has the strongest oracle in this codebase: it evaluates the validated +//! configuration directly and compares that against the lowered tables, so a lowering mistake cannot +//! hide behind the thing it produced. What it does not touch is a packet. Every probe there is a +//! [`PacketSummary`] handed straight to `lookup`. +//! +//! Two pieces of production code sit between a packet and that summary, and neither had any +//! coverage from a generated configuration: +//! +//! * **`PacketSummary::try_from`**, which reads the five-tuple and the two discriminants out of the +//! headers. A summary is six fields, and a stage that read the destination where the source +//! belongs would pass every property in `fuzz.rs` -- they never build the packet it misreads. +//! * **`AclFilter::process_packet`**, which turns a verdict into a fate: `DoneReason::AclDropped`, +//! `invalidate_flows`, and the `is_overlay` gate deciding whether any of it happens. +//! +//! So this module re-points the existing generators rather than writing new ones. The +//! [`OverlaySpec`] and [`ProbeSpec`] are the same; what differs is that a probe becomes a packet and +//! the answer is read off the packet's fate rather than returned from a function. +//! +//! # Why the verdict is still not predicted here +//! +//! `oracle_verdict` is the config-semantics oracle from `fuzz.rs`, unchanged. This module does not +//! reimplement it -- it asks the same oracle the same question and checks that the *stage* agrees, +//! which makes this a differential test over the packet path rather than a second ACL. + +#![cfg(test)] + +use crate::fuzz::oracle_resolved_action; +use crate::fuzz_gen::{OverlaySpec, ProbeSpec}; +use crate::{AclFilter, AclFilterContext, AclFilterContextWriter, PacketSummary}; +use concurrency::sync::atomic::{AtomicUsize, Ordering}; +use config::external::overlay::acl::AclAction; +use net::buffer::TestBuffer; +use net::ip::{NextHeader, UnicastIpAddr}; +use net::packet::test_utils::{ + build_test_ipv4_packet_with_transport, build_test_ipv6_packet_with_transport, +}; +use net::packet::{DoneReason, Packet, VpcDiscriminant}; +use net::tcp::port::TcpPort; +use net::udp::UdpPort; +use pipeline::NetworkFunction; +use std::net::IpAddr; + +/// The fewest arriving probes any property may see before it is considered vacuous. +const MIN_REACHED: usize = 8; + +/// Probes per configuration. +const PROBES: usize = 8; + +/// Build a packet carrying a summary's five-tuple and discriminants. +/// +/// Returns `None` for a protocol with no port builder. TCP and UDP are what carry ports and so what +/// the port half of every ACL rule is about; a probe drawing ICMP or an arbitrary next header is +/// counted and skipped rather than approximated, since a packet whose headers do not match the +/// summary it came from would make every disagreement below meaningless. +fn packet_for(summary: &PacketSummary) -> Option> { + let (sport, dport) = summary.ports?; + let tcp = match summary.proto { + NextHeader::TCP => true, + NextHeader::UDP => false, + _ => return None, + }; + + let mut packet = match (summary.src_ip, summary.dst_ip) { + (IpAddr::V4(_), IpAddr::V4(_)) => { + build_test_ipv4_packet_with_transport(64, Some(summary.proto)).ok()? + } + (IpAddr::V6(_), IpAddr::V6(_)) => { + build_test_ipv6_packet_with_transport(64, Some(summary.proto)).ok()? + } + // The generator's `CrossVersion` stray produces these on purpose. There is no such packet + // to build, so the case belongs to the summary-level properties. + _ => return None, + }; + + packet + .set_ip_source(UnicastIpAddr::try_from(summary.src_ip).ok()?) + .ok()?; + packet.set_ip_destination(summary.dst_ip).ok()?; + if tcp { + packet + .set_tcp_source_port(TcpPort::new_checked(sport.max(1)).ok()?) + .ok()?; + packet + .set_tcp_destination_port(TcpPort::new_checked(dport.max(1)).ok()?) + .ok()?; + } else { + packet + .set_udp_source_port(UdpPort::new_checked(sport.max(1)).ok()?) + .ok()?; + packet + .set_udp_destination_port(UdpPort::new_checked(dport.max(1)).ok()?) + .ok()?; + } + + let meta = packet.meta_mut(); + meta.src_vpcd = Some(VpcDiscriminant::from_vni(summary.src_vni)); + meta.dst_vpcd = Some(VpcDiscriminant::from_vni(summary.dst_vni)); + meta.set_overlay(true); + meta.set_keep(true); + Some(packet) +} + +/// The summary a built packet actually carries, with its ports normalized the way the builder did. +fn expected_summary(summary: &PacketSummary) -> PacketSummary { + let mut expected = summary.clone(); + expected.ports = summary.ports.map(|(s, d)| (s.max(1), d.max(1))); + expected +} + +fn filter(built: &crate::fuzz_gen::BuiltOverlay) -> AclFilter { + let writer = AclFilterContextWriter::new(); + writer.store(AclFilterContext::for_test(&built.overlay)); + AclFilter::new("nf-fuzz-acl-filter", writer.get_reader()) +} + +/// How much of a run reached the code under test. +#[derive(Default)] +struct Tally { + drawn: AtomicUsize, + reached: AtomicUsize, + denied: AtomicUsize, +} + +impl Tally { + /// Assert the run was not vacuous. + /// + /// Both floors are **ratios**, not absolute counts. An absolute floor measures how fast the + /// machine was: a property reaching ten thousand probes on its own reaches a few hundred beside + /// nine hundred other tests under coverage instrumentation, and a floor tuned to the fast case + /// then fails for a reason unrelated to the code under test. + /// + /// The denial ratio matters as much as the arrival one and is easy to miss. A run that only ever + /// saw permits would pass every assertion below while the drop path -- the only path where the + /// stage does anything at all -- went entirely unexercised. + fn report(&self, what: &str) { + let (drawn, reached, denied) = ( + self.drawn.load(Ordering::Relaxed), + self.reached.load(Ordering::Relaxed), + self.denied.load(Ordering::Relaxed), + ); + println!("{what}: {reached}/{drawn} probes became packets, {denied} of them denied"); + assert!( + reached >= MIN_REACHED && reached * 4 >= drawn, + "only {reached} of {drawn} probes became packets, so the {what} assertion is barely \ + running" + ); + assert!( + denied * 20 >= reached, + "only {denied} of {reached} probes were denied, so the drop path is barely exercised \ + and this property is mostly checking that nothing happens" + ); + } +} + +/// The stage's verdict on a packet is the configuration's verdict on its five-tuple. +/// +/// The claim `fuzz.rs` makes about the tables, carried to where it is observable: a denied packet is +/// dropped and says `AclDropped`, a permitted one survives untouched. +/// +/// This is where the summary extraction is tested, and it is tested implicitly rather than by +/// inspection -- if `PacketSummary::try_from` read any of the six fields from the wrong place, the +/// stage would look up a different tuple from the one the oracle judged, and the two would disagree +/// on the probes where that field decides the answer. The generator's near-miss strays exist to make +/// those probes common. +#[test] +fn the_stage_agrees_with_the_configuration() { + let tally = Tally::default(); + + bolero::check!() + .with_type::<(OverlaySpec, [ProbeSpec; PROBES])>() + .for_each(|(overlay_spec, probe_specs)| { + let built = overlay_spec.build(); + let mut acl = filter(&built); + + for probe_spec in probe_specs { + tally.drawn.fetch_add(1, Ordering::Relaxed); + let summary = probe_spec.resolve(&built); + let Some(packet) = packet_for(&summary) else { + continue; + }; + + let want = oracle_resolved_action(&built.overlay, &summary); + let out: Vec<_> = acl.process(std::iter::once(packet)).collect(); + let got = out[0].get_done(); + + match want { + AclAction::Deny => { + assert_eq!( + got, + Some(DoneReason::AclDropped), + "the configuration denies {summary:?} and the stage let it through \ + with {got:?}\nspec: {overlay_spec:?}" + ); + tally.denied.fetch_add(1, Ordering::Relaxed); + } + AclAction::Allow => { + assert_eq!( + got, None, + "the configuration allows {summary:?} and the stage dropped it for \ + {got:?}\nspec: {overlay_spec:?}" + ); + } + } + tally.reached.fetch_add(1, Ordering::Relaxed); + } + }); + + tally.report("stage verdict"); +} + +/// The five-tuple the stage reads back is the one the packet was built with. +/// +/// The previous property tests the extraction only where a misread field changes a verdict. This one +/// tests it directly, which catches the misread that happens to be harmless for the configuration +/// drawn -- a field read from the wrong place is a defect whether or not this particular ruleset +/// notices. +#[test] +fn the_summary_survives_the_round_trip_through_a_packet() { + let tally = Tally::default(); + + bolero::check!() + .with_type::<(OverlaySpec, [ProbeSpec; PROBES])>() + .for_each(|(overlay_spec, probe_specs)| { + let built = overlay_spec.build(); + + for probe_spec in probe_specs { + tally.drawn.fetch_add(1, Ordering::Relaxed); + let summary = probe_spec.resolve(&built); + let Some(packet) = packet_for(&summary) else { + continue; + }; + + let read = PacketSummary::try_from(&packet) + .unwrap_or_else(|e| panic!("a built packet did not yield a summary: {e:?}")); + let expected = expected_summary(&summary); + + assert_eq!( + (read.src_vni, read.dst_vni), + (expected.src_vni, expected.dst_vni), + "discriminants came back swapped or wrong\nspec: {overlay_spec:?}" + ); + assert_eq!( + (read.src_ip, read.dst_ip), + (expected.src_ip, expected.dst_ip), + "addresses came back swapped or wrong\nspec: {overlay_spec:?}" + ); + assert_eq!( + read.proto, expected.proto, + "protocol came back wrong\nspec: {overlay_spec:?}" + ); + assert_eq!( + read.ports, expected.ports, + "ports came back swapped or wrong\nspec: {overlay_spec:?}" + ); + tally.reached.fetch_add(1, Ordering::Relaxed); + // The drop path is not this property's subject; borrow the floor. + tally.denied.fetch_add(1, Ordering::Relaxed); + } + }); + + tally.report("summary round trip"); +} + +/// A packet with no discriminants is dropped, and says why. +/// +/// `PacketSummary::try_from` returns `DoneReason::Unroutable` for it, and that is the whole of what +/// the stage can do -- an ACL is indexed by the vpc pair, so a packet that names neither cannot be +/// judged at all. Letting it through would apply no policy to it whatsoever, which is the failure +/// this rules out. +#[test] +fn a_packet_with_no_discriminants_is_dropped() { + let tally = Tally::default(); + + bolero::check!() + .with_type::<(OverlaySpec, [ProbeSpec; PROBES])>() + .for_each(|(overlay_spec, probe_specs)| { + let built = overlay_spec.build(); + let mut acl = filter(&built); + + for probe_spec in probe_specs { + tally.drawn.fetch_add(1, Ordering::Relaxed); + let summary = probe_spec.resolve(&built); + let Some(mut packet) = packet_for(&summary) else { + continue; + }; + packet.meta_mut().dst_vpcd = None; + + let out: Vec<_> = acl.process(std::iter::once(packet)).collect(); + assert_eq!( + out[0].get_done(), + Some(DoneReason::Unroutable), + "a packet with no destination vpc was not refused\nspec: {overlay_spec:?}" + ); + tally.reached.fetch_add(1, Ordering::Relaxed); + tally.denied.fetch_add(1, Ordering::Relaxed); + } + }); + + tally.report("missing discriminant"); +} + +/// A packet that is not overlay traffic is left alone. +/// +/// The stage's gate. Underlay traffic is not indexed by a vpc pair and no ACL in the configuration +/// describes it, so applying one would be applying a policy to traffic it was never written for. +#[test] +fn underlay_traffic_is_not_judged() { + let tally = Tally::default(); + + bolero::check!() + .with_type::<(OverlaySpec, [ProbeSpec; PROBES])>() + .for_each(|(overlay_spec, probe_specs)| { + let built = overlay_spec.build(); + let mut acl = filter(&built); + + for probe_spec in probe_specs { + tally.drawn.fetch_add(1, Ordering::Relaxed); + let summary = probe_spec.resolve(&built); + let Some(mut packet) = packet_for(&summary) else { + continue; + }; + packet.meta_mut().set_overlay(false); + + let out: Vec<_> = acl.process(std::iter::once(packet)).collect(); + assert_eq!( + out[0].get_done(), + None, + "a packet that is not overlay traffic was judged by an overlay acl\nspec: \ + {overlay_spec:?}" + ); + tally.reached.fetch_add(1, Ordering::Relaxed); + tally.denied.fetch_add(1, Ordering::Relaxed); + } + }); + + tally.report("underlay gate"); +} diff --git a/config/src/external/overlay/vpcpeering.rs b/config/src/external/overlay/vpcpeering.rs index 09336ae3a6..d8aae9f377 100644 --- a/config/src/external/overlay/vpcpeering.rs +++ b/config/src/external/overlay/vpcpeering.rs @@ -1136,37 +1136,73 @@ pub mod contract { #[derive(Debug, Clone, Copy, Default)] pub struct MasqueradeExpose; + /// Several masquerade exposes for one manifest, which a manifest will accept together. + /// + /// The same two problems [`StaticNatExposes`] solves, for the same reasons. [`MasqueradeExpose`] + /// draws its base index freely, so two of them collide whenever their index ranges intersect -- + /// which is often, since each covers up to three consecutive indices. Here each expose gets a + /// slot of [`MASQUERADE_SLOT`] indices, wider than the widest one can occupy, and the address + /// family is drawn once and shared. + #[derive(Debug, Clone, Copy)] + pub struct MasqueradeExposes(pub u8); + + impl Default for MasqueradeExposes { + fn default() -> Self { + Self(3) + } + } + + /// Indices reserved per expose. [`MasqueradeExpose`] uses at most three consecutive ones. + const MASQUERADE_SLOT: u8 = 4; + + impl ValueGenerator for MasqueradeExposes { + type Output = Vec; + + fn generate(&self, driver: &mut D) -> Option> { + let v4 = driver.produce::()?; + let count = driver.gen_u8(Included(&1), Included(&self.0.max(1)))?; + (0..count) + .map(|slot| masquerade_expose(driver, v4, slot.wrapping_mul(MASQUERADE_SLOT))) + .collect() + } + } + impl ValueGenerator for MasqueradeExpose { type Output = VpcExpose; fn generate(&self, driver: &mut D) -> Option { let v4 = driver.produce::()?; - let privates = driver.gen_u8(Included(&1), Included(&3))?; - let publics = driver.gen_u8(Included(&1), Included(&2))?; let base = driver.produce::()?; - let idle_timeout = match driver.gen_u8(Included(&0), Included(&2))? { - 0 => None, - 1 => Some(Duration::from_secs(30)), - _ => Some(Duration::from_mins(2)), - }; + masquerade_expose(driver, v4, base) + } + } + + /// One masquerade expose of the given family, from the given base index. + fn masquerade_expose(driver: &mut D, v4: bool, base: u8) -> Option { + let privates = driver.gen_u8(Included(&1), Included(&3))?; + let publics = driver.gen_u8(Included(&1), Included(&2))?; + let idle_timeout = match driver.gen_u8(Included(&0), Included(&2))? { + 0 => None, + 1 => Some(Duration::from_secs(30)), + _ => Some(Duration::from_mins(2)), + }; - let mut expose = VpcExpose::empty().make_masquerade(idle_timeout).ok()?; - for index in 0..privates { - expose = expose.ip(PrefixWithOptionalPorts::new( - block(v4, Side::Private, base.wrapping_add(index))?, + let mut expose = VpcExpose::empty().make_masquerade(idle_timeout).ok()?; + for index in 0..privates { + expose = expose.ip(PrefixWithOptionalPorts::new( + block(v4, Side::Private, base.wrapping_add(index))?, + None, + )); + } + for index in 0..publics { + expose = expose + .as_range(PrefixWithOptionalPorts::new( + block(v4, Side::Public, base.wrapping_add(index))?, None, - )); - } - for index in 0..publics { - expose = expose - .as_range(PrefixWithOptionalPorts::new( - block(v4, Side::Public, base.wrapping_add(index))?, - None, - )) - .ok()?; - } - Some(expose) + )) + .ok()?; } + Some(expose) } #[derive(Clone, Copy)] @@ -1207,36 +1243,152 @@ pub mod contract { /// sampling. Parts are placed largest first from an aligned base, which keeps every prefix /// aligned to its own size and keeps them from overlapping. /// - /// No port ranges yet: static NAT permits them, and they take the mapping down a second path - /// (`PortAddrTranslationValue` rather than `AddrTranslationValue`) that carries its own - /// unfinished work. That path wants a generator of its own. + /// Addresses only. For the port-range form, which takes the mapping down a different path, see + /// [`StaticNatExposes::with_ports`]. #[derive(Debug, Clone, Copy, Default)] pub struct StaticNatExpose; + /// Several static NAT exposes for one manifest, which a manifest will accept together. + /// + /// [`StaticNatExpose`] draws one expose, and one expose builds a table with one rule in it. + /// Several are what give a longest-prefix match anything to choose between, so anything testing + /// a lookup wants this rather than a repeated draw of the single-expose generator. + /// + /// Two independent draws are refused by a manifest almost every time, for two reasons that both + /// have to be handled here rather than by the caller: + /// + /// * **Overlap.** Every expose is laid out from the same two bases, so two of them cover the + /// same addresses. Each is placed in a block of its own instead, [`BLOCK_STRIDE`] apart, which + /// is wider than the widest span one expose can occupy. + /// * **Address family.** A peering's manifests must agree on one family, so a v4 expose beside a + /// v6 one is refused. The family is drawn once here and shared. + /// + /// # Ports + /// + /// Static NAT permits a port range on each prefix, and that takes the mapping down a second + /// path: `NatTableValue::Pat` and `PortAddrTranslationValue` rather than + /// `NatTableValue::Nat` and `AddrTranslationValue`. The rule validation applies is that the two + /// sides cover the same **total**, counting addresses times ports -- so a `/32` carrying 64 + /// ports is a legal answer to a `/30` carrying 16, and the mapping has to run across both + /// dimensions at once. + /// + /// That asymmetry is the whole reason the path exists, so [`StaticNatExposes::with_ports`] + /// draws it deliberately: one total per expose, split into addresses and ports **independently + /// per side**. Note that this is legal for static NAT and *illegal* for port forwarding, which + /// requires the two lengths and the two port counts to match individually. + #[derive(Debug, Clone, Copy)] + pub struct StaticNatExposes { + /// The most exposes to draw. The generator draws between one and this. + pub max: u8, + /// Whether each prefix carries a port range. + pub ports: bool, + } + + impl Default for StaticNatExposes { + fn default() -> Self { + Self::addresses_only(3) + } + } + + impl StaticNatExposes { + /// Exposes whose prefixes carry no port range, mapping address to address. + #[must_use] + pub fn addresses_only(max: u8) -> Self { + Self { max, ports: false } + } + + /// Exposes whose prefixes carry port ranges, mapping address and port together. + #[must_use] + pub fn with_ports(max: u8) -> Self { + Self { max, ports: true } + } + } + /// The largest total either side covers, as a power of two. Small enough to enumerate. const MAX_TOTAL_LOG: u8 = 6; + /// The distance between two blocks. + /// + /// A side lays out at most `2^MAX_TOTAL_LOG` addresses, each part followed by a gap of its own + /// size, so it spans at most twice that. Double it again for room to grow. + const BLOCK_STRIDE: u128 = 4 << MAX_TOTAL_LOG; + impl ValueGenerator for StaticNatExpose { type Output = VpcExpose; fn generate(&self, driver: &mut D) -> Option { let v4 = driver.produce::()?; - let total_log = driver.gen_u8(Included(&0), Included(&MAX_TOTAL_LOG))?; + static_nat_expose(driver, v4, 0) + } + } - let privates = place(v4, Side::Private, &split(driver, total_log)?)?; - let publics = place(v4, Side::Public, &split(driver, total_log)?)?; + impl ValueGenerator for StaticNatExposes { + type Output = Vec; - let mut expose = VpcExpose::empty().make_static_nat().ok()?; - for prefix in privates { - expose = expose.ip(PrefixWithOptionalPorts::new(prefix, None)); - } - for prefix in publics { - expose = expose - .as_range(PrefixWithOptionalPorts::new(prefix, None)) - .ok()?; - } - Some(expose) + fn generate(&self, driver: &mut D) -> Option> { + let v4 = driver.produce::()?; + let count = driver.gen_u8(Included(&1), Included(&self.max.max(1)))?; + (0..count) + .map(|block| { + if self.ports { + static_nat_pat_expose(driver, v4, block) + } else { + static_nat_expose(driver, v4, block) + } + }) + .collect() + } + } + + /// One static NAT expose of the given family, laid out in the given block. + fn static_nat_expose(driver: &mut D, v4: bool, block: u8) -> Option { + let total_log = driver.gen_u8(Included(&0), Included(&MAX_TOTAL_LOG))?; + + let privates = place(v4, Side::Private, block, &split(driver, total_log)?)?; + let publics = place(v4, Side::Public, block, &split(driver, total_log)?)?; + + let mut expose = VpcExpose::empty().make_static_nat().ok()?; + for prefix in privates { + expose = expose.ip(PrefixWithOptionalPorts::new(prefix, None)); } + for prefix in publics { + expose = expose + .as_range(PrefixWithOptionalPorts::new(prefix, None)) + .ok()?; + } + Some(expose) + } + + /// One static NAT expose whose two sides carry port ranges. + /// + /// One prefix per side rather than a split, because the interesting asymmetry here is between + /// the two *dimensions* -- how a total is divided between addresses and ports -- and adding a + /// prefix split on top only makes the case harder to read for no new coverage. + /// + /// Each side draws its own division of the same total, so a `/32` carrying 64 ports opposite a + /// `/30` carrying 16 is a shape this produces on purpose. Both sides' port ranges start at a + /// drawn offset, so a mapping that quietly assumes the two ranges begin at the same port fails + /// here rather than in the field. + fn static_nat_pat_expose(driver: &mut D, v4: bool, block: u8) -> Option { + let total_log = driver.gen_u8(Included(&0), Included(&MAX_TOTAL_LOG))?; + + let mut side = |which| -> Option { + let port_log = driver.gen_u8(Included(&0), Included(&total_log))?; + let addr_log = total_log - port_log; + let prefix = *place(v4, which, block, &[addr_log])?.first()?; + let ports = port_range(driver, 1u16 << port_log)?; + Some(PrefixWithOptionalPorts::new(prefix, Some(ports))) + }; + + let private = side(Side::Private)?; + let public = side(Side::Public)?; + + VpcExpose::empty() + .make_static_nat() + .ok()? + .ip(private) + .as_range(public) + .ok() } // Split 2^total_log into powers of two, largest first. Halving a part keeps the total the @@ -1271,19 +1423,21 @@ pub mod contract { // Each part is followed by a gap of its own size. Placed end to end they would be aligned // siblings, and validation normalizes those back into one prefix -- so the shape the generator // worked out to differ between the sides would be collapsed away before anything saw it. - fn place(v4: bool, side: Side, parts: &[u8]) -> Option> { - let mut cursor = if v4 { - u128::from(match side { - Side::Private => 0x0A00_0000u32, - Side::Public => 0xAC10_0000, - }) - } else { - let selector = match side { - Side::Private => 0u128, - Side::Public => 1, + fn place(v4: bool, side: Side, block: u8, parts: &[u8]) -> Option> { + let offset = u128::from(block) * BLOCK_STRIDE; + let mut cursor = offset + + if v4 { + u128::from(match side { + Side::Private => 0x0A00_0000u32, + Side::Public => 0xAC10_0000, + }) + } else { + let selector = match side { + Side::Private => 0u128, + Side::Public => 1, + }; + (0x2001_0db8u128 << 96) | (selector << 80) }; - (0x2001_0db8u128 << 96) | (selector << 80) - }; let mut out = Vec::with_capacity(parts.len()); for &log in parts { diff --git a/development/code/README.md b/development/code/README.md index 7e512e6f92..8a87f3dff8 100644 --- a/development/code/README.md +++ b/development/code/README.md @@ -12,6 +12,8 @@ wrong thing. If you need to write a test, prefer [property-based tests] over simple unit tests. +For inputs too large to generate directly -- a whole configuration, say -- build them from an algebra of +valid operations and derive the oracles from that same algebra; see the [config algebra note][config-algebra]. If you need to handle errors, prefer `Result` types over panics in general, but see the [error handling guide][error] for details. @@ -21,6 +23,7 @@ If you need to [handle an error][error], follow the guidelines. [avoid-global-reasoning]: ./avoid-global-reasoning.md [property-based tests]: ./property-testing.md +[config-algebra]: ./config-algebra-testing.md [error]: ./error-handling.md ## Testing instructions diff --git a/development/code/config-algebra-testing.md b/development/code/config-algebra-testing.md new file mode 100644 index 0000000000..c2059322aa --- /dev/null +++ b/development/code/config-algebra-testing.md @@ -0,0 +1,988 @@ +# Testing a config-driven dataplane with an operation algebra + +Status: **design note, partly implemented**. It records a strategy and, more importantly, the +reasoning that rejected the alternatives, so that the next attempt does not rediscover them. + +The per-packet half of the decomposition has a first worked example in `nat/src/static_nat/probe.rs` +and `nat/src/static_nat/fuzz.rs`: packets drawn relative to a generated configuration, put through a +real network function, and judged by metamorphic relations rather than by an oracle. The operation +algebra itself -- sequences, undo, commutation from read and write sets -- is still unbuilt, and the +enactment path refactor it implies is still deferred. + +## The problem + +k8s and the config validator decide what configurations exist. The dataplane is bound by that +decision: it has no channel to tell an operator "I refused your config," so **everything which passes +the validator must in fact be enactable**. Testing that claim needs two things, and the second is the +hard one: + +1. a supply of valid configurations, and +2. a way to know whether the dataplane did the right thing with one. + +Neither is served by generating configuration values directly, and the reason generalises. + +## Why not generate configurations directly + +A [`TypeGenerator`] over the config types produces values that are *syntactically* valid and +*semantically* nonsense: colliding VNIs, peerings between VPCs that do not exist, features named +where they are not rendered. The validator rejects nearly all of them, so a coverage-guided fuzzer +spends its budget exploring the validator's rejection paths rather than the enactment path we care +about. + +Filtering does not rescue it. To generate configs that pass validation, the generator has to encode +the validator's rules -- and then there are two copies of those rules to keep in agreement, which is a +worse problem than the one being solved. + +Reaching for a narrower [`ValueGenerator`] each time the fuzzer cannot get somewhere does not scale +either, and there is local evidence. Covering `net::headers` needed four bespoke generators -- +`ShapedHeaders`, `ShapedQuote`, `ThinHeaders`, `SometimesHeadless` -- each written because the +previous one could not reach one more shape. They do not compose, and each encodes a little more +knowledge of the implementation. At the scale of a whole configuration that pattern does not +terminate. + +## The algebra + +Build configurations by construction instead. A configuration is a fold of operations over the blank +config: + +```text +X = E . D . C . B . A where A = blank, B = add a VPC, C = add another, D = peer those two, ... +``` + +The generator draws an **operation sequence**, not a configuration. Two consequences: + +- **Preconditions become unrepresentable rather than checked.** If `peer` takes handles to VPCs that + already exist, a peering between absent VPCs cannot be expressed. This is the same move as + enforcing an invariant in the type system rather than validating it at runtime, which the + [code guidelines](./README.md) already ask for. +- **Every generated configuration is valid by construction**, so the generator never needs to know + the validator's rules. + +A partially modelled algebra yields partial coverage of the configuration space. That is a feature: +model a manageable subset, fuzz it, fix what falls out, then extend the vocabulary. What grows is the +set of operations, not a collection of single-purpose generators. + +### Checking the algebra is not lying + +The algebra reaches exactly the configurations its operations compose to, which may be a strict subset +of what the validator accepts. Configurations outside its reach are invisible to the fuzzer, and +nothing about a green run says otherwise. + +So treat the algebra's completeness as its own property: take real configurations -- from CI, from the +field -- and assert each is expressible as an operation sequence. A configuration that is not points +at a missing operation. + +## Updates come along for free + +The property "the dataplane must be able to move from config `X` to config `Y`, for all legal `X` and +`Y`" is true and useless: the space of pairs is far too sparse to fuzz. + +Generating `X => A.X` instead -- one operation applied to an already-built configuration -- exercises a +single *species* of update at a time, which is both tractable and diagnosable. The general property is +recovered by composition: `A.X`, then `B.A.X`, then `C.B.A.X`. + +The dataplane does not have to observe the intermediate states. It may be handed several operations at +once, and should be, since batching is what production does. + +### Deletion is where the bugs live + +An algebra of only additive operations will look healthy and find little. The interesting failures are +in removal and modification, because a deletion's footprint is *everything that referred to the +deleted thing*. + +Both known scars are of this kind: rollback to a blank config leaves the previous config's ACL, NAT +and flow-filter tables live (the blank path returns early, before every table writer), and the +masquerade overlap defect was a config change underneath live NAT allocations. Model removal and +modification early. + +### Every operation needs an undo, and the undo is not a function of the operation alone + +For every `A` in the algebra there should be an `A^-1` that reverses it, which buys the whole +"configuration existed and was then removed" class -- as important as the add case and much less +travelled. + +It is not a group, though, and pretending otherwise will bite. The reverse of `set_flow_table_capacity(n)` +needs the *previous* capacity, so it is a function of the operation **and the state it was applied to**, +not of the operation alone. Model it as an undo log rather than an inverse element: + +```text +apply(A, X) -> (X', undo) where undo(X') == X +``` + +Two things fall out. + +**`undo . A` is the cleanest state-leak probe available.** The configuration afterwards is provably +identical to the configuration before, so *any* difference in observable behaviour is attributable to +runtime state and nothing else. No other experiment controls for configuration that exactly, which +makes this the sharpest available test of the "never resurrected" disposition below. + +**A missing undo is a product finding, not a test gap.** An operation whose reverse is not expressible +is a configuration change an operator cannot walk back. That is an operational hazard worth reporting +even though no test failed. + +### Algebraic laws are metamorphic relations + +Calling it an algebra earns something concrete: its laws are testable. If `A` and `B` commute then +`A . B . X` and `B . A . X` must agree, and that is checkable without knowing what either produces. + +Distinguish two strengths, because conflating them manufactures false positives: + +- **Configuration-level commutation** -- the resulting configurations are equal. Cheap, and a pure + property of the `config -> tables` half. +- **Behavioural commutation** -- the resulting dataplanes behave the same. Strictly stronger, and it can + fail while the configurations are equal, *legitimately*: the two orders allocate NAT ports in + different sequences, so live flows get different translations. State the property over the observable + projection -- verdicts and reachability -- never over raw state. + +### Derive commutation from read and write sets, do not declare it + +Commutation is *not* a property of a pair of operators. `peer(A, B)` and `add_vpc(C)` commute; `peer(A, B)` +and `add_vpc(A)` cannot be swapped at all, because `peer` needs A to exist. The difference is definedness +inherited from everything earlier in the sequence, so any table of commuting pairs is wrong as soon as it +leaves the position it was written for. + +Give each operation a **read set** and a **write set** instead, and derive commutation the way a database +scheduler does: + +| conflict | commutes | +| --- | --- | +| write-write | no | +| read-write | no | +| read-read | yes | + +`peer(A, B)` reads VPC A and VPC B and writes peering AB. `add_vpc(C)` writes VPC C -- no conflict, so they +commute. `add_vpc(A)` writes VPC A, which `peer(A, B)` reads -- a read-write conflict, so they do not. +**Preconditions stop being a special case**: a precondition is exactly a read of something an earlier +operation wrote. + +This costs `O(n)` footprints rather than `O(n^2)` declarations, is independent of position, and the write +set is the same metadata the frame condition already needs. Formally this makes the sequences a trace +monoid, but none of the theory is required -- only the conflict test. + +It also generates a test family for free: two sequences related by swaps of adjacent non-conflicting +operations must produce equivalent pipelines, so the whole equivalence class of a generated sequence is +checkable. + +## Oracles as contracts + +The tempting oracle is a shadow model: give each operation an `apply_to_model()` that maintains an +expected copy of the tables, then compare. Do not. The shadow model grows into a second dataplane, it +drifts from the first, and it has to be rewritten whenever the real one is refactored. It is the same +non-composing trap as the bespoke generators, one level up. + +Instead each operation emits **claims about observable behaviour**, stated in operator-facing terms. +`peer(A, B)` claims things like "traffic from A's subnet to B's subnet is not denied", "its +translation is reversible", "no verdict involving any other VPC changed". Claims conjoin, so oracles +compose; and because they describe behaviour rather than representation, they survive a rewrite of the +representation. + +Each operation then has four parts, which are the familiar contract pieces: + +| part | what it is | where it lives | +| --- | --- | --- | +| **precondition** | the state the operation needs | unrepresentable, by construction | +| **postcondition** | positive claims the operation adds | test-side, accumulated | +| **invariant** | local consistency of the structures it touched | `debug_assert!`, in place | +| **frame** | everything outside its footprint is unchanged | test-side, probe set | + +### The frame is the highest-value part + +Overlapping NAT and ACL rules are hard to oracle absolutely: predicting which of several matching +rules wins means reimplementing the matcher. But **overlap bugs are frame violations**, and the frame +is easy to state: + +> Adding a peering for VPC A changed nothing observable for VPC B. + +That is cheap, catches the entire cross-talk class, and is completely indifferent to how NAT is +implemented. + +Frames need a probe set re-run after each operation, so the cost is `operations x probes`. Keep it +affordable by deriving probes from the algebra too: each operation contributes a handful at its own +boundary -- inside the subnet, just outside it, the adjacent prefix -- which gives relevance without +enumerating address space. + +### The peering graph indexes the frame + +VPC peering is a graph relation, and it supplies the footprint the frame needs -- which is otherwise the +awkward part to pin down. + +Two graph notions are in play and they are **not** the same: + +- **Reachability is a direct edge.** `VpcPeering` is pairwise, narrowed further by what each side's + manifest exposes and by the peering-scoped ACL. It is not transitive: peerings `A-B` and `B-C` create + no path from `A` to `C`. +- **Non-interference is a disjoint component** of the transitive closure. If `A` and `B` fall in + different components, nothing done in one can be observed in the other. + +The second is tenant isolation, and it has two halves worth stating separately: + +1. **Spatially** -- no packet confined to one component is ever observed in another. +2. **Operationally** -- no configuration change or state mutation confined to one component changes any + verdict in another. + +The second half is exactly a frame condition, indexed by graph component instead of by operation +footprint. So for the whole family of VPC operations, the connected component *is* the footprint, and +the graph tells you which probes must come back unchanged. + +This is the highest-value property in the document. It is negative, so it is cheap to state and +indifferent to implementation; it is a *security* property, so its failures differ in kind from +functional bugs; and it is stated in domain terms, so it should outlive any rewrite underneath it. + +#### The generator has to be pushed into producing disjoint components + +Peering random pairs of VPCs produces a single giant component almost immediately -- the threshold is +around one edge per VPC -- and in a connected configuration the isolation property is vacuously true +and never tested. + +So the operation vocabulary needs to distinguish "peer two VPCs already in the same component" from +"peer across two components", and the generator has to be biased toward keeping several components +alive. Count configurations with two or more components and assert on it; this is precisely the kind of +reachability failure the [vacuity](#vacuity) guard exists to catch. + +### Making an oracle composable + +An oracle is a **projection plus a predicate**: a view of the world, and a claim about that view. It +names what it needs rather than where that lives, so a refactor re-points the projection and leaves +the predicate untouched. + +There is a working example in `net/src/headers/view.rs`: the `Addrs` trait projects a tuple of layer +references of any arity down to an array of addresses, and the predicate is plain equality. One check +covering eight arities, where previously the same check had to be hand-written per arity and so +existed at only two. + +## You never need an end-to-end oracle + +The reason a whole-dataplane oracle looks intractable is that it is framed as a function oracle: given +a config and a packet, what should happen? That requires a second dataplane. Decompose instead: + +```text +config --[A]--> tables --[B]--> verdict +``` + +- **A is a pure, total function.** A differential oracle is affordable here: write a slow, obviously + correct table builder and compare. No netlink, no FRR, no pipeline needed. +- **B is per-packet.** Use metamorphic relations and invariants. + +Oracles for `A` and `B` compose. `A . B` needs no oracle of its own, which is what makes the whole +thing tractable. + +This is one of *two* independent decompositions, and they cut along different axes. This one splits +configuration handling from packet handling. The other splits packet handling across the pipeline stages -- +see [contracts belong to network functions](#contracts-belong-to-network-functions-not-to-the-dag). Both are +needed and neither substitutes for the other. + +### Metamorphic relations for the per-packet half + +Do not say what the output is; say how outputs relate under transformations of the input. + +- **ACL** -- adding a deny never widens the accepted set; adding a permit never narrows it; reordering + rules with disjoint match sets changes no verdict. +- **NAT** -- translate then reverse is the identity on the 5-tuple; distinct live flows never collide + in translated space; translation preserves protocol and payload. +- **FIB** -- adding a less specific route changes no existing decision; adding a more specific one + changes decisions only for addresses inside it; deletion is the inverse. + +Rule *precedence* is deliberately absent from that list. It looks like it needs either a +reimplementation of the matcher or an ablation sweep -- removing rules one at a time to see when the +verdict changes, at `O(n)` executions per packet. Neither is necessary: see +[the selection oracle](#the-selection-oracle-is-already-built) below. + +## The part that is not free: state across transitions + +The dataplane is **not a pure function of its configuration.** Live flows, NAT port allocations, FIB +contents and neighbour state all survive a config change. + +So passing every oracle for every legal config `X`, with the dataplane born blank under `X`, is *not* +evidence of sensible behaviour having arrived at `X` from `W` carrying `W`'s state. The masquerade +overlap defect lived exactly in that gap. + +The fix is to extend the frame from config-derived tables to **runtime state**. Each operation +classifies every piece of live state it could touch into one of three dispositions, and each is a +claim: + +1. **Preserved** -- state still legal under the new config keeps behaving identically. Same verdict, + same translation. This is what "do not break established connections" means concretely. +2. **Invalidated attributably** -- state made illegal by the operation is torn down *and observably + so*: a counted drop with a reason, never a silent blackhole. +3. **Never resurrected** -- state from the old config must not leak into decisions under the new one. + A port allocation released by a removed VPC must not be handed out while anything still refers to + it. + +There is a cheap universal approximation of all three, worth having before any of them: + +> **No silent change.** After any config operation, every live flow either behaves exactly as it did +> before, or fails with an attributable reason. Never "works differently", and never "fails silently". + +## Run the related configurations side by side + +Production would never do this, but a test harness can hold several pipelines at once -- `X`, `A.X`, +`B.A.X` -- and feed all of them the *same* packets. That turns most of the relations above from +before-and-after bookkeeping into a live comparison, and it is the mechanism that makes them affordable: + +- **Frames become direct.** Pipelines `X` and `A.X` must agree on every packet outside `A`'s footprint. + No probe set to maintain, no replay, and the disagreement names the packet. +- **Isolation becomes direct.** A configuration change confined to one peering component must leave the + other pipeline's verdicts for that component's traffic untouched, packet for packet. +- **State leakage becomes measurable.** Run `P1` at configuration `X` fed stream `S`; run `P2` at `X`, + then `A`, then some stream `S'`, then `undo`, then the same `S`. The two configurations are now + identical by construction, so any divergence on `S` is state carried through the excursion -- and that + is the "never resurrected" claim made concrete. + +Three prerequisites, all of which have already bitten this codebase once: + +1. **Seed the non-determinism.** `apply_masquerade_config` sets `randomize(true)` unconditionally, so + two pipelines will allocate different ports for the same flow and a naive comparison fails + immediately. Either seed it identically per pipeline or keep it out of the compared projection. +2. **Advance timers in lockstep.** Flow timers are already known to leak between fuzz inputs; across + concurrent pipelines they must be driven explicitly rather than by wall clock. +3. **Compare projections, not state.** Counters and port allocations legitimately differ between two + pipelines that agree on every verdict. Compare what an operator can observe. + +## When the pipeline becomes a DAG + +The network function pipeline is currently a line graph. The plan is to give it a non-trivial topology, +and that changes what has to be tested. + +Do not confuse this graph with the peering graph above. They index frames in the same way but they are +different objects: the **peering graph** is dynamic and config-driven, describing which tenants may +reach each other; the **NF DAG** is static topology, fixed when the dataplane is built. That the NF +topology is static is precisely what makes the analysis below tractable -- the graph is not part of the +state space, so what remains is per-NF generation and packets in flight. + +The DAG also supplies a second footprint for free: two NFs on disjoint paths cannot interfere. So the +frame abstraction wants to be parameterised over *which graph defines the footprint* rather than +assuming peering. + +### The property that matters: no packet sees a torn config + +In a line graph a config generation can be swapped in between packets. In a DAG a packet is at several +NFs over its lifetime, so if `NF1` is on generation `N` while `NF2` has already adopted `N+1`, the packet +gets hybrid treatment. That is not hypothetical harm: an ACL can permit under `N` while NAT translates +under `N+1`, and the packet leaves carrying a translation the newer ACL would have denied. + +There are two defensible designs and they need different proofs: + +- **Barrier** -- packets drain before an NF adopts a new generation. Property: no packet spans a barrier. +- **Permitted hybrids** -- property: every hybrid traversal is equivalent to *some* single generation. + +Deciding which is affordable is a design question, best answered before the DAG is built. + +### The design constraint that decides everything else + +> The DAG's generation-propagation logic must be a **pure state machine over a small, `Hash`-able state**, +> separate from packet processing and free of I/O. + +Honour that and the coordination logic can be model-checked *directly* -- the checker exercises the code +production runs, so it is a genuine regression suite and belongs in CI. Miss it, and adoption logic ends +up scattered across NF implementations with kernel calls interleaved; the only way to check it is then to +write a shadow model, which is worth something once as design validation and nothing thereafter. + +The constraint is cheap to honour in advance and expensive to retrofit, which is why it is written down +here rather than left until the tests are wanted. + +### Notes on stateright, if it is used for this + +[`stateright`][stateright] is an explicit-state model checker (0.31.0, June 2026; small maintainer pool +but active). Its `Model` trait is a good fit: `next_state` returns `Option`, so inapplicable actions are +`None` and preconditions fall out the same way they do in the algebra. + +Three points worth knowing before starting: + +1. **Use `Model` directly, not `ActorModel`.** The actor layer models a *network* -- loss, duplication, + reordering -- which NFs inside one process do not suffer, so it manufactures counterexamples that + cannot occur. It is also where the state space explodes. From stateright's own documentation, the same + protocol with an unordered network: + + | configuration | unique states | + | --- | --- | + | 2 servers + 2 clients | 544 | + | 3 servers + 2 clients | 37,168,889 | + + The network state is the dominant term, not the component count. Explicit bounded ordered queues keep + a three-NF, two-generation, two-packet model in the hundreds of states -- which runs in milliseconds, + as an ordinary test. + +2. **`Sometimes` properties are the vacuity guard as a language feature.** Assert that two NFs are ever + observed on different generations; without it the model may never produce the interesting interleaving + and will pass for nothing. Two more habits worth copying: `unique_state_count()` is assertable, so a + model quietly changing shape fails a test, and `assert_discovery` pins a counterexample trace as a + permanent regression -- the analogue of a fuzzer's crash corpus. + +3. **`Hash` is required but `Eq` is not**, so the visited set is keyed on the hash alone. Two + consequences: collisions can silently prune states, so a state count is a lower bound on confidence; + and any state containing a `HashMap` is unusable, because its iteration order is not reproducible. + That is not a problem for generation counters and adoption flags. It *is* the reason real flow tables + and port allocators can never be the checked state. + +Whatever the checker validates must also be re-stated as a tier 0 or tier 1 check in the NFs themselves. +The checker sees the coordination core; nothing stops an NF from ignoring what the core tells it. Same +claims, two enforcement points. + +The house pattern to copy is the quartet in `concurrency/tests/` -- `quiescent_model.rs` (loom/shuttle +interleavings), `quiescent_protocol.rs` (real threads), `quiescent_properties.rs` (bolero), and +`quiescent_shuttle.rs` (bolero x shuttle) -- and `#[concurrency::test]`, which routes one body to +whichever backend is active. Model checking already runs in CI here; this would not be a new practice. + +## Session-level oracles: let a real protocol be the oracle + +Every oracle above computes an expectation and compares. A transport protocol does not need one: run a +TCP session across the dataplane and the protocol itself decides whether the path worked. Sequence +numbers, checksums, retransmission and final byte-stream equality give a verdict with **no model of what +the dataplane should have done**. + +That is a different kind of oracle from the rest of this document, and it is strong enough that it may +retire the differential tier below -- which is the only place a reference implementation survives, and +the piece most exposed to a pipeline rewrite. + +Use [`smoltcp`][smoltcp] rather than writing a stack. It is `0BSD`, so it raises none of the licensing +problems that put FRR out of reach, and it takes its clock from the caller -- `poll(timestamp, ...)` -- +which is what makes runs deterministic, replayable, and advanceable in lockstep across the parallel +pipelines above. A home-grown stack would lose the property that matters most: the oracle has to be +*independent*, and protocol code written by the same team under the same assumptions is not. + +### What a session catches that a packet cannot + +- **The TCP checksum after a NAT rewrite.** It covers a pseudo-header containing the IP addresses, so + NAT must recompute it. A single-packet test never looks; a session stalls. +- **MSS clamping and MTU handling.** Invisible to one packet, fatal to a transfer. +- **Bidirectional translation consistency over a real flow**, including retransmissions and reordering. +- **"Established connections keep working."** Establish a session, apply a config operation, watch + whether bytes keep moving. That is the *preserved* disposition above, answered for free. +- Flow table eviction under sustained load. + +### A stall is not a refusal + +"Eventually completes" has to be bounded -- some number of polls of virtual time -- and the expectation +has to come from the algebra: this session *should* complete, or it *should* be refused. A refusal has +to be **attributable**: a RST, an ICMP unreachable, or a counted drop carrying a reason. + +Never a stall. Hunting stalls is most of the value, because a silent stall is exactly the failure an +operator cannot diagnose. This is [no silent change](#the-part-that-is-not-free-state-across-transitions) +restated at session granularity. + +### Two guards, and one staging decision + +- **Run a null path first.** Every session oracle should also run client-to-server directly, with no + dataplane in between. A failure there is the harness or the stack, not us. That converts "what if + `smoltcp` has a bug" from a source of false positives into a detected condition. +- **Bound the transfer.** A bulk transfer is thousands of packets. Fuzz cases want the minimum that + exercises handshake, a few segments and teardown; save large transfers for the window and MTU + properties specifically. Throughput is coverage. +- **Start in `Medium::Ip`, not Ethernet.** IP mode skips ARP and neighbour discovery, so those do not + have to work before any session test can pass. Add Ethernet mode later, at which point ARP/ND becomes + its own testable surface rather than a prerequisite. + +### How it composes with the algebra + +Each operation's postcondition becomes a claim about sessions rather than packets: + +- `peer(A, B)` -- a session from A's exposed prefixes to B's completes; one to a prefix the manifest does + not expose is refused, attributably. +- `undo(peer(A, B))` -- new sessions are refused, and *established* ones either drain or die. Which of + those is correct is a product decision; the point is that a session oracle makes the answer + observable rather than theoretical. +- **Disjoint peering components** -- no session across them ever completes. +- **Frame condition** -- establish sessions inside one component, operate inside another, and assert the + first component's sessions keep moving bytes. Tenant isolation, probed as hard as it can be probed. + +## The selection oracle is already built + +Every network function that consults a table has two separable halves, and only one of them is hard to +oracle: + +| half | question | oracle | +| --- | --- | --- | +| **selection** | which rule matched? | differential, against a trivial reference matcher | +| **action** | was the right thing then done? | invariants and metamorphic relations | + +Selection is where the frightening bugs live -- overlapping NAT rules, ACL precedence, LPM +disambiguation -- and it is also the half that already has a reference implementation in this tree. +`acl/src/reference/` provides: + +```rust +pub fn lookup(&self, key: &K) -> Option<&A> // the winner +pub fn matches(&self, key: &K) -> Vec<&RefRule> // every matching rule, in order +``` + +with a test named `matches_is_nonlossy_and_retains_shadowed_losers`. So "which rule should have won, and +which ones it shadowed" is answerable in a single pass, for any key. + +### Why this generalises past ACL + +`match_action::FieldKind` is `{Prefix, Mask, Range, Exact}` -- the P4 and DPDK classifier vocabulary -- +and rule selection in every function discussed here fits inside it: + +| function | selection expressed as | +| --- | --- | +| ACL | prefix + range + exact over the 5-tuple | +| FIB / LPM | prefix on destination | +| static NAT | exact or prefix on source and destination | +| masquerade | prefix, to choose the pool | +| port forwarding | range over ports | + +One trivial reference mechanic therefore serves as the selection oracle for all of them. It is also the +piece *least* exposed to the pipeline rework, because the vocabulary says nothing about topology -- it +does not care whether the functions form a line or a DAG. + +### Per-rule counters are the aggregate form + +Comparing per-rule hit counts across a whole traffic stream is cheaper than a per-packet comparison -- +nothing lands in the hot path -- and strictly stronger, because it catches *distribution* differences. A +rule winning three percent too often is invisible packet by packet and obvious in aggregate. + +Counters are wanted for operational reasons regardless, which makes this the best kind of test +dependency: one that pays for itself elsewhere. + +### Three boundaries to respect + +**Selection is not action.** The oracle says which rule should have matched. It says nothing about +whether NAT then allocated the right port, built consistent bidirectional state, or handled the reverse +direction. That half is stateful and already has its own properties -- the exclusivity and injectivity +claims in `nat/src/masquerade/apalloc/`. Two oracles for two halves, which is a decomposition rather +than a shortfall. + +**It speaks only to flow-establishing packets.** A flow table hit bypasses rule lookup entirely, so the +reference has nothing to say about subsequent packets of an established flow. Those get a different and +easier claim: treatment consistent with what the first packet established. + +**Build the reference from the configuration, not from the production table.** This one matters. If both +sides consume the same built table then a bug in `config -> table` is invisible, because both agree on +it -- the same-source problem that makes shadow models worthless. The reference must go from +configuration to its own naive rule list. Check which way `acl/tests/eal_classify_via_projection.rs` +does it; the name suggests a projection of the real table, which is the weaker arrangement. + +### Footprints come from predicates, not from document structure + +A rule mutation's footprint is **the rule's own match predicate**: the set of keys it matches. That is +exact, computed rather than declared, and it needs no analysis of the configuration document's shape. + +`matches()` supplies the rest. Adding a rule changes verdicts for the keys it matches *minus* those where +something else still wins, and the shadow set is precisely what `matches()` returns. So the reference +matcher is not only the selection oracle -- **it is also the footprint calculator.** + +This supersedes an earlier line of thinking worth recording so it is not re-derived. The configuration +document is a tree, so it is tempting to take an entity's subtree as its footprint and recurse: a VPC's +subtree, an ACL's rule array, an LPM's prefix subtree. Two things go wrong. + +**"Technically a tree" is not the property that matters; locality is.** An LPM trie gives a genuinely local +footprint -- the subtree under a prefix is exactly the more-specific routes. An ACL rule array is a `Vec`, +and modelling it as a linked list is true but useless: the "subtree" of rule *i* is every rule after it, so +the footprint is `O(n)` and the frame is a predicate over packets rather than a region of the document. The +recursion recovers the *shape* and loses the only property the shape was wanted for. + +**Cross-references break subtree containment, and delegating them to the validator does not help.** The +validator's concern is whether a reference resolves. The frame's concern is that a mutation inside VPC A's +subtree can change behaviour governed by the peering that references A -- so the footprint is the subtree +*plus everything referencing into it*. That is the **inbound** closure, which is the one direction a +document structure does not give you. It is also the same fact as "a deletion's footprint is everything +that referred to the deleted thing": cross-references are the deletion problem seen from the configuration +side. + +What survives, then: + +- **At the table level**, footprints come from predicates. No tree, no index. +- **At the configuration level**, a reverse-reference index is still required, for exactly the deletion and + modification cases. The validator needs the same index, so it is shared machinery rather than a second + mechanism. +- **Set versus sequence semantics still predicts cost**, and is now a property of a table's disambiguation + rather than of the document: + + | disambiguation | insertion order | footprint | mutations commute | + | --- | --- | --- | --- | + | most specific wins (LPM) | irrelevant | the predicate | freely | + | first match wins (`Vec`) | *is* the meaning | predicate minus shadowing, positional | rarely | + + Both are computable from `matches()`. The second is simply more expensive to reason about, which is worth + knowing when choosing a representation: priority-tagged rules with validator-enforced disjointness would + move a table into the cheap column. Whether that is worth the change to operator-visible semantics is a + product question, not a testing one. + +### Actions need no reference implementation + +Stopping the reference at selection sounds like it leaves the action half unchecked. It does not, and the +reason is structural rather than a rule of thumb: + +- **Selection has no local invariant.** "Which of these overlapping rules should have won" can only be + answered by comparing against something, so it needs a differential. +- **Actions do have local invariants.** "What did you do to this packet" is a relation between before and + after, checkable in place. + +Sorted by what they require, and note that nothing here needs a second implementation: + +| requires | examples | +| --- | --- | +| the output alone | the packet still parses; source is not a multicast address; the checksum is self-consistent | +| input and output | TTL exactly one less, or dropped; payload unchanged; only fields NAT may rewrite differ | +| output + matched rule | dest MAC is the nexthop's resolved MAC per that rule; translated addr in that rule's pool | +| two executions | forward then reverse is the identity on the 5-tuple | +| enumerable state | distinct live flows never collide; the mapping just created is in the overlay | + +#### The selected rule is the specification for the action + +The third row is what makes a whole-pipeline fuzz possible. Never compute what the output should be. +Verify two things and chain them: + +1. the right rule was selected -- differential, against the reference matcher; +2. the output is consistent with the rule that was selected -- invariant, no reference. + +Composed, those give end-to-end correctness with no parallel dataplane anywhere. This is why stopping the +reference at selection costs nothing. + +It does impose a design requirement, and a cheap-now-expensive-later one: **a rule must name its action +completely enough to serve as a specification.** If a rule says "masquerade" while the pool it draws from +lives somewhere else, the rule is not a spec and the action cannot be checked against it. + +#### Duplicate no semantics; expose whatever state you need + +"Non-intrusive" was the wrong way to state the constraint. The distinction that matters is: + +- An **observability seam** -- counters, an overlay, an event log -- exposes state. It encodes no semantics, + so it cannot drift. The worst it can become is stale API. +- A **reference implementation** duplicates semantics. It drifts by construction, because two encodings of + one rule diverge under maintenance. + +Rot comes from duplicated semantics, not from exposed state. Per-rule counters are already an intrusion of +the first kind and are entirely fine. + +An overlay over NAT's mappings is the same class of intrusion, and it buys **enumerability**: without one +you can see that a packet was translated but cannot enumerate every mapping a batch created. That is what +turns per-packet checks into set-level ones, and set level is where injectivity, exact accounting and leak +detection live. A batch of zero packets is a useful degenerate case -- it asserts that nothing is allocated +when nothing flows. + +Two requirements fall out of it: + +- **Record events, not a final set.** A create/destroy/create sequence within one batch collapses to a + single create if only the endpoints are diffed, and that is exactly where the interesting bug hides. +- **Timers need the caller-supplied clock**, the same one the session oracles need. Build the virtual clock + once and properly rather than twice badly; flow timers leaking between fuzz inputs has already been a + real defect here. + +#### Re-point the existing property tests rather than writing new ones + +`net/` already contains a large body of property tests asserting that the header machinery is +self-consistent. The **same predicates**, applied to `(packet_in, packet_out)` pairs, assert that an action +used that machinery correctly. Same predicates, different subject -- re-pointing rather than copying, so it +adds no maintenance surface. + +`Checksum::validate_checksum` is public and usable as an action invariant today. `parse_back_test` in +`net/src/headers/mod.rs` is the round-trip oracle and needs only to be `pub(crate)` to be reused. + +### Why this is not "a parallel dataplane" + +Casting selection as a reference implementation invites the objection that we are building a second +dataplane to check the first. The objection is worth answering precisely, because the answer is also the +maintenance argument. + +What differs between the two paths is the **table build** and the **lookup algorithm** -- optimised trie or +hash against a naive linear scan. What is *held fixed* is the meaning of a rule and the meaning of an +action. So this is a differential test of construction and lookup, not a reimplementation of semantics. + +The consequence that matters: **the reference scales with the match vocabulary, not with the feature set.** +There are four `FieldKind`s. Add ten network functions and the reference does not change; it changes only +if a genuinely new kind of match is introduced. A parallel dataplane would scale with features and would +therefore rot. + +Three things to hold onto: + +- **The reference must consume configuration and emit verdicts, and touch nothing internal.** Its + independence from internal structures is what stops it breaking when they change. Refusing intrusive + dependency is not a nicety here; it is the whole reason the thing stays maintainable. +- **Stop at selection.** It will be tempting to have the reference also compute the translated packet, the + checksum fixup, the encapsulation. That is the line where it *does* become a parallel dataplane and does + start to drift. The action half is oracled by invariants, metamorphic relations and session-level checks + -- never by a reference. +- **`FieldPredicate` is genuinely shared**, so a bug in what "prefix /24 matches" means is invisible to the + differential. It is small enough to property-test directly against a naive bit-by-bit implementation, and + that is worth doing precisely because it is the one place the same-source objection lands. + +One qualifier on the longer-term ambition of casting the whole dataplane in match-action terms: match-action +describes the *stateless classification* in each function. The stateful part -- flow tables, NAT sessions, +connection tracking -- is match-action *plus* mutable state, which is why a concurrent bimap is needed for +NAT rather than a table alone. + +That is the same boundary as the selection/action split, restated one level up. When the test structure and +the architecture divide along the same line, the tests survive changes to either side; when they do not, +every refactor invalidates a test suite. This one divides along the same line, which is the strongest reason +to think the approach will hold. + +A note on the interim NAT representation: an `Arc>` forward/reverse pair is fine for an oracle, +but it means the oracle cannot live in a per-packet path even in debug builds. So selection oracles run +test-side, and the in-place tier 0 assertions stay confined to structural invariants that need no lock. + +## Contracts belong to network functions, not to the DAG + +The natural first instinct is to put the oracles at the boundary of the whole pipeline: feed traffic in one +end, judge what comes out the other, and let one set of mutations cover ACL, router, NAT and everything +else together. **That does not work, and the reason is masking.** + +An ACL rule that drops traffic before the router ever sees it hides the router entirely. At the pipeline +boundary there is no way to distinguish "the ACL correctly dropped this" from "the router would have +misrouted it and we never found out". Worse, the oracle has to predict the *composition* -- what the ACL +did, and then what the router would have done to whatever survived -- so the expectation becomes a +cross-product over domains and grows unmanageable exactly as the vocabulary grows. + +### Masking is a vacuity problem wearing a disguise + +Notice what masking actually costs: coverage of the router's logic silently falls to zero for that class of +traffic, and a green run says nothing about it. Tighten an upstream ACL and downstream oracles quietly stop +being exercised. + +Per-function contracts make that measurable rather than invisible. Count arrivals at each function's input. +If a mutation upstream causes that count to collapse, the [vacuity](#vacuity) guard fires and names the +function that stopped being tested. At the pipeline boundary the same change looks like a pass. + +### The decomposition + +Each network function gets its own contract: + +- a **precondition** -- what it may assume about a packet arriving, and +- a **postcondition** -- what it guarantees about a packet departing. + +Pipeline behaviour is then the *composition* of those contracts, and no pipeline-level oracle is needed. +When a function drops a packet, the next function's contract is vacuously satisfied for it -- no input, no +obligation -- which is both the correct semantics and free. + +ACL, router, NAT and the rest are **distinct domains**. This is consistent with deriving commutation from +read and write sets: mutations in different domains usually touch disjoint state and therefore commute by +that test, without needing to be told they are unrelated. Where they genuinely conflict is where their +domains share a referenced entity -- an ACL rule reading a VPC that another mutation removes -- and that is +exactly the deletion footprint that makes removal the interesting case. + +### Two levels of contract, kept apart + +The word "precondition" is now doing two jobs, and confusing them will cause trouble: + +| | subject | precondition | postcondition | frame | +| --- | --- | --- | --- | --- | +| **mutation** | configuration state | definedness (its read set) | the claims it adds | its write set | +| **network function** | packet and flow state | what may arrive | what departs | untouched fields | + +The link between them: a mutation's claims are ultimately claims *about network function contracts*. +`peer(A, B)` does not directly assert anything about a packet -- it changes what the ACL function's +postcondition is for traffic between A and B. + +### Why this is where `debug_assert!` belongs + +A function's pre- and postconditions live at its entry and exit, which is literally where an assertion goes. +So tier 0 and this decomposition are the same idea, and that has two consequences worth having: + +- **The oracle moves with the code.** Rework the DAG and a function's contract travels with the function, + because it is written at its boundary rather than in a test that knows the old topology. +- **Failures localise.** A stalled session says only "something in the pipeline is wrong". The first + violated postcondition names the function. That repairs the one real weakness of in-place assertions -- + that they fire where a problem is observed rather than where it was caused. + +### What it costs + +Writing these contracts down forces every implicit assumption a function makes about its predecessors to +become explicit, and some of those assumptions will turn out to be disputed. That is the point rather than a +side effect -- undocumented coupling between stages is the defect, not the documentation of it -- but it is +real work and it will surface disagreements. + +One consequence specific to the DAG: a function may have several predecessors, so its precondition has to +hold for packets arriving from *any* of them. That is strictly stronger than the line-graph case, and it is +a question the DAG design has to answer rather than one the tests can. + +## Deriving the oracles from the algebra + +Everything above describes oracles that *could* be written. This section is about not writing them by +hand. + +Treat configuration operations and traffic as members of one monoid acting on pipeline state. Write +`Tcp(p)` for pushing a session `p` through the pipeline and `A` for a configuration mutation, composed +right to left, so `Tcp(p) . B . A . P` means "apply `A`, then `B`, then run session `p`". This matters +because **traffic mutates state too** -- flow tables, NAT allocations -- so treating it as a read-only +probe misses a class of failure. + +### This is a naming scheme, not a logic + +The algebraic notation is suggestive and it leaks. Do not try to reason in it: + +- **There is no `Tcp(p)^-1`.** Not merely unimplemented -- semantically meaningless, and it fails + uniqueness of inverses. The nearest thing to `Tcp(p)^-1 . Tcp(p) . P` is `time(+t) . Tcp(p) . P` for a + `t` long enough to decay whatever transient `Tcp(p)` left behind. +- **It is a groupoid, not a group.** The undo of an operation depends on the state it was applied to, so + `[B, A] = B A B^-1 A^-1` is not literally formable. +- **The operators are relations, not functions.** `apply_masquerade_config` sets `randomize(true)` + unconditionally, so a session's port allocation is not determined by the input. Either seed it or keep + it out of the compared projection. +- **`~=` is transitive only with a growing bound.** If `P ~= Q` within `K` steps and `Q ~= R` within `K`, + then `P ~= R` within `2K`. Short expressions only. + +Following those leaks toward rigour ends in rebuilding a temporal logic, which is not a project this team +can afford and not one it needs: **we want to find defects, not prove their absence.** Testing needs none +of the properties the notation appears to promise. It needs a way to enumerate expressions, a way to run +two of them, and a projection to compare. + +Where genuine temporal reasoning *is* wanted -- liveness over unbounded interleavings -- that is what the +model checker is for, over the small coordination state space described above. The division of labour: + +| | state space | how "eventually" is discharged | +| --- | --- | --- | +| model checker | small, exhaustive | a liveness property over all interleavings | +| algebra-derived oracles | large, sampled | advance virtual time to quiescence, then compare | + +### The mechanism + +Each operation in the vocabulary carries three pieces of metadata, all cheap and all derivable from its +arguments: + +- **`footprint(A)`** -- which peering components, VPCs or NFs it can affect. +- **`undo(A, X)`** -- its state-dependent reverse. +- **`commutes_with(A)`** -- a declaration, which the tests then check. + +From those alone, five families of test are generated. No test in any family is hand-written, so adding +an operation to the vocabulary adds tests to all five: + +| family | shape | catches | +| --- | --- | --- | +| postcondition | `Tcp(p) . A . P` for `p` inside `footprint(A)` | the operation did what it claims | +| frame | `[Tcp(p), A] = 0` for `p` outside `footprint(A)` | config disturbing unrelated traffic | +| traffic isolation | `[Tcp(p), Tcp(q)] = 0` for `p`, `q` in disjoint components | interference via shared resources | +| transience | `O(undo(A) . Tcp(p) . A . P) ~= O(P)` | state orphaned when config is removed | +| commutation | declared `[B, A] = 0` implies observable equivalence | order dependence the config data hides | + +Two notes on reading that table. + +**The frame condition is a vanishing commutator.** That is the general form; the probe-set formulation +earlier in this document is the special case where the two orders are run as a before-and-after rather +than side by side. A *non*-vanishing commutator is more than a failure signal -- its magnitude is how much +the configuration change disturbed the traffic, which is "established connections keep working" with a +number attached. + +**Transience is stated over the behaviour function, not the state.** `O(P)` maps a session to a verdict. +The claim is that no effect of traffic is observable in the verdict of a later independent session -- *not* +that traffic leaves no trace. Some traces are legitimate and must survive: a neighbour cache entry created +by traffic should persist. Stating it over verdicts permits that and still catches the case that matters, +which is an allocation orphaned by a peering that no longer exists. + +### Implementation shape + +Enough of the structure is settled to sketch it. Start from the blank configuration -- which already exists +as `ExternalConfig::BLANK_GENID` -- as the identity the sequences fold over. Worth noting that the blank +config is also where the rollback defect lives, so the identity element of the algebra is a known-bad state +and the first test written lands on the worst path. + +```rust +trait Mutation { + /// Apply, returning the state-dependent reverse. + fn apply(&self, p: &mut Pipeline) -> Undo; + + /// Ordering and definedness: a precondition is a read of what someone else wrote. + fn reads(&self) -> Footprint; + + /// The frame: everything outside this is unchanged. + fn writes(&self) -> Footprint; + + /// Which probes this mutation must make a difference to. Derived, not written, in the common case. + fn interested_in(&self, probe: &Probe) -> bool { + self.writes().intersects(probe.touches()) + } +} +``` + +Three things this sketch deliberately does *not* have. + +**No per-mutation expectation object.** An expectation that closes over the two states it was born between +goes stale as soon as the sequence continues past it. Make it a pure function of `(probe, &Pipeline)` and it +stays valid everywhere -- but then it is not per-mutation at all, it is a claim about correct behaviour given +a configuration. So there is a *small* reusable set of expectation predicates, one per kind of observable, +and one `interested_in` per mutation. That is far cheaper than one oracle per mutation and it puts all the +domain knowledge in a handful of named predicates. + +**No inverse oracle.** A differential oracle between `P` and `P'` is direction-agnostic: same interest set, +same expectation. The reverse mutation reuses it. + +**No global oracle array.** Configurations snapshot cheaply because they are data; live pipelines with their +flow tables and port allocations do not. So the oracles are a *stream checked with a window of two* -- three +for transience: before, after the mutation plus traffic, after the undo. Each mutation is checked against its +immediate neighbours rather than against the final state. The abstraction reads as though it is global; the +implementation cannot be, and pretending otherwise will run the harness out of memory. + +**The interest partition is what does the work.** For a given probe, split the mutations into those that +claim interest and those that do not. The uninterested ones must leave the probe's verdict unchanged -- that +is the frame. The interested ones must change it -- and a mutation that claims interest but changes nothing +is a mutation that was accepted and silently not enacted, which is the defect class the IPv6 peering +reproducer belongs to. + +## Where the checks live + +Four tiers, cheapest and most local first: + +| tier | kind | survives refactoring | +| --- | --- | --- | +| 0 | local invariants, `debug_assert!` in place | while the structures do | +| 1 | metamorphic relations, test-side | best -- stated in domain terms | +| 2 | differential against a reference matcher, for *rule selection* | well -- the vocabulary is topology-independent | +| 3 | end to end: session oracles plus conservation laws (in = out + drops, attributable) | best; cheapest | + +Factor each check as a **named function** callable from both tests and `debug_assert!`. That, rather +than the assertion itself, is what survives a rewrite. + +### Rules for the in-place checks + +- **Only the assertion bodies may compile out.** If a `#[cfg]` reaches the code under test, the fuzzed + binary is not the shipped binary and the results do not transfer. +- **Tier the cost.** For a coverage-guided fuzzer, throughput *is* coverage: a debug build ten times + slower explores a tenth as much. Cheap invariants can be always-on in debug; anything `O(n)` in a + per-packet path belongs behind its own feature. +- **`debug_assert!` is a net, not a specification.** It catches falls; it does not state what correct + means. Five hundred of them still do not answer "does this ACL do what the config asked". That + question needs tier 2. + +## Vacuity + +An algebra can quietly stop producing interesting sequences -- every operation refused by its +preconditions, say -- and a suite of claims that are never exercised passes beautifully. + +Count what was actually reached and assert on it, as `agreement_is_not_vacuous` in +`net/src/headers/view.rs` does. In this campaign that guard has repeatedly been the only thing +standing between a green run and a meaningless one. + +## Shrinking + +When an operation sequence fails, the useful artefact is the minimal failing subsequence, and a +state-dependent generator makes that harder than usual. + +Because the drawable operations at each step are a function of the configuration built so far, removing an +earlier operation changes what every later draw *means*. Byte-level shrinking therefore yields a +*different* sequence rather than a smaller one, and the failure usually evaporates for reasons unrelated to +the bug. + +Two things help: + +- **Shrink at the sequence level.** Try removing each operation, re-run, and keep the removal if the failure + survives. This is a handful of lines and it is the only shrinker that respects the dependency structure. +- **Select arguments by index modulo what exists** -- "the third VPC present" rather than "VPC with id 7" -- + so that deleting an earlier operation degrades the rest of the sequence instead of scrambling it. + +## What this does not give you + +- It does not prove the validator is right, only that the dataplane agrees with it. +- It reaches only the configurations the modelled operations compose to. +- Environmental failures -- netlink refusing an operation, FRR being down -- are not config-derived and + cannot be tested this way. They need retry-to-convergence and reporting, not a config oracle. +- It says nothing about whether the dataplane is *fast*, and several of the checks here are affordable + only because they are compiled out of release builds. + +## Open questions + +- The peering graph supplies the frame's footprint for VPC operations. What supplies it for the + operations that are not VPC-scoped -- device and tracing configuration, flow table capacity? +- Whether a per-packet assertion of any kind is affordable in a debug datapath is unmeasured. If it is + not, tier 0 has to move out of the packet path and into the structures it mutates. +- Does `acl/tests/eal_classify_via_projection.rs` build its reference from the configuration or by + projecting the production table? If the latter, the `config -> table` build is untested by it, and that + is the arrangement to fix before leaning on the selection oracle anywhere else. +- `acl/src/dpdk/dyn_table.rs` is the largest in-scope gap in `acl` at 82.4%, 104 uncovered lines. The + production side of the selection machinery is well tested but not fully. +- Where the session endpoints attach relative to VXLAN encapsulation. This has to be settled before the + harness is written, and it is not obvious. +- Barrier versus permitted hybrids for config adoption across the DAG. This is the question the model + checker exists to answer. + +[smoltcp]: https://docs.rs/smoltcp +[stateright]: https://www.stateright.rs/title-page.html +[`TypeGenerator`]: https://docs.rs/bolero/latest/bolero/generator/trait.TypeGenerator.html +[`ValueGenerator`]: https://docs.rs/bolero/latest/bolero/generator/trait.ValueGenerator.html diff --git a/development/code/property-testing.md b/development/code/property-testing.md index a9ab2b32ec..4e06999a7b 100644 --- a/development/code/property-testing.md +++ b/development/code/property-testing.md @@ -20,5 +20,13 @@ A type may implement [`ValueGenerator`] to provide a more restricted set of valu This is useful if you wish to focus fuzzing efforts more narrowly than a correct implementation of [`TypeGenerator`] allows. +## Generating large structured inputs + +Reaching for a narrower [`ValueGenerator`] each time the fuzzer cannot get somewhere stops scaling once +the input is as large as a whole configuration: the generators do not compose, and each one encodes a +little more knowledge of the implementation. For those cases, build the input from an algebra of valid +operations instead, and derive the oracles from the same algebra -- see +[testing a config-driven dataplane with an operation algebra](./config-algebra-testing.md). + [`TypeGenerator`]: https://docs.rs/bolero/latest/bolero/generator/trait.TypeGenerator.html [`ValueGenerator`]: https://docs.rs/bolero/latest/bolero/generator/trait.ValueGenerator.html diff --git a/nat/src/masquerade/fuzz.rs b/nat/src/masquerade/fuzz.rs new file mode 100644 index 0000000000..d35e7c447c --- /dev/null +++ b/nat/src/masquerade/fuzz.rs @@ -0,0 +1,480 @@ +// SPDX-License-Identifier: Apache-2.0 +// Copyright Open Network Fabric Authors + +//! Properties of the masquerade network function, driven by generated configurations and packets. +//! +//! `static_nat::fuzz` covers a stage that is a pure function of its configuration. This one is not: +//! masquerade's answer for a flow is whatever the allocator handed out the first time it saw it, +//! and every property here is really about that state being kept consistently. +//! +//! # What can be asserted without an oracle +//! +//! Nothing here predicts which address and port a flow will be given -- that is the allocator's +//! business and predicting it would be a second copy of it. What can be said is how the answers +//! relate to each other and to the configuration: +//! +//! * the reply to a translated flow comes back to where the flow started (**reversibility**); +//! * the same flow gets the same answer every time (**stability**); +//! * two flows never get the same answer at once (**exclusivity**); +//! * every answer is inside a range the configuration named (**containment**). +//! +//! Containment is the one that consults the configuration, and legitimately: it is a statement that +//! the output is a member of a declared set, not a prediction of which member. An allocator handing +//! out an address nobody gave it is the failure that check exists for. +//! +//! # No timers +//! +//! Every property completes within one flow lifetime, so none depends on expiry either happening or +//! not. Expiry is a separate subject and needs the explicitly driven clock the development guide +//! asks for, rather than a wall clock a property happens to outrun. + +#![cfg(test)] + +use crate::masquerade::probe::{Arrival, Fabric, ProbeSpec, Stray, run}; +use bolero::{Driver, TypeGenerator, ValueGenerator}; +use concurrency::sync::atomic::{AtomicUsize, Ordering}; +use config::external::overlay::vpcpeering::VpcExpose; +use config::external::overlay::vpcpeering::contract::MasqueradeExposes; +use net::buffer::TestBuffer; +use net::packet::Packet; +use std::collections::BTreeMap; +use std::net::IpAddr; +use std::num::NonZero; + +/// Exposes per configuration. +const MAX_EXPOSES: u8 = 3; + +/// The fewest reaching draws any property may see before it is considered vacuous. +const MIN_REACHED: usize = 8; + +/// Flows per configuration. +const PROBES: usize = 8; + +/// A configuration and a batch of flows to put through it. +#[derive(Debug, Clone, Copy)] +struct Scenario { + strays: bool, +} + +impl ValueGenerator for Scenario { + type Output = (Vec, Vec); + + fn generate(&self, driver: &mut D) -> Option { + let exposes = MasqueradeExposes(MAX_EXPOSES).generate(driver)?; + + let mut probes = Vec::with_capacity(PROBES); + for _ in 0..PROBES { + let mut probe = ProbeSpec::generate(driver)?; + if !self.strays { + probe.clear_stray(); + } + probes.push(probe); + } + Some((exposes, probes)) + } +} + +/// Run a property inside a tokio runtime. +/// +/// `FlowTable::insert` spawns a per-flow expiry timer, so an insert outside a runtime context +/// panics. The existing masquerade tests get one from `#[tokio::test]`; a bolero property's body is +/// synchronous, so it enters a runtime rather than becoming async. +/// +/// A current-thread runtime with time enabled, and nothing ever awaits it: the timers exist so that +/// spawning them succeeds, and every property here finishes well inside the shortest flow timeout. +fn with_runtime(body: impl FnOnce()) { + let runtime = tokio::runtime::Builder::new_current_thread() + .enable_time() + .build() + .unwrap_or_else(|e| unreachable!("{e}")); + let _guard = runtime.enter(); + body(); +} + +fn fabric(exposes: &[VpcExpose]) -> Option { + let fabric = Fabric::build(exposes)?; + fabric.is_probeable().then_some(fabric) +} + +/// The source half of a packet's five-tuple. +fn source_of(packet: &Packet) -> (IpAddr, u16) { + ( + packet + .ip_source() + .unwrap_or_else(|| unreachable!("a probe is always an ip packet")), + packet.transport_src_port().map_or(0, NonZero::get), + ) +} + +/// The destination half. +fn destination_of(packet: &Packet) -> (IpAddr, u16) { + ( + packet + .ip_destination() + .unwrap_or_else(|| unreachable!("a probe is always an ip packet")), + packet.transport_dst_port().map_or(0, NonZero::get), + ) +} + +/// How much of a run actually reached the code under test. +#[derive(Default)] +struct Tally { + seen: AtomicUsize, + built: AtomicUsize, + reached: AtomicUsize, +} + +impl Tally { + /// Assert the run was not vacuous. + /// + /// The floor is **relative to the configurations actually built**, not an absolute count, because + /// an absolute one is really a measure of how fast the machine was. A property that reached + /// thousands of flows alone can reach a few dozen when it runs beside nine hundred other + /// tests on a loaded machine or under coverage instrumentation, and a floor tuned to the fast + /// case then fails for a reason that has nothing to do with the code under test. + /// + /// Both counts scale with the iteration budget, so their ratio does not. What the guard is for is + /// a property that has stopped reaching its assertion at all -- and a collapse to zero is just as + /// visible in the ratio. + fn report(&self, what: &str) { + let (seen, built, reached) = ( + self.seen.load(Ordering::Relaxed), + self.built.load(Ordering::Relaxed), + self.reached.load(Ordering::Relaxed), + ); + println!("{what}: {built}/{seen} configurations built, {reached} flows reached it"); + assert!( + built * 2 >= seen, + "only {built} of {seen} configurations built, so this checked much less than it looks \ + like it did" + ); + // At least one reaching flows for every two configurations built, and never zero. + assert!( + reached >= MIN_REACHED && reached * 2 >= built, + "{reached} flows reached the {what} assertion across {built} configurations; \ + this property has gone vacuous" + ); + } +} + +/// The reply to a masqueraded flow comes back to where the flow started. +/// +/// The stateful analogue of static NAT's round trip, and it works quite differently. There is no +/// second table built from the other side of the peering: the reverse translation exists only +/// because the forward packet created a flow entry holding it, `FlowLookup` finds that entry, and +/// `Masquerade` applies it. +/// +/// So this is a statement about state rather than about configuration -- whatever the allocator +/// chose, the entry it wrote down has to describe the inverse of what was done to the packet. A +/// forward translation that is not faithfully recorded is a connection that never gets an answer, +/// which is the characteristic masquerade failure and is invisible to any test of the allocator on +/// its own. +#[test] +fn a_masqueraded_flow_comes_back() { + let tally = Tally::default(); + + with_runtime(|| { + bolero::check!() + .with_generator(Scenario { strays: false }) + .cloned() + .for_each(|(exposes, probes): (Vec, Vec)| { + tally.seen.fetch_add(1, Ordering::Relaxed); + let Some(fabric) = fabric(&exposes) else { + return; + }; + tally.built.fetch_add(1, Ordering::Relaxed); + let (mut lookup, mut masq) = fabric.stages(); + + for spec in &probes { + let probe = (*spec).resolve(&fabric); + let before = (probe.source, probe.sport); + let out = run( + &mut lookup, + &mut masq, + vec![probe.packet()], + probe.arrival.dst_vpcd, + ); + let after = source_of(&out[0]); + if after == before || out[0].is_done() { + continue; + } + + let back = run( + &mut lookup, + &mut masq, + vec![probe.reply(after.0, after.1)], + Arrival::inbound().dst_vpcd, + ); + assert_eq!( + destination_of(&back[0]), + before, + "{:?} was masqueraded to {after:?}, and the reply came back to {:?}", + before, + destination_of(&back[0]) + ); + tally.reached.fetch_add(1, Ordering::Relaxed); + } + }); + }); + + tally.report("reversibility"); +} + +/// A flow keeps the translation it was first given. +/// +/// The second packet of a flow takes a different path from the first: the first allocates and +/// writes a flow entry, the second finds that entry and reuses it. A stage that allocated again +/// would still produce a legal-looking packet, and the connection would break in a way nothing at +/// the allocator level could see -- the two allocations are individually correct. +#[test] +fn a_flow_keeps_its_translation() { + let tally = Tally::default(); + + with_runtime(|| { + bolero::check!() + .with_generator(Scenario { strays: false }) + .cloned() + .for_each(|(exposes, probes): (Vec, Vec)| { + tally.seen.fetch_add(1, Ordering::Relaxed); + let Some(fabric) = fabric(&exposes) else { + return; + }; + tally.built.fetch_add(1, Ordering::Relaxed); + let (mut lookup, mut masq) = fabric.stages(); + + for spec in &probes { + let probe = (*spec).resolve(&fabric); + let before = (probe.source, probe.sport); + let first = run(&mut lookup, &mut masq, vec![probe.packet()], probe.arrival.dst_vpcd); + if out_unchanged(&first, before) { + continue; + } + let second = run(&mut lookup, &mut masq, vec![probe.packet()], probe.arrival.dst_vpcd); + + assert_eq!( + source_of(&second[0]), + source_of(&first[0]), + "the same flow from {before:?} was given {:?} and then {:?}, so its reply can \ + only reach one of them", + source_of(&first[0]), + source_of(&second[0]) + ); + tally.reached.fetch_add(1, Ordering::Relaxed); + } + }); + }); + + tally.report("stability"); +} + +/// Whether a batch's first packet came out as it went in. +fn out_unchanged(out: &[Packet], before: (IpAddr, u16)) -> bool { + out[0].is_done() || source_of(&out[0]) == before +} + +/// Two live flows never share a translation. +/// +/// The exclusivity claim the allocator exists to keep, stated where it matters: at the stage, over +/// packets, with the flow table in the loop. Two flows sharing an address and port are +/// indistinguishable on the way back, so one of them receives the other's traffic -- a tenant +/// isolation failure rather than a routing one. +/// +/// Distinct source *ports* as well as addresses, since masquerade puts many private addresses behind +/// few public ones and the port is what keeps them apart once the addresses have collapsed. +#[test] +fn distinct_flows_do_not_share_a_translation() { + let tally = Tally::default(); + + with_runtime(|| { + bolero::check!() + .with_generator(Scenario { strays: false }) + .cloned() + .for_each(|(exposes, probes): (Vec, Vec)| { + tally.seen.fetch_add(1, Ordering::Relaxed); + let Some(fabric) = fabric(&exposes) else { + return; + }; + tally.built.fetch_add(1, Ordering::Relaxed); + let (mut lookup, mut masq) = fabric.stages(); + + let mut taken: BTreeMap<(IpAddr, u16), (IpAddr, u16)> = BTreeMap::new(); + for (index, spec) in probes.iter().enumerate() { + let mut probe = (*spec).resolve(&fabric); + // A distinct port per probe, so that repeated draws are still distinct flows and + // the property is about contention rather than about the draw. + probe.sport = u16::try_from(1024 + index).unwrap_or(1024); + let before = (probe.source, probe.sport); + let out = run(&mut lookup, &mut masq, vec![probe.packet()], probe.arrival.dst_vpcd); + if out_unchanged(&out, before) { + continue; + } + let after = source_of(&out[0]); + + if let Some(previous) = taken.insert(after, before) { + assert_eq!( + previous, before, + "flows from {previous:?} and {before:?} were both masqueraded to {after:?}, \ + so a reply can only reach one of them" + ); + } + tally.reached.fetch_add(1, Ordering::Relaxed); + } + }); + }); + + tally.report("exclusivity"); +} + +/// Every translation lands inside a range the configuration named. +/// +/// The containment claim, and the one place a property here looks at the configuration. It is a +/// membership test rather than a prediction: which public address a flow gets is the allocator's +/// business, but *some* public address the operator declared is not negotiable. +/// +/// An address from outside the declared set is not merely wrong, it is unroutable -- the fabric has +/// no path back to it, so the flow is a blackhole that looks like a successful translation from +/// inside the box. +#[test] +fn a_translation_stays_inside_the_public_range() { + let tally = Tally::default(); + + with_runtime(|| { + bolero::check!() + .with_generator(Scenario { strays: false }) + .cloned() + .for_each(|(exposes, probes): (Vec, Vec)| { + tally.seen.fetch_add(1, Ordering::Relaxed); + let Some(fabric) = fabric(&exposes) else { + return; + }; + tally.built.fetch_add(1, Ordering::Relaxed); + let (mut lookup, mut masq) = fabric.stages(); + + for spec in &probes { + let probe = (*spec).resolve(&fabric); + let before = (probe.source, probe.sport); + let out = run( + &mut lookup, + &mut masq, + vec![probe.packet()], + probe.arrival.dst_vpcd, + ); + if out_unchanged(&out, before) { + continue; + } + let (addr, port) = source_of(&out[0]); + + assert!( + fabric.is_public(addr), + "{before:?} was masqueraded to {addr}:{port}, which no expose offers; the \ + fabric has no route back to it" + ); + tally.reached.fetch_add(1, Ordering::Relaxed); + } + }); + }); + + tally.report("containment"); +} + +/// Nothing is masqueraded that did not ask to be. +/// +/// The same precondition claim as static NAT's, over masquerade's own flags. Getting this wrong is +/// worse here than there, because a translation is not just applied but *recorded*: a packet +/// masqueraded without permission leaves a flow entry behind that will keep translating its +/// successors long after the mistaken packet is gone. +#[test] +fn nothing_is_masqueraded_without_permission() { + let tally = Tally::default(); + + with_runtime(|| { + bolero::check!() + .with_generator(Scenario { strays: true }) + .cloned() + .for_each(|(exposes, probes): (Vec, Vec)| { + tally.seen.fetch_add(1, Ordering::Relaxed); + let Some(fabric) = fabric(&exposes) else { + return; + }; + tally.built.fetch_add(1, Ordering::Relaxed); + let (mut lookup, mut masq) = fabric.stages(); + + for spec in &probes { + let probe = (*spec).resolve(&fabric); + if probe.asks_for_translation() && probe.exposed { + continue; + } + let before = (probe.source, probe.sport); + let (stray, arrival) = (probe.stray, probe.arrival); + let out = run(&mut lookup, &mut masq, vec![probe.packet()], probe.arrival.dst_vpcd); + + // A dropped packet is a legitimate answer for a flow the configuration cannot + // place; what is not legitimate is translating it. + if out[0].is_done() { + tally.reached.fetch_add(1, Ordering::Relaxed); + continue; + } + assert_eq!( + source_of(&out[0]), + before, + "masquerade translated {before:?} although {stray:?} forbade it; the packet \ + arrived as {arrival:?}" + ); + tally.reached.fetch_add(1, Ordering::Relaxed); + } + }); + }); + + tally.report("permission"); +} + +/// A flow that cannot be masqueraded is dropped, and says why. +/// +/// Same obligation as everywhere else, and masquerade has an unusually rich failure vocabulary -- +/// no allocator, allocation refused, capacity exceeded, unsupported protocol -- so the assertion is +/// that *some* reason is attached rather than which. What it rules out is the silent pass, which +/// here means letting a private address out onto the fabric untranslated. +#[test] +fn a_flow_that_cannot_be_masqueraded_says_so() { + let tally = Tally::default(); + + with_runtime(|| { + bolero::check!() + .with_generator(Scenario { strays: true }) + .cloned() + .for_each(|(exposes, probes): (Vec, Vec)| { + tally.seen.fetch_add(1, Ordering::Relaxed); + let Some(fabric) = fabric(&exposes) else { + return; + }; + tally.built.fetch_add(1, Ordering::Relaxed); + let (mut lookup, mut masq) = fabric.stages(); + + for spec in &probes { + let probe = (*spec).resolve(&fabric); + // The flows the configuration genuinely cannot place: a source it never named, or a + // vpc pair it has no allocator for. Masquerade must not simply forward these. + let unplaceable = matches!( + probe.stray, + Some(Stray::SourceNotExposed | Stray::UnknownSourceVni | Stray::UnknownDestVni) + ); + if !unplaceable { + continue; + } + let before = (probe.source, probe.sport); + let stray = probe.stray; + let out = run(&mut lookup, &mut masq, vec![probe.packet()], probe.arrival.dst_vpcd); + let packet = &out[0]; + + assert!( + packet.is_done(), + "a flow from {before:?} with {stray:?} passed masquerade with no verdict, so \ + a private address reaches the fabric untranslated" + ); + tally.reached.fetch_add(1, Ordering::Relaxed); + } + }); + }); + + tally.report("attribution"); +} diff --git a/nat/src/masquerade/mod.rs b/nat/src/masquerade/mod.rs index d7b2861dba..5e149bb06f 100644 --- a/nat/src/masquerade/mod.rs +++ b/nat/src/masquerade/mod.rs @@ -5,10 +5,12 @@ pub(crate) mod allocation; mod allocator_writer; pub mod apalloc; pub(crate) mod flows; +mod fuzz; pub(crate) mod icmp_handling; mod natip; mod nf; mod packet; +mod probe; mod protocol; mod state; mod test; diff --git a/nat/src/masquerade/probe.rs b/nat/src/masquerade/probe.rs new file mode 100644 index 0000000000..4d05b328ac --- /dev/null +++ b/nat/src/masquerade/probe.rs @@ -0,0 +1,332 @@ +// SPDX-License-Identifier: Apache-2.0 +// Copyright Open Network Fabric Authors + +//! Packets drawn relative to a masquerade configuration. +//! +//! The same shape as `static_nat::probe` -- a [`ProbeSpec`] of bare indices, resolved against a +//! built [`Fabric`] -- and the same reason for it. What differs is everything that follows from +//! masquerade being **stateful**, and that difference is the whole point of doing it second. +//! +//! # Static NAT is a function of its configuration; masquerade is not +//! +//! Static NAT's answer for a packet is fixed by the tables. Masquerade's is whatever the allocator +//! handed out the first time it saw the flow, kept in the flow table and reused thereafter. So: +//! +//! * **A probe is a flow, not a packet.** The first packet of a flow takes the allocation path; the +//! second takes the hot path through `flow_info`. They are different code and the interesting +//! properties relate them. +//! * **The reply needs a stage in front.** `Masquerade` recovers the reverse translation from +//! `flow_info`, which `FlowLookup` attaches, and only when `dst_vpcd` is absent. So the harness +//! runs two stages, and the reply arrives with the annotation deliberately left off. +//! * **Order matters.** Two runs of the same batch against the same fabric are not required to +//! agree, because the first left allocations behind. Every property here either states something +//! about one run or builds a fresh fabric. +//! +//! # The three prerequisites +//! +//! The development guide lists what has to be true before a stateful stage can be compared at all, +//! and all three are handled here rather than assumed: +//! +//! 1. **Seeded non-determinism.** `apply_masquerade_config` randomizes port selection, so two +//! fabrics allocate differently for the same flow. [`Fabric::build`] sets `set_randomize(false)`. +//! 2. **Timers.** Flow entries expire on a wall clock the harness does not drive. Rather than fake +//! it, every property here is written to complete within one flow lifetime -- the shortest +//! masquerade timeout is five seconds and a probe is a handful of packets -- so no property +//! depends on expiry either happening or not. Expiry is a separate subject and wants the +//! explicit clock the guide asks for. +//! 3. **Projections, not state.** Nothing here inspects the allocator or the flow table. Every +//! assertion is over what came out of the pipeline. + +#![cfg(test)] + +use crate::masquerade::{MasqueradeConfig, NatAllocatorWriter}; +use bolero::TypeGenerator; +use concurrency::sync::Arc; +use config::external::overlay::vpcpeering::VpcExpose; +use config::external::overlay::vpcpeering::contract::{ + LOCAL_VNI, REMOTE_VNI, overlay_with_exposes, +}; +use flow_entry::flow_table::{FlowLookup, FlowTable}; +use lpm::prefix::Prefix; +use net::buffer::TestBuffer; +use net::packet::{Packet, VpcDiscriminant}; +use net::vxlan::Vni; +use pipeline::NetworkFunction; +use std::net::IpAddr; + +use crate::Masquerade; +use crate::static_nat::probe::{build, vni}; + +/// Flow table capacity. Large enough that no property here can exhaust it, so a translation failure +/// is never the table being full. +const FLOW_CAPACITY: usize = 4096; + +/// A VNI no generated configuration uses. +const ABSENT_VNI: u32 = 4_000; + +/// A built masquerade configuration, and the addresses it declares. +pub(crate) struct Fabric { + flow_table: Arc, + allocator: NatAllocatorWriter, + /// Every address the local exposes offer. + pub(crate) private: Vec, + /// The prefixes translations must land inside. + pub(crate) public: Vec, + /// Addresses in the peer vpc. + pub(crate) peer: Vec, +} + +impl Fabric { + /// Build the allocator a set of exposes implies, or `None` if the overlay is not valid. + pub(crate) fn build(exposes: &[VpcExpose]) -> Option { + let overlay = overlay_with_exposes(exposes.to_vec()).ok()?; + let validated = overlay.validate().ok()?; + + // Only the first address of each private prefix: masquerade puts many private addresses + // behind few public ones, so the prefixes are /24s and enumerating them would be tens of + // thousands of probes for no new behaviour. What matters is that distinct sources contend + // for the same public range, and a handful of them does that. + let private: Vec = exposes + .iter() + .flat_map(|e| e.ips.iter().map(|p| p.prefix().as_address())) + .collect(); + let public: Vec = exposes + .iter() + .filter_map(|e| e.nat.as_ref()) + .flat_map(|nat| { + nat.as_range + .iter() + .map(lpm::prefix::PrefixWithOptionalPorts::prefix) + }) + .collect(); + + let peer = match private.first() { + Some(IpAddr::V6(_)) => vec![ + "2001:db8:ffff::1" + .parse() + .unwrap_or_else(|_| unreachable!()), + "2001:db8:ffff::2" + .parse() + .unwrap_or_else(|_| unreachable!()), + ], + _ => vec![ + "3.3.3.1".parse().unwrap_or_else(|_| unreachable!()), + "3.3.3.2".parse().unwrap_or_else(|_| unreachable!()), + ], + }; + + let flow_table = Arc::new(FlowTable::new(FLOW_CAPACITY)); + let mut allocator = NatAllocatorWriter::new(); + // Randomized port selection would make two fabrics built from one configuration disagree on + // every flow, which is legitimate behaviour and useless to compare. + let config = MasqueradeConfig::new(validated.vpc_table()).set_randomize(false); + allocator.update_nat_allocator(config, 1, &flow_table); + + Some(Self { + flow_table, + allocator, + private, + public, + peer, + }) + } + + /// The two stages a masqueraded packet passes through. + /// + /// `FlowLookup` first, because it is what turns a reply into something `Masquerade` can + /// recognise: the reverse translation lives in the flow entry the forward packet created, and + /// nothing else puts it on the packet. + pub(crate) fn stages(&self) -> (FlowLookup, Masquerade) { + ( + FlowLookup::new("flow-lookup", self.flow_table.clone()), + Masquerade::new( + "masquerade", + self.flow_table.clone(), + self.allocator.get_reader(), + ), + ) + } + + /// Whether this fabric can be probed at all. + pub(crate) fn is_probeable(&self) -> bool { + !self.private.is_empty() && !self.public.is_empty() + } + + /// Whether `addr` is inside one of the public prefixes the configuration named. + pub(crate) fn is_public(&self, addr: IpAddr) -> bool { + self.public.iter().any(|p| p.covers_addr(&addr)) + } +} + +/// Put a batch through the stages, in the order the real pipeline uses. +/// +/// **The order is the whole point, and getting it wrong makes the harness lie.** `FlowLookup` +/// attaches a flow entry only to a packet whose `dst_vpcd` is *absent*, and the flow filter that +/// sets `dst_vpcd` runs after it. So a harness that stamps both annotations up front never attaches +/// any flow state, every packet takes the allocation path, and a flow appears to be re-allocated on +/// every packet -- which is what this harness did until it was corrected. +/// +/// `Masquerade` then requires `dst_vpcd` to be present, so the annotation genuinely has to arrive +/// between the two stages rather than before or after both. That is the flow filter's job in +/// production and `TestFlowFilter`'s in the existing tests; here it is one assignment, which is all +/// of it that matters to masquerade. +pub(crate) fn run( + lookup: &mut FlowLookup, + masq: &mut Masquerade, + packets: Vec>, + dst_vpcd: Option, +) -> Vec> { + let mut looked: Vec<_> = lookup.process(packets.into_iter()).collect(); + for packet in &mut looked { + packet.meta_mut().dst_vpcd = dst_vpcd.map(VpcDiscriminant::from_vni); + } + masq.process(looked.into_iter()).collect() +} + +/// The metadata a packet must carry for [`Masquerade`] to look at it. +/// +/// Split in two on purpose. Everything here except `dst_vpcd` is set before the flow lookup; +/// `dst_vpcd` is set between the lookup and masquerade, because the lookup refuses to attach flow +/// state to a packet that already carries it. See [`run`]. +#[derive(Debug, Clone, Copy)] +pub(crate) struct Arrival { + pub(crate) src_vpcd: Option, + /// Supplied *after* the flow lookup, by [`run`], standing in for the flow filter. + pub(crate) dst_vpcd: Option, + pub(crate) wants_masquerade: bool, +} + +impl Arrival { + /// The first packet of a flow leaving the local vpc. + pub(crate) fn outbound() -> Self { + Self { + src_vpcd: Some(vni(LOCAL_VNI)), + dst_vpcd: Some(vni(REMOTE_VNI)), + wants_masquerade: true, + } + } + + /// The reply, arriving from the peer. The flow filter resolves its destination back to the + /// local vpc from the flow entry, which is what [`run`] stands in for. + pub(crate) fn inbound() -> Self { + Self { + src_vpcd: Some(vni(REMOTE_VNI)), + dst_vpcd: Some(vni(LOCAL_VNI)), + wants_masquerade: true, + } + } + + /// Everything an upstream stage sets *before* the flow lookup. + pub(crate) fn stamp(self, packet: &mut Packet) { + let meta = packet.meta_mut(); + meta.src_vpcd = self.src_vpcd.map(VpcDiscriminant::from_vni); + meta.set_overlay(true); + meta.set_keep(true); + meta.set_masquerade(self.wants_masquerade); + } +} + +/// A deliberate deviation from a flow the configuration masquerades. +#[derive(Debug, Clone, Copy, TypeGenerator)] +pub(crate) enum Stray { + /// A source address no expose offers, which the allocator has no range for. + SourceNotExposed, + /// A source vpc with no allocator entry of its own. + UnknownSourceVni, + /// A destination vpc the local vpc does not peer with. + UnknownDestVni, + /// Nothing asked for masquerade, so the stage should pass the packet through untouched. + NotAskedFor, +} + +/// A drawn probe, before it knows anything about a configuration. +#[derive(Debug, Clone, Copy, TypeGenerator)] +pub(crate) struct ProbeSpec { + source: u8, + peer: u8, + /// UDP throughout. TCP is refused unless the packet is a first segment, which is a separate + /// question from the mapping and would only add a rejection path to every property here. + sport: u16, + dport: u16, + stray: Option, +} + +/// A probe resolved against a fabric. +pub(crate) struct Probe { + pub(crate) source: IpAddr, + pub(crate) destination: IpAddr, + pub(crate) sport: u16, + pub(crate) dport: u16, + pub(crate) exposed: bool, + pub(crate) arrival: Arrival, + pub(crate) stray: Option, +} + +impl Probe { + /// Whether masquerade was asked to translate this flow and given what it needs to. + pub(crate) fn asks_for_translation(&self) -> bool { + self.arrival.wants_masquerade + && self.arrival.src_vpcd == Some(vni(LOCAL_VNI)) + && self.arrival.dst_vpcd == Some(vni(REMOTE_VNI)) + } + + /// The outbound packet, which may be built more than once. + /// + /// Unlike the static NAT probe this hands back a fresh packet each time on purpose: sending the + /// same flow twice is how the hot path is reached, and a property that wants to compare the two + /// needs both. + pub(crate) fn packet(&self) -> Packet { + let mut packet = build(self.source, self.destination, false, self.sport, self.dport); + self.arrival.stamp(&mut packet); + packet + } + + /// The reply to a flow that was translated to `translated`. + pub(crate) fn reply(&self, translated: IpAddr, translated_port: u16) -> Packet { + let mut packet = build( + self.destination, + translated, + false, + self.dport, + translated_port, + ); + Arrival::inbound().stamp(&mut packet); + packet + } +} + +impl ProbeSpec { + /// Drop the deviation, leaving a flow the configuration is meant to masquerade. + pub(crate) fn clear_stray(&mut self) { + self.stray = None; + } + + /// Interpret this draw against a fabric. + pub(crate) fn resolve(self, fabric: &Fabric) -> Probe { + let mut arrival = Arrival::outbound(); + let mut source = fabric.private[self.source as usize % fabric.private.len()]; + let destination = fabric.peer[self.peer as usize % fabric.peer.len()]; + let mut exposed = true; + + match self.stray { + None => {} + Some(Stray::SourceNotExposed) => { + source = destination; + exposed = false; + } + Some(Stray::UnknownSourceVni) => arrival.src_vpcd = Some(vni(ABSENT_VNI)), + Some(Stray::UnknownDestVni) => arrival.dst_vpcd = Some(vni(ABSENT_VNI)), + Some(Stray::NotAskedFor) => arrival.wants_masquerade = false, + } + + Probe { + source, + destination, + sport: self.sport.max(1), + dport: self.dport.max(1), + exposed, + arrival, + stray: self.stray, + } + } +} diff --git a/nat/src/static_nat/fuzz.rs b/nat/src/static_nat/fuzz.rs new file mode 100644 index 0000000000..a1209ef8cf --- /dev/null +++ b/nat/src/static_nat/fuzz.rs @@ -0,0 +1,597 @@ +// SPDX-License-Identifier: Apache-2.0 +// Copyright Open Network Fabric Authors + +//! Properties of the static NAT network function, driven by generated configurations and packets. +//! +//! `setup::config_driven` already proves the *mapping* correct by enumeration: it builds the tables +//! a generated expose implies and checks that the two sides pair up one to one. Nothing there +//! touches a packet, a `Packet`'s metadata, or [`StaticNat`] itself. +//! +//! This module covers the rest of the stage, which is the half where the decisions live: +//! +//! * whether the mapping is applied to the packet's headers at all, and to which ones; +//! * whether it is applied when the arrival state does not ask for it, or forbids it; +//! * whether a packet it cannot look up is dropped with a reason or silently; and +//! * whether the two independently built halves of one expose still agree once each has been +//! applied to a real packet by real code. +//! +//! # No oracle +//! +//! None of these predicts what a source address should translate to. Each is either a metamorphic +//! relation -- a statement about how two runs relate -- or an invariant over one run's output. +//! Following the development guide's decomposition, the `config -> tables` half gets a differential +//! oracle by enumeration and the per-packet half gets relations, and the two compose without +//! anything needing to know the answer in advance. A property here that had to predict an address +//! would be a second copy of `RangeBuilder`, and two copies disagree. +//! +//! # Vacuity +//! +//! The failure mode that matters is not a wrong assertion but an assertion that never runs. A probe +//! that misses every table satisfies most of what follows trivially, and a generated overlay that +//! fails to validate satisfies all of it. Each property counts what it actually exercised and +//! asserts a floor on that count, so a change that quietly stops reaching the code leaves a failing +//! test rather than a green one. + +#![cfg(test)] + +use crate::static_nat::nf::StaticNat; +use crate::static_nat::probe::{Fabric, ProbeSpec, Stray}; +use bolero::{Driver, TypeGenerator, ValueGenerator}; +use concurrency::sync::atomic::{AtomicUsize, Ordering}; +use config::external::overlay::vpcpeering::VpcExpose; +use config::external::overlay::vpcpeering::contract::StaticNatExposes; +use net::buffer::TestBuffer; +use net::ip::NextHeader; +use net::packet::{DoneReason, Packet}; +use pipeline::NetworkFunction; +use std::collections::BTreeMap; +use std::net::IpAddr; +use std::num::NonZero; + +/// Exposes per configuration. More than one is what makes the tables hold several rules, which is +/// where a longest-prefix match has a choice to get wrong. +const MAX_EXPOSES: u8 = 3; + +/// The fewest reaching draws any property may see before it is considered vacuous. +const MIN_REACHED: usize = 8; + +/// Probes per configuration. Building the configuration costs far more than resolving a probe +/// against it, so a batch amortizes the expensive half over the interesting one. +const PROBES: usize = 8; + +/// A configuration and a batch of packets to put through it. +/// +/// The two halves are drawn from the same driver but independently of each other: a [`ProbeSpec`] +/// is indices and raw values, and means something only once [`ProbeSpec::resolve`] interprets it +/// against the fabric the exposes built. +#[derive(Debug, Clone, Copy)] +struct Scenario { + /// Whether probes may deviate from a packet the configuration translates. + /// + /// Off for the properties that are about the mapping surviving the round trip, since a probe + /// that is meant to miss has nothing to round trip; on for the ones about the stage's own + /// decisions, which is all a stray exercises. + strays: bool, + /// Which flavour of expose to draw. + exposes: StaticNatExposes, +} + +impl Scenario { + /// Address-to-address exposes, taking the mapping down `AddrTranslationValue`. + fn addresses(strays: bool) -> Self { + Self { + strays, + exposes: StaticNatExposes::addresses_only(MAX_EXPOSES), + } + } + + /// Exposes carrying port ranges, taking the mapping down `PortAddrTranslationValue` instead. + /// + /// A separate property per flavour rather than one over a mix. A mixed property reaches each + /// path eventually; one that asks for a path reaches it every time and says in its name which + /// one failed. + fn ports(strays: bool) -> Self { + Self { + strays, + exposes: StaticNatExposes::with_ports(MAX_EXPOSES), + } + } +} + +impl ValueGenerator for Scenario { + type Output = (Vec, Vec); + + fn generate(&self, driver: &mut D) -> Option { + let exposes = self.exposes.generate(driver)?; + + let mut probes = Vec::with_capacity(PROBES); + for _ in 0..PROBES { + let mut probe = ProbeSpec::generate(driver)?; + if !self.strays { + probe.clear_stray(); + } + probes.push(probe); + } + Some((exposes, probes)) + } +} + +/// Put a batch through the stage and collect what comes out. +/// +/// Nothing is filtered: every probe carries `keep`, so a packet the stage drops still appears in +/// the output with its reason attached. Without that a drop is indistinguishable from a +/// pass-through, and half of what follows could not be stated. +fn run(nf: &mut StaticNat, packets: Vec>) -> Vec> { + nf.process(packets.into_iter()).collect() +} + +/// Build the fabric a scenario describes, or report that the overlay was refused. +/// +/// A refusal is legitimate: each expose is valid on its own by construction, but two of them may +/// overlap, and a manifest rejects that. Callers count refusals rather than ignoring them. +fn fabric(exposes: &[VpcExpose]) -> Option { + let fabric = Fabric::build(exposes)?; + fabric.is_probeable().then_some(fabric) +} + +/// The source half of a packet's five-tuple. +/// +/// Address and port together, because that is the granularity static NAT maps at once an expose +/// carries port ranges: comparing addresses alone would call a translation that moved only the port +/// "unchanged", and every property below would then skip it. +fn five_tuple_source(packet: &Packet) -> (IpAddr, u16) { + ( + packet + .ip_source() + .unwrap_or_else(|| unreachable!("a probe is always an ip packet")), + packet.transport_src_port().map_or(0, NonZero::get), + ) +} + +/// The destination half, for judging a reply. +fn five_tuple_destination(packet: &Packet) -> (IpAddr, u16) { + ( + packet + .ip_destination() + .unwrap_or_else(|| unreachable!("a probe is always an ip packet")), + packet.transport_dst_port().map_or(0, NonZero::get), + ) +} + +/// How much of a run actually reached the code under test. +#[derive(Default)] +struct Tally { + /// Scenarios drawn. + seen: AtomicUsize, + /// Scenarios whose overlay validated and built a non-empty table. + built: AtomicUsize, + /// Probes that reached the assertion the property is about. + reached: AtomicUsize, +} + +impl Tally { + /// Assert the run was not vacuous. + /// + /// The floor is **relative to the configurations actually built**, not an absolute count, because + /// an absolute one is really a measure of how fast the machine was. A property that reached + /// thousands of probes alone can reach a few dozen when it runs beside nine hundred other + /// tests on a loaded machine or under coverage instrumentation, and a floor tuned to the fast + /// case then fails for a reason that has nothing to do with the code under test. + /// + /// Both counts scale with the iteration budget, so their ratio does not. What the guard is for is + /// a property that has stopped reaching its assertion at all -- and a collapse to zero is just as + /// visible in the ratio. + fn report(&self, what: &str) { + let (seen, built, reached) = ( + self.seen.load(Ordering::Relaxed), + self.built.load(Ordering::Relaxed), + self.reached.load(Ordering::Relaxed), + ); + println!("{what}: {built}/{seen} configurations built, {reached} probes reached it"); + assert!( + built * 2 >= seen, + "only {built} of {seen} configurations built, so this checked much less than it looks \ + like it did" + ); + // At least one reaching probes for every two configurations built, and never zero. + assert!( + reached >= MIN_REACHED && reached * 2 >= built, + "{reached} probes reached the {what} assertion across {built} configurations; \ + this property has gone vacuous" + ); + } +} + +/// A translated source comes back to where it started. +/// +/// The headline property, and the one that needs two tables. A packet leaving the local vpc has its +/// source rewritten by that vpc's table, which was built from the *local* side of the peering. The +/// reply arrives at the peer, whose table rewrites destinations and was built from the *remote* +/// side of the same peering -- a separate pass over separate data, by a separate code path +/// (`find_dst_mapping` against `dst_nat` rather than `find_src_mapping` against `src_nat`). +/// +/// So this is the one statement that ties the two halves together, and it is stated without knowing +/// what either produces: whatever the first one did, the second must undo. +/// +/// The development guide names this relation directly -- *translate then reverse is the identity on +/// the five-tuple* -- as the per-packet half of the decomposition. +fn drive_round_trip(scenario: Scenario) { + let tally = Tally::default(); + + bolero::check!().with_generator(scenario).cloned().for_each( + |(exposes, probes): (Vec, Vec)| { + tally.seen.fetch_add(1, Ordering::Relaxed); + let Some(fabric) = fabric(&exposes) else { + return; + }; + tally.built.fetch_add(1, Ordering::Relaxed); + let mut nf = fabric.nf(); + + for spec in &probes { + let mut probe = (*spec).resolve(&fabric); + let (source, sport) = (probe.source, probe.sport); + let out = run(&mut nf, vec![probe.take()]); + let (translated, translated_port) = five_tuple_source(&out[0]); + + // An exposed source the tables do not cover is not a finding here: the mapping's + // completeness is proved by enumeration in `setup::config_driven`. This property is + // about what happens once a translation has occurred. + if (translated, translated_port) == (source, sport) { + continue; + } + + let back = run(&mut nf, vec![probe.reply(translated, translated_port)]); + let (returned, returned_port) = five_tuple_destination(&back[0]); + + assert_eq!( + (returned, returned_port), + (source, sport), + "{source}:{sport} translated to {translated}:{translated_port} on the way out, \ + and the reply came back to {returned}:{returned_port}" + ); + tally.reached.fetch_add(1, Ordering::Relaxed); + } + }, + ); + + tally.report("round trip"); +} + +#[test] +fn a_translated_source_comes_back() { + drive_round_trip(Scenario::addresses(false)); +} + +/// The same, where the mapping moves the port as well as the address. +/// +/// A second code path entirely -- `PortAddrTranslationValue` rather than `AddrTranslationValue` -- +/// and the harder one, since the two sides may divide their common total between addresses and +/// ports differently. A `/32` carrying 64 ports is a legal answer to a `/30` carrying 16, so the +/// reverse mapping cannot recover the address without also accounting for the port. +#[test] +fn a_translated_source_and_port_come_back() { + drive_round_trip(Scenario::ports(false)); +} + +/// Two sources that differ stay different after translation. +/// +/// Static NAT is one-to-one by definition, so a collision is a tenant isolation defect rather than a +/// performance one: two flows arriving at the peer as the same address and port are +/// indistinguishable to everything downstream, including the reverse mapping. +/// +/// `setup::config_driven` proves the *table* injective. This proves the stage is, which is a +/// different claim: the table could be right and the write to the packet's headers wrong, and no +/// table-level property would see it. +fn drive_injectivity(scenario: Scenario) { + let tally = Tally::default(); + + bolero::check!().with_generator(scenario).cloned().for_each( + |(exposes, _probes): (Vec, Vec)| { + tally.seen.fetch_add(1, Ordering::Relaxed); + let Some(fabric) = fabric(&exposes) else { + return; + }; + tally.built.fetch_add(1, Ordering::Relaxed); + let mut nf = fabric.nf(); + + // Everything the configuration maps, not the drawn probes: the draws may repeat, and a + // collision is only visible across distinct inputs. + let sources = fabric.every_source(); + let batch: Vec> = sources + .iter() + .map(|(endpoint, port)| fabric.outbound_to_peer(*endpoint, *port)) + .collect(); + let out = run(&mut nf, batch); + + let mut taken: BTreeMap<(IpAddr, u16), (IpAddr, u16)> = BTreeMap::new(); + for ((endpoint, port), packet) in sources.iter().zip(out.iter()) { + let before = (endpoint.addr, *port); + let after = five_tuple_source(packet); + if after == before { + continue; + } + if let Some(previous) = taken.insert(after, before) { + let (addr, port) = after; + let (pa, pp) = previous; + let (ba, bp) = before; + panic!( + "{ba}:{bp} and {pa}:{pp} both translated to {addr}:{port}, so static NAT \ + is not one to one for {exposes:#?}" + ); + } + tally.reached.fetch_add(1, Ordering::Relaxed); + } + }, + ); + + tally.report("injectivity"); +} + +#[test] +fn distinct_sources_stay_distinct() { + drive_injectivity(Scenario::addresses(false)); +} + +/// The same over address-and-port pairs. +/// +/// Sweeping addresses alone here would check a diagonal of the space and call it injective: with +/// port ranges the thing the mapping is one to one over is the pair, so two ports on one address +/// colliding is a defect an address-only sweep cannot see. +#[test] +fn distinct_sources_and_ports_stay_distinct() { + drive_injectivity(Scenario::ports(false)); +} + +/// Translating the source leaves everything else alone. +/// +/// The frame condition for this stage, and it differs between the two paths -- which is the point of +/// stating it per flavour rather than once. With no port range on the expose the transport ports are +/// part of the frame and a rewrite would be a mapping reaching further than it was configured to; +/// with one they are part of what is being translated, and only the destination and the protocol +/// remain. +/// +/// The destination matters in both. The local vpc's table also holds a destination half, built from +/// its peer's manifest; the peer offers no translation, so an outbound packet's destination must come +/// through untouched, and a rewrite would mean the two halves of the table are bleeding into each +/// other. +fn drive_frame(scenario: Scenario) { + let tally = Tally::default(); + + bolero::check!().with_generator(scenario).cloned().for_each( + |(exposes, probes): (Vec, Vec)| { + tally.seen.fetch_add(1, Ordering::Relaxed); + let Some(fabric) = fabric(&exposes) else { + return; + }; + tally.built.fetch_add(1, Ordering::Relaxed); + let mut nf = fabric.nf(); + + for spec in &probes { + let mut probe = (*spec).resolve(&fabric); + let (destination, sport, dport) = (probe.destination, probe.sport, probe.dport); + let proto = if probe.tcp { + NextHeader::TCP + } else { + NextHeader::UDP + }; + let out = run(&mut nf, vec![probe.take()]); + let packet = &out[0]; + + assert_eq!( + packet.ip_destination(), + Some(destination), + "source translation rewrote the destination" + ); + assert_eq!( + packet.transport_dst_port().map(NonZero::get), + Some(dport), + "source translation rewrote the destination port" + ); + assert_eq!( + packet.ip_proto(), + Some(proto), + "source translation changed the transport protocol" + ); + if !fabric.uses_ports { + assert_eq!( + packet.transport_src_port().map(NonZero::get), + Some(sport), + "source translation rewrote the source port, which no expose asked for" + ); + } + tally.reached.fetch_add(1, Ordering::Relaxed); + } + }, + ); + + tally.report("frame"); +} + +#[test] +fn translation_touches_only_the_source() { + drive_frame(Scenario::addresses(false)); +} + +#[test] +fn port_translation_touches_only_the_source() { + drive_frame(Scenario::ports(false)); +} + +/// Nothing is translated that did not ask to be. +/// +/// The arrival state is the stage's precondition, and every flag in it is a decision an upstream +/// stage made. `requires_static_nat_src` says this packet is to be translated; `is_src_natted` says +/// something already has. Ignoring either means translating a packet twice, or translating one the +/// pipeline had decided to leave alone -- both of which produce an address the reverse mapping +/// cannot undo. +/// +/// A source the exposes do not offer is the same claim from the other side: the stage may only act +/// on what the configuration named. +fn drive_permission(scenario: Scenario) { + let tally = Tally::default(); + + bolero::check!().with_generator(scenario).cloned().for_each( + |(exposes, probes): (Vec, Vec)| { + tally.seen.fetch_add(1, Ordering::Relaxed); + let Some(fabric) = fabric(&exposes) else { + return; + }; + tally.built.fetch_add(1, Ordering::Relaxed); + let mut nf = fabric.nf(); + + for spec in &probes { + let mut probe = (*spec).resolve(&fabric); + // Every reason a probe may not be translated, taken together: the request was not + // made, an earlier stage already made it, the annotations needed to answer it are + // missing or name something the configuration does not have, or the source is an + // address no expose offers. Whichever it is, the source must come out as it went in. + if probe.asks_for_translation() && probe.exposed { + continue; + } + + let (source, sport) = (probe.source, probe.sport); + let (stray, arrival) = (probe.stray, probe.arrival); + let out = run(&mut nf, vec![probe.take()]); + + assert_eq!( + five_tuple_source(&out[0]), + (source, sport), + "static NAT translated {source}:{sport} although {stray:?} forbade it; the \ + packet arrived as {arrival:?}" + ); + tally.reached.fetch_add(1, Ordering::Relaxed); + } + }, + ); + + tally.report("permission"); +} + +#[test] +fn nothing_is_translated_without_permission() { + drive_permission(Scenario::addresses(true)); +} + +#[test] +fn no_port_is_translated_without_permission() { + drive_permission(Scenario::ports(true)); +} + +/// A packet the stage cannot look up is dropped, and says why. +/// +/// The dataplane's universal obligation, and the cheapest one to state: an outcome the operator can +/// see beats a correct outcome nobody can explain. `DoneReason` is the vocabulary, so the assertion +/// is that the packet carries one and that it is the one that describes what happened. +/// +/// A silent pass here is the real failure: a packet whose source vpc is unknown has no table, so +/// letting it through means forwarding untranslated traffic under a configuration that never +/// mentioned it. +fn drive_attribution(scenario: Scenario) { + let tally = Tally::default(); + + bolero::check!().with_generator(scenario).cloned().for_each( + |(exposes, probes): (Vec, Vec)| { + tally.seen.fetch_add(1, Ordering::Relaxed); + let Some(fabric) = fabric(&exposes) else { + return; + }; + tally.built.fetch_add(1, Ordering::Relaxed); + let mut nf = fabric.nf(); + + for spec in &probes { + let mut probe = (*spec).resolve(&fabric); + let unroutable = matches!( + probe.stray, + Some(Stray::NoSourceVni | Stray::UnknownSourceVni) + ); + if !unroutable { + continue; + } + + let (source, stray) = (probe.source, probe.stray); + let out = run(&mut nf, vec![probe.take()]); + + let reason = out[0].get_done().unwrap_or_else(|| { + panic!( + "a packet with {stray:?} passed static NAT with no verdict at all, so \ + {source} would be forwarded untranslated" + ) + }); + assert_eq!( + reason, + DoneReason::Unroutable, + "a packet with {stray:?} was dropped for {reason:?}, which does not describe \ + what happened to it" + ); + tally.reached.fetch_add(1, Ordering::Relaxed); + } + }, + ); + + tally.report("attribution"); +} + +#[test] +fn a_packet_that_cannot_be_looked_up_says_so() { + drive_attribution(Scenario::addresses(true)); +} + +/// A packet whose five-tuple changed is marked as having changed. +/// +/// Static NAT rewrites headers in place and leaves the transport checksum stale, relying on +/// `checksum_refresh` to have a later stage fix it. So the mark is not bookkeeping: a translated +/// packet that is not marked goes out with a checksum for the addresses it no longer carries, and is +/// discarded by the receiver rather than by anything that could report it. +/// +/// `is_src_natted` carries the same weight in the other direction -- it is what stops a second NAT +/// stage translating the packet again. +fn drive_marking(scenario: Scenario) { + let tally = Tally::default(); + + bolero::check!().with_generator(scenario).cloned().for_each( + |(exposes, probes): (Vec, Vec)| { + tally.seen.fetch_add(1, Ordering::Relaxed); + let Some(fabric) = fabric(&exposes) else { + return; + }; + tally.built.fetch_add(1, Ordering::Relaxed); + let mut nf = fabric.nf(); + + for spec in &probes { + let mut probe = (*spec).resolve(&fabric); + let before = (probe.source, probe.sport); + let out = run(&mut nf, vec![probe.take()]); + let packet = &out[0]; + + if five_tuple_source(packet) == before { + continue; + } + let (source, sport) = before; + + assert!( + packet.meta().is_src_natted(), + "{source}:{sport} was translated without the source-natted mark, so a later \ + stage would translate it again" + ); + assert!( + packet.meta().checksum_refresh(), + "{source}:{sport} was translated without asking for a checksum refresh, so the \ + packet goes out with a checksum for headers it no longer carries" + ); + tally.reached.fetch_add(1, Ordering::Relaxed); + } + }, + ); + + tally.report("marking"); +} + +#[test] +fn a_modified_packet_is_always_marked() { + drive_marking(Scenario::addresses(true)); +} + +#[test] +fn a_port_modified_packet_is_always_marked() { + drive_marking(Scenario::ports(true)); +} diff --git a/nat/src/static_nat/mod.rs b/nat/src/static_nat/mod.rs index 844cefa19a..a2bf321741 100644 --- a/nat/src/static_nat/mod.rs +++ b/nat/src/static_nat/mod.rs @@ -3,8 +3,10 @@ //! Static NAT implementation +pub(crate) mod fuzz; pub mod natrw; pub mod nf; +pub(crate) mod probe; pub mod setup; pub(crate) mod test; diff --git a/nat/src/static_nat/probe.rs b/nat/src/static_nat/probe.rs new file mode 100644 index 0000000000..ee6efeea70 --- /dev/null +++ b/nat/src/static_nat/probe.rs @@ -0,0 +1,538 @@ +// SPDX-License-Identifier: Apache-2.0 +// Copyright Open Network Fabric Authors + +//! Packets drawn relative to a static NAT configuration. +//! +//! A [`bolero::TypeGenerator`] over `Packet` produces packets that miss every table a generated +//! configuration builds, so a property driven by one explores the miss path and nothing else. The +//! [development guide][crate] makes the same argument one level up, about generating configuration +//! values rather than building configurations from operations: a generator that does not know what +//! the thing under test is configured for reaches only its rejection paths. +//! +//! So the configuration is a **parameter to resolution**, not a predicate to filter against. A +//! [`ProbeSpec`] is drawn without reference to any configuration -- it is a handful of indices -- +//! and [`ProbeSpec::resolve`] interprets it against a [`Fabric`]. Resolution is total: every draw +//! becomes a packet, and the ones that are *meant* to miss miss deliberately, named by [`Stray`], +//! rather than by accident. +//! +//! This mirrors `acl-filter`'s `ProbeSpec`, which resolves against a built overlay the same way. +//! +//! # The arrival state is the network function's precondition +//! +//! [`StaticNat`] sits in the middle of the pipeline and assumes its predecessors have annotated the +//! packet: a source and destination VPC discriminant, the overlay flag, and the two flags saying +//! which directions of translation are wanted. Nothing in the type system says so -- `process` +//! silently passes over a packet that lacks them, and `process_packet` drops one whose +//! discriminants are missing. +//! +//! [`Arrival`] writes that state down in one place. It is the network function's precondition made +//! explicit, which is what the development guide asks for when it puts contracts on functions +//! rather than on the pipeline: the assumption travels with the stage instead of being re-derived +//! by every test that drives it. `masquerade`'s tests hand-roll the same thing as a mock stage. + +#![cfg(test)] + +use crate::static_nat::nf::StaticNat; +use crate::static_nat::setup::build_nat_configuration; +use bolero::TypeGenerator; +use config::external::overlay::vpcpeering::VpcExpose; +use config::external::overlay::vpcpeering::contract::{ + LOCAL_VNI, REMOTE_VNI, overlay_with_exposes, +}; +use lpm::prefix::{PortRange, PrefixWithOptionalPorts}; +use net::buffer::TestBuffer; +use net::ip::{NextHeader, UnicastIpAddr}; +use net::packet::test_utils::{ + build_test_ipv4_packet_with_transport, build_test_ipv6_packet_with_transport, +}; +use net::packet::{Packet, VpcDiscriminant}; +use net::tcp::port::TcpPort; +use net::udp::UdpPort; +use net::vxlan::Vni; +use std::collections::BTreeSet; +use std::net::IpAddr; + +/// The TTL every probe is built with, so that a property can tell a translation from a rewrite of +/// anything else. +pub(crate) const PROBE_TTL: u8 = 64; + +/// A VNI no generated configuration uses, for the probe that asks to be looked up in a table that +/// does not exist. +const ABSENT_VNI: u32 = 4_000; + +pub(crate) fn vni(raw: u32) -> Vni { + Vni::new_checked(raw).unwrap_or_else(|_| unreachable!("{raw} is a legal vni")) +} + +/// One address the configuration names, and the ports it names alongside it. +/// +/// Static NAT permits a port range on a prefix, and a prefix that carries one is mapped address and +/// port *together*: the private side's total, counted as addresses times ports, has to equal the +/// public side's, but the two may divide that total differently. So an address on its own is not a +/// thing the configuration maps -- the pair is -- and a probe has to carry the range it may draw a +/// port from or it will miss. +#[derive(Debug, Clone, Copy, PartialEq, Eq, PartialOrd, Ord)] +pub(crate) struct Endpoint { + pub(crate) addr: IpAddr, + /// The ports the prefix this address came from carries, if any. + pub(crate) ports: Option, +} + +impl Endpoint { + /// A port this endpoint is mapped on, chosen by an arbitrary index. + /// + /// Total, so a draw always lands on a port the configuration covers rather than near one. Port + /// 0 is not a legal port on either transport and no expose may name it. + pub(crate) fn port(&self, index: u16) -> u16 { + match self.ports { + None => index.max(1), + Some(range) => { + let len = u32::try_from(range.len()).unwrap_or(u32::from(u16::MAX)); + let offset = u32::from(index) % len.max(1); + u16::try_from(u32::from(range.start()) + offset).unwrap_or(range.end()) + } + } + } +} + +/// Every address-and-ports pair a set of prefixes covers. +/// +/// The static NAT generator keeps both sides of an expose small enough that this is a handful of +/// endpoints, which is what lets a property enumerate rather than sample. +pub(crate) fn endpoints(prefixes: &BTreeSet) -> Vec { + let mut out = Vec::new(); + for prefix_with_ports in prefixes { + let ports = prefix_with_ports.ports(); + let prefix = prefix_with_ports.prefix(); + let (start, end) = (prefix.as_address(), prefix.last_address()); + let (mut bits, last) = match (start, end) { + (IpAddr::V4(a), IpAddr::V4(b)) => (u128::from(a.to_bits()), u128::from(b.to_bits())), + (IpAddr::V6(a), IpAddr::V6(b)) => (a.to_bits(), b.to_bits()), + _ => unreachable!("a prefix does not change address family"), + }; + while bits <= last { + out.push(Endpoint { + addr: match start { + IpAddr::V4(_) => IpAddr::V4( + u32::try_from(bits) + .unwrap_or_else(|_| unreachable!()) + .into(), + ), + IpAddr::V6(_) => IpAddr::V6(bits.into()), + }, + ports, + }); + bits += 1; + } + } + out +} + +/// A built static NAT configuration, and the address sets it declares. +/// +/// The two vpcs are the ones [`overlay_with_exposes`] builds: `VPC-1` at [`LOCAL_VNI`] offers the +/// generated exposes, and `VPC-2` at [`REMOTE_VNI`] offers one unrelated prefix with no translation +/// on it. That asymmetry is what makes the round trip a property over two independently built +/// tables rather than over one: +/// +/// * `VPC-1`'s table translates **sources**, private to public, since the exposes are its own; and +/// * `VPC-2`'s table translates **destinations**, public back to private, since it builds that half +/// from its peer's manifest. +/// +/// So a packet leaving `VPC-1` and the reply coming back to it are handled by different tables built +/// from opposite ends of the same expose, and the two must agree. +pub(crate) struct Fabric { + writer: crate::static_nat::natrw::NatTablesWriter, + /// Every endpoint the local exposes offer, before translation. + pub(crate) private: Vec, + /// Every endpoint the local exposes translate to. + pub(crate) public: Vec, + /// Addresses in the peer vpc, which no expose translates. + pub(crate) peer: Vec, + /// Whether the exposes carry port ranges, so the mapping moves ports as well as addresses. + /// + /// The two paths differ in what a property may assert: with no port range the transport ports + /// are part of the frame and must survive untouched, and with one they are part of what is + /// being translated. + pub(crate) uses_ports: bool, +} + +impl Fabric { + /// Build the tables a set of exposes implies, or `None` if the overlay they form is not valid. + /// + /// A rejection here is a legitimate outcome rather than a failure: exposes are generated one at + /// a time and two of them may overlap, which a manifest refuses. The properties count how often + /// it happens so that a generator change that starts rejecting everything cannot pass quietly. + pub(crate) fn build(exposes: &[VpcExpose]) -> Option { + let private: Vec = exposes.iter().flat_map(|e| endpoints(&e.ips)).collect(); + let public: Vec = exposes + .iter() + .filter_map(|e| e.nat.as_ref()) + .flat_map(|nat| endpoints(&nat.as_range)) + .collect(); + let uses_ports = private.iter().chain(&public).any(|e| e.ports.is_some()); + + let overlay = overlay_with_exposes(exposes.to_vec()).ok()?; + let validated = overlay.validate().ok()?; + let tables = build_nat_configuration(validated.vpc_table()).ok()?; + + // The peer prefix `overlay_with_exposes` fixes, in whichever family the exposes chose. + let peer = match private.first().map(|e| e.addr) { + Some(IpAddr::V6(_)) => vec![ + "2001:db8:ffff::1" + .parse() + .unwrap_or_else(|_| unreachable!()), + "2001:db8:ffff::2" + .parse() + .unwrap_or_else(|_| unreachable!()), + ], + _ => vec![ + "3.3.3.1".parse().unwrap_or_else(|_| unreachable!()), + "3.3.3.2".parse().unwrap_or_else(|_| unreachable!()), + ], + }; + + let mut writer = crate::static_nat::natrw::NatTablesWriter::new(); + writer.update_nat_tables(tables); + Some(Self { + writer, + private, + public, + peer, + uses_ports, + }) + } + + /// A network function reading these tables. + /// + /// Fresh per call: `StaticNat` holds no state of its own, so a property that wants to know a + /// batch was not influenced by an earlier one can simply take another. + pub(crate) fn nf(&self) -> StaticNat { + StaticNat::with_reader("probe", self.writer.get_reader()) + } + + /// An outbound packet from `source` on `port` to the peer. + /// + /// For a property that wants to sweep everything the configuration offers rather than the drawn + /// ones -- injectivity, which is only visible across distinct inputs and so cannot be left to a + /// draw that may repeat. + pub(crate) fn outbound_to_peer(&self, source: Endpoint, port: u16) -> Packet { + let mut packet = build(source.addr, self.peer[0], false, port, 80); + Arrival::outbound().stamp(&mut packet); + packet + } + + /// Every distinct thing the configuration maps, as a source and a port to send it from. + /// + /// With no port range that is one entry per address. With one it is every address-and-port pair, + /// since the pair is what the mapping is one to one over -- sweeping addresses alone would check + /// a diagonal of the space and call it injective. + pub(crate) fn every_source(&self) -> Vec<(Endpoint, u16)> { + self.private + .iter() + .flat_map(|endpoint| match endpoint.ports { + None => vec![(*endpoint, 1024)], + Some(range) => (range.start()..=range.end()) + .map(|port| (*endpoint, port)) + .collect(), + }) + .collect() + } + + /// Whether this fabric can be probed at all. + /// + /// An expose whose two sides are empty builds a table with nothing in it, and every probe + /// against it misses. Properties skip those rather than count them as passes. + pub(crate) fn is_probeable(&self) -> bool { + !self.private.is_empty() && !self.public.is_empty() + } +} + +/// The metadata a packet must carry for [`StaticNat`] to look at it. +/// +/// Every field here is something an upstream stage sets in production. Writing them out is what +/// makes this a test of static NAT rather than a test of whatever mock supplies them. +#[derive(Debug, Clone, Copy)] +pub(crate) struct Arrival { + /// The vpc the packet came from, which selects the table. + pub(crate) src_vpcd: Option, + /// The vpc the packet is going to, which selects the source-translation half of it. + pub(crate) dst_vpcd: Option, + pub(crate) wants_src_nat: bool, + pub(crate) wants_dst_nat: bool, + /// Set when an earlier stage has already translated the source, which static NAT must respect. + pub(crate) already_src_natted: bool, +} + +impl Arrival { + /// Leaving the local vpc for its peer: source translation, private to public. + pub(crate) fn outbound() -> Self { + Self { + src_vpcd: Some(vni(LOCAL_VNI)), + dst_vpcd: Some(vni(REMOTE_VNI)), + wants_src_nat: true, + wants_dst_nat: false, + already_src_natted: false, + } + } + + /// The reply, arriving at the peer for the local vpc: destination translation, public back to + /// private. + pub(crate) fn inbound() -> Self { + Self { + src_vpcd: Some(vni(REMOTE_VNI)), + dst_vpcd: Some(vni(LOCAL_VNI)), + wants_src_nat: false, + wants_dst_nat: true, + already_src_natted: false, + } + } + + /// Stamp the state onto a packet. + /// + /// `set_keep` is what makes a dropped packet observable: `Packet::enforce` removes a dropped + /// packet from the output iterator, so without it a drop and a translation-that-did-nothing are + /// the same event seen from outside, and no property could tell them apart. + pub(crate) fn stamp(self, packet: &mut Packet) { + let meta = packet.meta_mut(); + meta.src_vpcd = self.src_vpcd.map(VpcDiscriminant::from_vni); + meta.dst_vpcd = self.dst_vpcd.map(VpcDiscriminant::from_vni); + meta.set_overlay(true); + meta.set_keep(true); + meta.set_static_nat_src(self.wants_src_nat); + meta.set_static_nat_dst(self.wants_dst_nat); + meta.src_natted(self.already_src_natted); + } +} + +/// A deliberate deviation from a packet the configuration translates. +/// +/// Each one is a question about the network function's own decisions rather than about the mapping: +/// the mapping is covered by enumeration at the table level, and none of these reach it. +#[derive(Debug, Clone, Copy, TypeGenerator)] +pub(crate) enum Stray { + /// A source address no expose offers. Nothing should translate it. + SourceNotExposed, + /// No source vpc annotation, which the stage cannot proceed without. + NoSourceVni, + /// A source vpc with no table of its own. + UnknownSourceVni, + /// A destination vpc the local vpc does not peer with, so the source half finds no table. + UnknownDestVni, + /// An earlier stage has already translated the source. + AlreadySourceNatted, + /// Nothing asked for translation, so the stage should pass the packet through untouched. + NotAskedFor, +} + +/// A drawn probe, before it knows anything about a configuration. +/// +/// Deliberately all indices and raw values: nothing here refers to a prefix, an address or a vni, so +/// the same draw is meaningful against any fabric and shrinking stays interpretable. +#[derive(Debug, Clone, Copy, TypeGenerator)] +pub(crate) struct ProbeSpec { + source: u8, + peer: u8, + tcp: bool, + sport: u16, + dport: u16, + stray: Option, +} + +/// A probe resolved against a fabric: the packet, and the facts a property may reason from. +/// +/// The facts are all *inputs* -- what was built and what was asked for. None of them is a +/// prediction of what static NAT should produce, because a prediction is a second implementation of +/// the mapping and the point of resolving against the configuration is not to need one. +pub(crate) struct Probe { + /// The packet itself, taken out by [`Probe::take`] when it is handed to the stage. + /// + /// Held in an `Option` so that taking it does not move out of the probe: the remaining fields + /// are what a property asserts against afterwards, and [`Probe::reply`] needs them once the + /// outbound packet is gone. + packet: Option>, + /// The source address as built. + pub(crate) source: IpAddr, + /// The destination address as built. + pub(crate) destination: IpAddr, + pub(crate) sport: u16, + pub(crate) dport: u16, + pub(crate) tcp: bool, + /// Whether the local exposes offer `source`. + pub(crate) exposed: bool, + /// The arrival state the packet carries. + pub(crate) arrival: Arrival, + pub(crate) stray: Option, +} + +impl Probe { + /// The packet, to hand to the stage. + /// + /// # Panics + /// + /// Panics if called twice. A probe is one packet; a property that wants the same five-tuple + /// again should resolve the spec again, which is cheap and says so plainly. + pub(crate) fn take(&mut self) -> Packet { + self.packet + .take() + .unwrap_or_else(|| unreachable!("a probe's packet is taken once")) + } + + /// Whether static NAT was both asked to translate the source and given everything it needs to. + /// + /// This is a statement about the *request*, not about the mapping: a probe that is `expected` may + /// still legitimately go untranslated if no rule covers its source. What it may not do is come + /// out translated when this is false. + pub(crate) fn asks_for_translation(&self) -> bool { + self.arrival.wants_src_nat + && !self.arrival.already_src_natted + && self.arrival.src_vpcd == Some(vni(LOCAL_VNI)) + && self.arrival.dst_vpcd == Some(vni(REMOTE_VNI)) + } + + /// The packet that answers this one, addressed to `translated`. + /// + /// The reply is what the peer would send back: the two ends swapped, and the local end named by + /// whatever the outbound translation produced rather than by what the sender used. It arrives at + /// the peer's vpc, so it is looked up in the peer's table -- the other half of the same expose, + /// built independently. + /// + /// The port matters as much as the address once the expose carries port ranges: the peer + /// answers the port it was contacted *from*, which is the translated one, and a reply sent to + /// the original port would miss the mapping and prove nothing. + pub(crate) fn reply(&self, translated: IpAddr, translated_port: u16) -> Packet { + let mut packet = build( + self.destination, + translated, + self.tcp, + self.dport, + translated_port, + ); + Arrival::inbound().stamp(&mut packet); + packet + } +} + +impl ProbeSpec { + /// Drop the deviation, leaving a probe the configuration is meant to translate. + /// + /// For the properties about what happens *after* a translation: a probe that misses on purpose + /// has no translation to say anything about, and would only dilute the batch. + pub(crate) fn clear_stray(&mut self) { + self.stray = None; + } + + /// Interpret this draw against a fabric. + /// + /// Total by construction: an index is taken modulo the set it selects from, so there is no draw + /// that fails to become a packet and no rejection loop to bias the distribution. + pub(crate) fn resolve(self, fabric: &Fabric) -> Probe { + let mut arrival = Arrival::outbound(); + let endpoint = fabric.private[self.source as usize % fabric.private.len()]; + + let destination = fabric.peer[self.peer as usize % fabric.peer.len()]; + let mut source = endpoint.addr; + // Drawn from the range the endpoint's prefix carries, so a probe against a configuration + // that maps ports lands on one it maps rather than beside it. + let mut sport = endpoint.port(self.sport); + let mut exposed = true; + + match self.stray { + None => {} + Some(Stray::SourceNotExposed) => { + source = destination; + // The peer's prefix carries no port range, so no port is the right one either. + sport = self.sport.max(1); + exposed = false; + } + Some(Stray::NoSourceVni) => arrival.src_vpcd = None, + Some(Stray::UnknownSourceVni) => arrival.src_vpcd = Some(vni(ABSENT_VNI)), + Some(Stray::UnknownDestVni) => arrival.dst_vpcd = Some(vni(ABSENT_VNI)), + Some(Stray::AlreadySourceNatted) => arrival.already_src_natted = true, + Some(Stray::NotAskedFor) => { + arrival.wants_src_nat = false; + arrival.wants_dst_nat = false; + } + } + + // Port 0 is not a legal port on either transport. The destination is in the peer vpc, which + // no expose translates, so its port is free. + let dport = self.dport.max(1); + let mut packet = build(source, destination, self.tcp, sport, dport); + arrival.stamp(&mut packet); + + Probe { + packet: Some(packet), + source, + destination, + sport, + dport, + tcp: self.tcp, + exposed, + arrival, + stray: self.stray, + } + } +} + +/// Build a packet with the given five-tuple. +/// +/// # Panics +/// +/// Panics if the two addresses are of different families. Resolution never mixes them, since an +/// expose is of one family throughout and the peer prefix is chosen to match. +pub(crate) fn build( + source: IpAddr, + destination: IpAddr, + tcp: bool, + sport: u16, + dport: u16, +) -> Packet { + let next_header = if tcp { + NextHeader::TCP + } else { + NextHeader::UDP + }; + let mut packet = match (source, destination) { + (IpAddr::V4(_), IpAddr::V4(_)) => { + build_test_ipv4_packet_with_transport(PROBE_TTL, Some(next_header)) + .unwrap_or_else(|e| unreachable!("{e:?}")) + } + (IpAddr::V6(_), IpAddr::V6(_)) => { + build_test_ipv6_packet_with_transport(PROBE_TTL, Some(next_header)) + .unwrap_or_else(|e| unreachable!("{e:?}")) + } + _ => unreachable!("a probe never mixes address families"), + }; + + packet + .set_ip_source(UnicastIpAddr::try_from(source).unwrap_or_else(|_| { + unreachable!("{source} is drawn from a prefix an expose offers, so it is unicast") + })) + .unwrap_or_else(|e| unreachable!("{e:?}")); + packet + .set_ip_destination(destination) + .unwrap_or_else(|e| unreachable!("{e:?}")); + + if tcp { + packet + .set_tcp_source_port(TcpPort::new_checked(sport).unwrap_or_else(|_| unreachable!())) + .unwrap_or_else(|e| unreachable!("{e:?}")); + packet + .set_tcp_destination_port( + TcpPort::new_checked(dport).unwrap_or_else(|_| unreachable!()), + ) + .unwrap_or_else(|e| unreachable!("{e:?}")); + } else { + packet + .set_udp_source_port(UdpPort::new_checked(sport).unwrap_or_else(|_| unreachable!())) + .unwrap_or_else(|e| unreachable!("{e:?}")); + packet + .set_udp_destination_port( + UdpPort::new_checked(dport).unwrap_or_else(|_| unreachable!()), + ) + .unwrap_or_else(|e| unreachable!("{e:?}")); + } + + packet +}