From dd4e341ae8993d46571bb482c68cb43950e48b8b Mon Sep 17 00:00:00 2001 From: DeFiDude <59237470+DeFiDude@users.noreply.github.com> Date: Sun, 3 May 2026 02:35:47 -0600 Subject: [PATCH] close flash milestone and activate transport rx --- FUNCTIONS.md | 14 +- MASTER_PLAN.md | 4 +- docs/milestones/README.md | 4 +- docs/milestones/milestone-4.md | 22 ++- docs/milestones/milestone-5.md | 333 +++++++++++++++++++++++++++++++++ 5 files changed, 369 insertions(+), 8 deletions(-) create mode 100644 docs/milestones/milestone-5.md diff --git a/FUNCTIONS.md b/FUNCTIONS.md index 13dbd58..d1cbd9e 100644 --- a/FUNCTIONS.md +++ b/FUNCTIONS.md @@ -52,7 +52,7 @@ post-milestone-1 task. Run `./verify --all` for the live tally.) hardware-RNG entropy properties) over the on-chip USB-Serial/JTAG endpoint per [ADR-0010](docs/adr/0010-usb-serial-jtag-backend.md). 12 hardware tests pass in ~6 s (run with `pytest --hardware tests/hardware/`). -- Total functions registered: **95** (excludes placeholder rows like +- Total functions registered: **101** (excludes placeholder rows like "(functions added when milestone N is activated)") - Verified: 94 (milestone 1 software side + ENTIRE milestone-2 crypto stack: SHA-256 family + SHA-512 family + HMAC + HKDF + AES-256-CBC stack + 13 X25519 functions + 11 Ed25519 functions (scalar arith, point ops, scalarmult, compress/decompress, keypair, sign, verify — all match pyca/cryptography under QEMU; RFC 7748 §5.2/§6.1 + RFC 8032 §7.1 vectors plus tampering rejection) + production HMAC-DRBG-SHA-256 RNG (NIST SP 800-90A Rev. 1 §10.1.2; `rng_entropy` raw-source layer + `hmac_drbg_update` + `rng_init` + `rng_bytes` together discharge the canonical NIST CAVP DRBGVS COUNT=0 KAT symbolically; on TARGET_C6 the entropy source is the on-chip LPPERI hardware RNG) + milestone-3 identity/destination/announce TX helpers (`identity_create`, `identity_hash`, `destination_name_hash`, `destination_hash`, `announce_build`, `announce_send`) + milestone-4 qemu flash model (`flash_init`, `flash_read`, `flash_write_page`, `flash_erase_sector`) + milestone-4 identity persistence (`identity_save`, `identity_load`) — all under ADR-0009) - Tier A coverage extended: the SHA-512 family (`sha512_init`, `sha512_compress`, `sha512_update`, `sha512_final`) now carries a Cryptol+SAW Tier A proof alongside the QEMU/hashlib KAT bridge. The SAW drivers discharge FIPS 180-4 §C.1 + §C.2 KATs symbolically over the 80-round transform + 16-word schedule, plus K-table constants, ROTR/ch/maj algebraic sanity, streaming associativity (small chunkings), and both padding paths (bl ≤ 111 single-block + bl > 111 two-block). @@ -80,7 +80,10 @@ post-milestone-1 task. Run `./verify --all` for the live tally.) - The X25519 algorithmic spec [proofs/crypto/x25519/X25519.cry](proofs/crypto/x25519/X25519.cry) and SAW driver are landed and proven against RFC 7748 §5.2 / §6.1 KATs; each of the 14 listed functions hangs off the same shared model. The asm implementation follows in subsequent commits. - Tested: 0 - In progress: 0 -- Planned: 1 (`uart_isr`) +- Planned: 7 (`uart_isr` plus milestone-5 transport RX functions: + `announce_parse`, `announce_validate`, `transport_path_init`, + `transport_path_update`, `transport_path_lookup`, and + `transport_process_announce`) The end-to-end milestone-1 demo path is observable: KISS-framed Reticulum packets sent to qemu's stdin produce `boot.ready`, `kiss.rx_frame`, and @@ -321,6 +324,8 @@ Reticulum announce transmission over the current KISS serial development interfa |----------|--------|-------|-----------|------|------| | `announce_build` | ◉ verified | | `identity_create`, `destination_name_hash`, `destination_hash`, `rng_bytes`, `ed25519_sign` | 0001, 0002, 0006, 0009 | [milestone-3](docs/milestones/milestone-3.md#announce_build) | | `announce_send` | ◉ verified | | `announce_build`, `packet_serialize_header`, `kiss_encode_frame`, `uart_tx_bytes` | 0001, 0002, 0004, 0006, 0009 | [milestone-3](docs/milestones/milestone-3.md#announce_send) | +| `announce_parse` | ☐ planned | | `packet_parse_header` | 0001, 0002, 0005, 0006, 0009 | [milestone-5](docs/milestones/milestone-5.md#announce_parse) | +| `announce_validate` | ☐ planned | | `announce_parse`, `identity_hash`, `destination_hash`, `ed25519_verify` | 0001, 0002, 0005, 0006, 0009 | [milestone-5](docs/milestones/milestone-5.md#announce_validate) | ## Module: `transport` @@ -328,7 +333,10 @@ Announce processing, path table, destination cache. Reticulum's routing layer. | Function | Status | Owner | Depends-on | ADRs | Spec | |----------|--------|-------|-----------|------|------| -| (functions added when milestone 5 is activated) | ☐ planned | | | | (milestone 5) | +| `transport_path_init` | ☐ planned | | — | 0001, 0002, 0005, 0009 | [milestone-5](docs/milestones/milestone-5.md#transport_path_init) | +| `transport_path_update` | ☐ planned | | `transport_path_init`, `clock_now_ms` | 0001, 0002, 0005, 0009 | [milestone-5](docs/milestones/milestone-5.md#transport_path_update) | +| `transport_path_lookup` | ☐ planned | | `transport_path_init` | 0001, 0002, 0005, 0009 | [milestone-5](docs/milestones/milestone-5.md#transport_path_lookup) | +| `transport_process_announce` | ☐ planned | | `announce_validate`, `transport_path_update` | 0001, 0002, 0004, 0005, 0006, 0009 | [milestone-5](docs/milestones/milestone-5.md#transport_process_announce) | ## Module: `link` diff --git a/MASTER_PLAN.md b/MASTER_PLAN.md index 5c78ad2..805b9df 100644 --- a/MASTER_PLAN.md +++ b/MASTER_PLAN.md @@ -101,8 +101,8 @@ developer working full-time, with verification overhead included. | 1 | Foundation stack + verifier infrastructure | Complete (2026-05-02) | 8–12 wk | Hardware demo passed on Adafruit ESP32-C6 Feather; harness + verifier dispatcher live | | 2 | Cryptographic primitives | Complete (2026-05-02) | 4–6 mo | Each primitive: KAT + formal equivalence + constant-time | | 3 | Identity + announce TX | Complete (2026-05-03) | 3–4 wk | TLA+ for announce state machine; signature verified end-to-end | -| 4 | Flash persistence | Active (2026-05-03) | 2–3 wk | Symbolic execution on flash driver; identity round-trip proven | -| 5 | Transport RX (announce processing, paths) | Planned | 4–6 wk | TLA+ for transport state; signature verify on inbound | +| 4 | Flash persistence | Complete (2026-05-03) | 2–3 wk | Symbolic execution on flash driver; identity round-trip proven on C6 hardware | +| 5 | Transport RX (announce processing, paths) | Active (2026-05-03) | 4–6 wk | TLA+ for transport state; signature verify on inbound | | 6 | Link establishment | Planned | 6–8 wk | TLA+ for link state machine; AES session round-trip proven | | 7 | Resource / channel | Planned | 4–6 wk | Refinement proof against reference behavior | | 8 | LoRa SPI interface | Planned | 4–6 wk | Driver contracts; symbolic execution; first wireless milestone | diff --git a/docs/milestones/README.md b/docs/milestones/README.md index a41930f..aafbd4f 100644 --- a/docs/milestones/README.md +++ b/docs/milestones/README.md @@ -13,8 +13,8 @@ spec for each milestone. | 1 | Foundation stack + verifier infrastructure | Complete (2026-05-02) | [milestone-1.md](milestone-1.md) | | 2 | Cryptographic primitives | Complete (2026-05-02) | [milestone-2.md](milestone-2.md) | | 3 | Identity + announce TX | Complete (2026-05-03) | [milestone-3.md](milestone-3.md) | -| 4 | Flash persistence | Active (2026-05-03) | [milestone-4.md](milestone-4.md) | -| 5 | Transport RX | Planned | (spec written when activated) | +| 4 | Flash persistence | Complete (2026-05-03) | [milestone-4.md](milestone-4.md) | +| 5 | Transport RX | Active (2026-05-03) | [milestone-5.md](milestone-5.md) | | 6 | Link establishment | Planned | (spec written when activated) | | 7 | Resource / channel | Planned | (spec written when activated) | | 8 | LoRa SPI interface | Planned | (spec written when activated) | diff --git a/docs/milestones/milestone-4.md b/docs/milestones/milestone-4.md index f7fc40d..b002821 100644 --- a/docs/milestones/milestone-4.md +++ b/docs/milestones/milestone-4.md @@ -1,7 +1,8 @@ # Milestone 4: Flash persistence -- **Status:** Active +- **Status:** Complete - **Started:** 2026-05-03 +- **Completed:** 2026-05-03 - **Estimate:** 2-3 weeks ## Goal @@ -276,3 +277,22 @@ The announce sender must use the persisted identity when one exists. | A power loss during erase/write can destroy the only identity copy | Single-slot storage is acceptable for milestone 4; the record checksum makes corruption detectable, and multi-slot wear leveling is deferred explicitly. | | QEMU cannot prove real reset retention | Require a TARGET_C6 hardware reset-retention test in addition to qemu-virt semantics. | | Identity persistence may accidentally log secret bytes | Keep logs to status events only and include no key material or hashes beyond existing public identity hash tests. | + +## Retrospective + +Milestone 4 closed faster than estimated because the flash scope stayed narrow: +one identity sector, one record page, and no wear-leveling. The qemu model and +Python proof were enough to pin the public flash contract before the C6 backend +landed. + +The physical C6 run caught the important hardware gap: the ROM flash helpers +reject reads until the ROM flash descriptor is configured by +`esp_rom_spiflash_config_param`. `flash_init` now installs the 4 MiB / 64 KiB / +4 KiB / 256-byte geometry before read/write/erase calls. The hardware +reset-retention test erases only `0x003ff000..0x003fffff`, creates and saves an +identity, resets without reflashing, and validates that the second announce uses +the same public identity. + +Single-slot erase-then-write remains acceptable for this milestone. Multi-slot +wear leveling, destination-cache persistence, and path-cache persistence should +wait until the transport table semantics are stable in milestone 5. diff --git a/docs/milestones/milestone-5.md b/docs/milestones/milestone-5.md new file mode 100644 index 0000000..0cbed51 --- /dev/null +++ b/docs/milestones/milestone-5.md @@ -0,0 +1,333 @@ +# Milestone 5: Transport RX + +- **Status:** Active +- **Started:** 2026-05-03 +- **Estimate:** 4-6 weeks + +## Goal + +Accept inbound Reticulum announces over the existing KISS development +interface, validate their signatures, and maintain a bounded in-RAM transport +path table. This is the first receive-side routing milestone: the node learns +peer destinations from announces without establishing links or forwarding +traffic yet. + +## Deliverables + +| Component | Spec section | Permanence | +|-----------|--------------|-----------| +| Inbound announce parser | [announce_parse](#announce_parse) | Forever | +| Inbound announce validator | [announce_validate](#announce_validate) | Forever | +| Transport path table | [path table](#path-table) | Forever | +| Announce-to-path processor | [transport_process_announce](#transport_process_announce) | Forever | +| Main-loop RX integration | [boot integration](#boot-integration) | Development path through LoRa milestone | +| Transport state-machine proof | [verifier plan](#verifier-plan) | Forever | + +## Definition of Done + +- [ ] [FUNCTIONS.md](../../FUNCTIONS.md) lists every milestone-5 function with + a source, tests, verifier artifact, and status `verified`. +- [ ] `announce_parse` accepts well-formed non-ratchet HEADER_1 announces and + rejects malformed flags, hops/context shape, short payloads, over-MDU + packets, and truncated signatures without copying out of bounds. +- [ ] `announce_validate` recomputes `identity_hash`, destination hash, and + Ed25519 signature validity for inbound announces, with negative tests for + tampered destination hash, public key, name hash, random hash, signature, + and app data. +- [ ] `transport_path_init`, `transport_path_update`, and + `transport_path_lookup` maintain a fixed-capacity path table with + deterministic replacement and no heap allocation. +- [ ] `transport_process_announce` validates a parsed announce, updates or + creates the path-table entry keyed by destination hash, and returns a + stable status code for accepted, duplicate, invalid, and full-table + cases. +- [ ] `_main` routes inbound Reticulum announce packets through + `transport_process_announce` while preserving existing packet parser logs + and the milestone-3 local `N` announce command. +- [ ] A TLA+ transport state model accepts every observable asm trace for + accept, reject, update, duplicate, and eviction cases. +- [ ] `make ci`, `make build TARGET=qemu-virt`, `make build TARGET=c6`, + `pytest --hardware tests/hardware/`, and `./verify ` pass for every + function added or modified in this milestone. + +## Scope + +Milestone 5 handles non-ratchet announces only. Link requests, encrypted +traffic, ratchets, retransmission, LoRa interfaces, and path persistence are +deferred. The path table is RAM-resident in this milestone; flash persistence +for destination/path caches waits until the update and eviction semantics are +stable. + +The inbound wire format is the same HEADER_1 announce described in +[milestone-3](milestone-3.md#wire-format): + +``` +flags[1] || hops[1] || destination_hash[16] || context[1] || +public_key[64] || name_hash[10] || random_hash[10] || +signature[64] || app_data[*] +``` + +The signed data is: + +``` +destination_hash || public_key || name_hash || random_hash || app_data +``` + +## Announce RX State + +State lives in `src/state/announce.S` and `src/state/transport.S`; constants +live in `src/include/announce.S` and `src/include/transport.S`. + +The parser writes a bounded `announce_rx_t` view into static storage or a +caller-provided output struct: + +| Field | Size | Meaning | +|-------|------|---------| +| `raw_len` | 4 | Full raw packet length | +| `payload_len` | 4 | Payload length after byte 18 context | +| `app_data_len` | 4 | Payload bytes after the signature | +| `destination_hash` | 16 | Packet destination hash | +| `public_key` | 64 | Announcing identity public key | +| `name_hash` | 10 | Destination name hash | +| `random_hash` | 10 | Announce random hash | +| `signature` | 64 | Ed25519 signature | +| `app_data_ptr` | 4 | Pointer into the original packet buffer | + +The parser may copy fixed fields into the struct but must not copy app data. +App data remains a `(ptr, len)` view into the already bounded KISS buffer. + +## Path Table + +Milestone 5 uses a fixed-capacity RAM table: + +``` +TRANSPORT_PATH_CAPACITY = 8 +TRANSPORT_INTERFACE_KISS = 1 +``` + +Each path entry stores: + +| Field | Size | Meaning | +|-------|------|---------| +| `valid` | 1 | Entry is populated | +| `interface_id` | 1 | `TRANSPORT_INTERFACE_KISS` for this milestone | +| `hops` | 1 | Packet hop count observed on receive | +| `reserved` | 1 | Zero | +| `last_seen_ms` | 4 | `clock_now_ms()` at update | +| `destination_hash` | 16 | Lookup key | +| `identity_hash` | 16 | `SHA256(public_key)[0:16]` | +| `public_key` | 64 | Announcing identity public key | + +Replacement is deterministic: update an existing destination hash first; else +use the first invalid entry; else replace the entry with the oldest +`last_seen_ms` using unsigned 32-bit age comparison. + +## announce_parse + +Module: `announce`. + +Inputs: + +``` +a0 = raw packet ptr +a1 = raw packet len +a2 = announce_rx_t* out +``` + +Outputs: + +``` +a0 = 0 on success, negative errno on failure +out = parsed fixed fields on success +``` + +Responsibilities: + +1. Reject null pointers and lengths shorter than the fixed announce length. +2. Require HEADER_1 announce flags `0x01`, context `0x00`, and a payload that + fits within `ANNOUNCE_RETICULUM_MDU`. +3. Extract destination hash, public key, name hash, random hash, signature, and + app-data view without heap allocation. +4. Never read beyond `raw_packet[0:raw_len]`. + +Verification: + +- QEMU tests against `tests/harness/oracle.announce_parse`. +- Negative malformed-field and short-buffer tests. +- Symbolic bounds proof over all lengths up to the Reticulum MDU. + +## announce_validate + +Module: `announce`. + +Inputs: + +``` +a0 = announce_rx_t* parsed +``` + +Outputs: + +``` +a0 = 0 on valid announce, negative errno on invalid announce +``` + +Responsibilities: + +1. Compute `identity_hash = SHA256(public_key)[0:16]`. +2. Compute expected destination hash as `SHA256(name_hash || identity_hash)[0:16]`. +3. Compare expected destination hash to packet destination hash. +4. Verify Ed25519 signature over + `destination_hash || public_key || name_hash || random_hash || app_data` + using `public_key[32:64]` as the Ed25519 public key. +5. Reject every mismatch without updating transport state. + +Verification: + +- Pyca/upstream oracle tests for valid announces. +- Tamper tests for every signed field and destination-hash-only mismatch. +- TLA+ trace coverage through `transport_process_announce`. + +## transport_path_init + +Module: `transport`. + +Inputs: + +``` +(none) +``` + +Outputs: + +``` +a0 = 0 +``` + +Responsibilities: + +1. Clear all path-table valid bits and reserved fields. +2. Leave no stale public key bytes observable through lookup. +3. Be idempotent. + +## transport_path_update + +Module: `transport`. + +Inputs: + +``` +a0 = announce_rx_t* valid announce +a1 = interface_id +a2 = hops +``` + +Outputs: + +``` +a0 = 0 on inserted/updated, negative errno on invalid input +``` + +Responsibilities: + +1. Update an existing destination hash if present. +2. Insert into the first invalid slot otherwise. +3. If full, evict the oldest entry by unsigned age from `last_seen_ms`. +4. Store destination hash, identity hash, public key, interface ID, hops, and + current timestamp. + +## transport_path_lookup + +Module: `transport`. + +Inputs: + +``` +a0 = destination_hash ptr (16 bytes) +a1 = transport_path_entry_t* out +``` + +Outputs: + +``` +a0 = 0 on found, negative errno on missing or invalid input +out = copied path entry on found +``` + +Responsibilities: + +1. Search only valid entries. +2. Copy exactly one fixed-size entry on hit. +3. Leave `out` unchanged on miss. + +## transport_process_announce + +Module: `transport`. + +Inputs: + +``` +a0 = raw packet ptr +a1 = raw packet len +a2 = interface_id +``` + +Outputs: + +``` +a0 = 0 accepted, positive duplicate/update status, negative invalid status +``` + +Responsibilities: + +1. Parse the inbound announce. +2. Validate destination hash and signature. +3. Update the path table when valid. +4. Return stable status codes so `_main` can log accepted, duplicate, and + rejected cases without inspecting private state. + +## Boot Integration + +The existing `_main` KISS frame path keeps the milestone-3 local command: + +``` +N || name_hash[10] || app_data +``` + +All other KISS frames still go through `packet_parse_header`. When the parsed +packet is a HEADER_1 announce, `_main` also calls +`transport_process_announce(kiss_buf, kiss_buf_len, TRANSPORT_INTERFACE_KISS)`. + +Required logs: + +| Case | Log sequence | +|------|--------------| +| Valid new path | `kiss.rx_frame`, `packet.parsed`, `transport.announce_valid`, `transport.path_updated` | +| Valid duplicate/update | `kiss.rx_frame`, `packet.parsed`, `transport.announce_valid`, `transport.path_updated` | +| Invalid announce | `kiss.rx_frame`, `packet.parsed`, `transport.announce_invalid` | +| Non-announce packet | existing `packet.parsed` or `packet.rejected` only | + +Logs must not include private key material. Public destination/identity hashes +may be exposed in tests only if the harness needs them for assertion; default +runtime logs should remain status-only. + +## Verifier Plan + +- `proofs/transport/transport_state.tla` models announce RX as + `Parse -> Validate -> UpdatePath | Reject` and covers duplicate/update and + full-table eviction. +- `announce_parse` needs a bounds proof because it handles attacker-controlled + lengths. +- `announce_validate` relies on the already verified SHA-256, destination hash, + and Ed25519 verify primitives, plus end-to-end oracle tests. +- `transport_path_*` functions need symbolic memory proofs for bounded table + search/update and unchanged-on-miss behavior. + +## Risks Specific To This Milestone + +| Risk | Mitigation | +|------|------------| +| Upstream Reticulum announce acceptance has edge cases not captured by milestone 3 TX validation | Differential tests use upstream `RNS.Identity.validate_announce()` and pyca for every accepted case. | +| Path-table eviction policy becomes incompatible with later forwarding | Keep replacement deterministic and documented; persistence and multi-interface metrics are deferred until after this RAM table is proven. | +| Signature verification cost makes RX sluggish on C6 | Start with correctness; measure hardware KISS RX latency and defer batching/queueing until the transport state machine exists. | +| Logs accidentally expose peer public keys or app data | Default logs are status-only; tests parse emitted KISS/packet bytes rather than adding verbose runtime logs. |