From ac0b35ca55e7e45dac0984c921ec6ff2b600ae77 Mon Sep 17 00:00:00 2001 From: Matt <47545907+SoundMatt@users.noreply.github.com> Date: Tue, 28 Jul 2026 21:31:27 -0700 Subject: [PATCH] =?UTF-8?q?feat:=20v2.18.0=20=E2=80=94=20Certification=20R?= =?UTF-8?q?efresh=20(=C2=A7Phase=2016=20milestone=2062)?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Retires the pre-replacement REQ-ZONE-*/REQ-CMD-*/REQ-STATUS-* requirement groups (20 entries) that milestone 61 explicitly left untouched, and regenerates HARA.md/.fusa-hara.json, TARA-ANALYSIS.md, CYBERSECURITY.md, and AUDIT_PACK.md against the full v2.x stream/endpoint/register-map requirement set, keeping existing OS-*/H-*/SG-*/A-*/T-* IDs stable while replacing every Zone/Command/Controller-era mechanism reference with the real v2.x module it now maps to. Adds a new H-011/SG-011 hazard/safety-goal pair for the E2E CRC mechanism, the roadmap's own stated most safety-relevant new surface. Replaces the three formal-verification TLA+ specs (AntiReplayGuard, HealthStateMachine, WatchdogProtocol), none of which matched any mechanism actually in this tree, with RxSequenceGuard/CrcSafeStateLatch/ WatchdogSafeState modelling rcp/e2e.hpp's and rcp/watchdog.hpp's actual primitives — each verified for real with TLC via a checked-in .cfg file, closing a pre-existing gap where FORMAL_VERIFICATION.md's documented invocation had no config to load. version.hpp/CMakeLists.txt bumped to 2.18.0. fmea.*/safety-case.*/tara.*/ sbom.json/audit-pack.zip/etc. are left for release.yml's existing tag-triggered regeneration rather than hand-edited here. Signed-off-by: Matt <47545907+SoundMatt@users.noreply.github.com> --- .fusa-hara.json | 90 ++++++++++++------ .fusa-reqs.json | 160 ------------------------------- .gitignore | 1 + AUDIT_PACK.md | 95 ++++++++++++------- CMakeLists.txt | 2 +- CYBERSECURITY.md | 129 +++++++++++++++++-------- FORMAL_VERIFICATION.md | 115 +++++++++++++++------- HARA.md | 190 ++++++++++++++++++++++++------------- ROADMAP.md | 108 +++++++++++++++++++++ SAFETY_PLAN.md | 6 +- TARA-ANALYSIS.md | 112 ++++++++++++---------- include/rcp/rcp.hpp | 42 ++++---- include/rcp/version.hpp | 2 +- tests/test_rcp.cpp | 36 ++----- tla/AntiReplayGuard.tla | 52 ---------- tla/CrcSafeStateLatch.cfg | 14 +++ tla/CrcSafeStateLatch.tla | 84 ++++++++++++++++ tla/HealthStateMachine.tla | 60 ------------ tla/RxSequenceGuard.cfg | 10 ++ tla/RxSequenceGuard.tla | 75 +++++++++++++++ tla/WatchdogProtocol.tla | 57 ----------- tla/WatchdogSafeState.cfg | 15 +++ tla/WatchdogSafeState.tla | 101 ++++++++++++++++++++ 23 files changed, 918 insertions(+), 638 deletions(-) delete mode 100644 tla/AntiReplayGuard.tla create mode 100644 tla/CrcSafeStateLatch.cfg create mode 100644 tla/CrcSafeStateLatch.tla delete mode 100644 tla/HealthStateMachine.tla create mode 100644 tla/RxSequenceGuard.cfg create mode 100644 tla/RxSequenceGuard.tla delete mode 100644 tla/WatchdogProtocol.tla create mode 100644 tla/WatchdogSafeState.cfg create mode 100644 tla/WatchdogSafeState.tla diff --git a/.fusa-hara.json b/.fusa-hara.json index 14a1597..3ae7560 100644 --- a/.fusa-hara.json +++ b/.fusa-hara.json @@ -2,37 +2,41 @@ "project": "cpp-RCP", "standard": "ISO 26262", "createdAt": "2026-06-16T00:00:00Z", - "updatedAt": "2026-06-16T00:00:00Z", + "updatedAt": "2026-07-28T00:00:00Z", "operationalSituations": [ { "id": "OS-001", - "description": "Normal vehicle operation \u2014 all zone controllers reachable" + "description": "Normal operation — the RC Client and every discovered RC Server are reachable" }, { "id": "OS-002", - "description": "Partial network fault \u2014 one or more zone controllers unreachable" + "description": "Partial network fault — one or more RC Servers unreachable or a request stream lost" }, { "id": "OS-003", - "description": "Safety-critical manoeuvre \u2014 emergency braking or collision avoidance active" + "description": "Safety-critical manoeuvre — a request is in flight to a safety-relevant endpoint (e.g. a GPIO/CAN endpoint driving a braking-adjacent actuator)" }, { "id": "OS-004", - "description": "HPC software fault \u2014 runaway process, crash, or OOM condition" + "description": "RC Client software fault — runaway process, crash, or OOM condition on the HPC" }, { "id": "OS-005", - "description": "Elevated network latency \u2014 congestion, EMI, or hardware degradation" + "description": "Elevated network latency — congestion, EMI, or hardware degradation on the AVB/TSN segment" }, { "id": "OS-006", - "description": "Adversarial access \u2014 attacker present on the zone Ethernet bus" + "description": "Adversarial access — attacker present on the Ethernet segment" + }, + { + "id": "OS-007", + "description": "RC Server power-state transition — cold/hot start or a StandBy/Sleep to Normal wake sequence in progress" } ], "hazards": [ { "id": "H-001", - "description": "Loss of command delivery to safety-critical zone (e.g. braking actuator)", + "description": "Loss of request delivery to a safety-critical endpoint (e.g. a braking-adjacent actuator)", "situations": [ "OS-001", "OS-002", @@ -50,7 +54,7 @@ }, { "id": "H-002", - "description": "Spurious command sent to wrong zone controller", + "description": "Request misaddressed to the wrong endpoint via a stale or corrupted stream_id/byte_bus_id pairing", "situations": [ "OS-001" ], @@ -66,7 +70,7 @@ }, { "id": "H-003", - "description": "Zone controller watchdog not kicked, leading to unintended reset", + "description": "Per-stream watchdog not kicked, leading to an unintended safe-state entry or endpoint reset", "situations": [ "OS-001", "OS-003" @@ -83,7 +87,7 @@ }, { "id": "H-004", - "description": "Replay of stale commands from a previous drive cycle", + "description": "Replay or out-of-order re-delivery of a stale request from a previous session", "situations": [ "OS-001", "OS-006" @@ -100,7 +104,7 @@ }, { "id": "H-005", - "description": "Zone controller falsely reported as alive when unresponsive", + "description": "RC Server falsely reported reachable/ready when actually unresponsive", "situations": [ "OS-002", "OS-005" @@ -117,7 +121,7 @@ }, { "id": "H-006", - "description": "Priority inversion \u2014 low-priority burst of commands starves a safety-critical CmdWatchdog", + "description": "Execution-priority inversion — a lower-priority request burst starves a safety-tagged or cancellation request", "situations": [ "OS-001", "OS-003", @@ -136,7 +140,7 @@ }, { "id": "H-007", - "description": "Rate limiter blocks watchdog kick during high command burst, causing spurious zone reset", + "description": "Rate limiter blocks a safety-relevant request during a high-traffic burst, causing a spurious watchdog trip", "situations": [ "OS-001", "OS-005" @@ -154,7 +158,7 @@ }, { "id": "H-008", - "description": "Unauthorized command injection via unsecured UDP transport on the zone Ethernet bus", + "description": "Unauthorized request injection or register-map modification via an unsecured transport, spoofed discovery response, or non-root EP0 write", "situations": [ "OS-006" ], @@ -170,10 +174,11 @@ }, { "id": "H-009", - "description": "Zone controller not properly woken from sleep, causing loss of actuation during safety manoeuvre", + "description": "RC Server not properly woken from StandBy/Sleep, causing loss of actuation during a safety manoeuvre", "situations": [ "OS-002", - "OS-003" + "OS-003", + "OS-007" ], "risk": { "severity": "S3", @@ -188,7 +193,7 @@ }, { "id": "H-010", - "description": "Fault injection state persists across vehicle power cycles, masking real faults in production", + "description": "Fault injection state persists across process/power cycles, masking real faults in production", "situations": [ "OS-001", "OS-004" @@ -202,47 +207,65 @@ "safetyGoals": [ "SG-009" ] + }, + { + "id": "H-011", + "description": "Undetected payload corruption bypasses the E2E CRC check, or a stream configured to latch on CRC failure fails to enter or hold safe state", + "situations": [ + "OS-001", + "OS-003", + "OS-005" + ], + "risk": { + "severity": "S3", + "exposure": "E3", + "controllability": "C2", + "asil": "ASIL-B" + }, + "safetyGoals": [ + "SG-011" + ] } ], "safetyGoals": [ { "id": "SG-001", - "description": "Commands to safety-critical zones shall be delivered within the watchdog period or a fault shall be signalled.", + "description": "Requests to safety-critical endpoints shall be delivered within the configured watchdog period or a fault shall be signalled.", "asil": "ASIL-B" }, { "id": "SG-002", - "description": "Commands shall only be processed by the zone they are addressed to; misrouted commands shall be rejected.", + "description": "Requests shall only be dispatched to the endpoint they are addressed to (stream_id + byte_bus_id); misaddressed requests shall be rejected.", "asil": "ASIL-B" }, { "id": "SG-003", - "description": "The watchdog kick command (CmdWatchdog) shall always be deliverable at the configured priority.", + "description": "A per-stream watchdog kick shall be recorded for every accepted inbound request, regardless of request kind or safety tag.", "asil": "ASIL-B" }, { "id": "SG-004", - "description": "Replayed or duplicated commands from prior sessions shall be detected and rejected.", + "description": "A request stream configured with rx_enforce_seq shall reject any sequence number that is not strictly greater than the last accepted one.", "asil": "ASIL-B" }, { - "id": "SG-007", - "description": "A zone controller that stops publishing Status shall be detected as dead within the configured deadline.", + "id": "SG-005", + "description": "Cancellation and triggered requests shall never be delayed by a standard or compound request queued earlier on the same stream.", "asil": "ASIL-B" }, { - "id": "SG-005", - "description": "Priority::Critical commands shall never be delayed by Priority::Normal or Priority::High commands queued earlier.", + "id": "SG-006", + "description": "Transport authentication (mTLS on the UDP/IP variant, or link-layer authentication on native Ethernet) and per-endpoint access policy shall be enforced on every external RC Server connection.", "asil": "ASIL-B" }, { - "id": "SG-006", - "description": "Transport authentication (mTLS or equivalent) shall be enforced on all external zone controller connections.", + "id": "SG-007", + "description": "An RC Server that stops responding shall be detected as unreachable within the configured liveness deadline.", "asil": "ASIL-B" }, { "id": "SG-008", - "description": "A zone controller shall only be declared operational after a successful Wake command response.", + "description": "An RC Server shall only be treated as operational after its lifecycle state machine reports RCP_CONFIGURED following a successful wake sequence.", "asil": "ASIL-B" }, { @@ -252,8 +275,13 @@ }, { "id": "SG-010", - "description": "Zone controller health state transitions shall be deterministically derivable from observable send() outcomes alone.", + "description": "A stream's watchdog/safe-state status shall be deterministically derivable from its own kick/overflow/latch history alone.", + "asil": "ASIL-B" + }, + { + "id": "SG-011", + "description": "A request whose computed E2E CRC does not match its received trailer shall be rejected, and a stream configured with rx_enforce_e2e shall latch safe state on the first such failure until explicitly reset.", "asil": "ASIL-B" } ] -} \ No newline at end of file +} diff --git a/.fusa-reqs.json b/.fusa-reqs.json index ded0e8f..44c56f4 100644 --- a/.fusa-reqs.json +++ b/.fusa-reqs.json @@ -1,69 +1,5 @@ { "requirements": [ - { - "id": "REQ-ZONE-001", - "title": "Zone::to_string returns unique human-readable name", - "text": "rcp::to_string(Zone) shall return a unique, non-empty, human-readable string for each defined Zone constant. Two distinct Zone constants shall never return the same string.", - "standard": "iso26262", - "level": "ASIL-A", - "asil": "ASIL-A" - }, - { - "id": "REQ-ZONE-002", - "title": "Zone::Unknown has value 0", - "text": "Zone::Unknown shall have the numeric value 0, making it the zero value of the Zone type and a safe default for uninitialized variables.", - "standard": "iso26262", - "level": "ASIL-A", - "asil": "ASIL-A" - }, - { - "id": "REQ-ZONE-003", - "title": "Zone::FrontLeft has value 1", - "text": "Zone::FrontLeft shall have the numeric value 1.", - "standard": "iso26262", - "level": "ASIL-A", - "asil": "ASIL-A" - }, - { - "id": "REQ-ZONE-004", - "title": "Zone::FrontRight has value 2", - "text": "Zone::FrontRight shall have the numeric value 2.", - "standard": "iso26262", - "level": "ASIL-A", - "asil": "ASIL-A" - }, - { - "id": "REQ-ZONE-005", - "title": "Zone::RearLeft has value 3", - "text": "Zone::RearLeft shall have the numeric value 3.", - "standard": "iso26262", - "level": "ASIL-A", - "asil": "ASIL-A" - }, - { - "id": "REQ-ZONE-006", - "title": "Zone::RearRight has value 4", - "text": "Zone::RearRight shall have the numeric value 4.", - "standard": "iso26262", - "level": "ASIL-A", - "asil": "ASIL-A" - }, - { - "id": "REQ-ZONE-007", - "title": "Zone::Central has value 5", - "text": "Zone::Central shall have the numeric value 5.", - "standard": "iso26262", - "level": "ASIL-A", - "asil": "ASIL-A" - }, - { - "id": "REQ-ZONE-008", - "title": "All named Zone constants are distinct", - "text": "Zone::FrontLeft, Zone::FrontRight, Zone::RearLeft, Zone::RearRight, and Zone::Central shall each have a different numeric value from every other named zone constant.", - "standard": "iso26262", - "level": "ASIL-B", - "asil": "ASIL-B" - }, { "id": "REQ-PRI-001", "title": "Priority::Normal has value 0", @@ -88,102 +24,6 @@ "level": "ASIL-B", "asil": "ASIL-B" }, - { - "id": "REQ-CMD-001", - "title": "CommandType::Noop has value 0", - "text": "CommandType::Noop shall have the numeric value 0. An uninitialized Command.type shall be interpreted as a safe no-op.", - "standard": "iso26262", - "level": "ASIL-A", - "asil": "ASIL-A" - }, - { - "id": "REQ-CMD-002", - "title": "CommandType::Set has value 1", - "text": "CommandType::Set shall have the numeric value 1.", - "standard": "iso26262", - "level": "ASIL-A", - "asil": "ASIL-A" - }, - { - "id": "REQ-CMD-003", - "title": "CommandType::Get has value 2", - "text": "CommandType::Get shall have the numeric value 2.", - "standard": "iso26262", - "level": "ASIL-A", - "asil": "ASIL-A" - }, - { - "id": "REQ-CMD-004", - "title": "CommandType::Reset has value 3", - "text": "CommandType::Reset shall have the numeric value 3.", - "standard": "iso26262", - "level": "ASIL-A", - "asil": "ASIL-A" - }, - { - "id": "REQ-CMD-005", - "title": "CommandType::Watchdog has value 4", - "text": "CommandType::Watchdog shall have the numeric value 4. The watchdog kick command shall be a stable, named constant.", - "standard": "iso26262", - "level": "ASIL-B", - "asil": "ASIL-B" - }, - { - "id": "REQ-CMD-006", - "title": "All CommandType constants are distinct", - "text": "CommandType::Noop, Set, Get, Reset, and Watchdog shall each have a different numeric value.", - "standard": "iso26262", - "level": "ASIL-B", - "asil": "ASIL-B" - }, - { - "id": "REQ-STATUS-001", - "title": "ResponseStatus::to_string returns unique human-readable name", - "text": "rcp::to_string(ResponseStatus) shall return a unique, non-empty, human-readable string for each defined ResponseStatus constant.", - "standard": "iso26262", - "level": "ASIL-A", - "asil": "ASIL-A" - }, - { - "id": "REQ-STATUS-002", - "title": "ResponseStatus::OK has value 0", - "text": "ResponseStatus::OK shall have the numeric value 0. An uninitialized Response.status shall be interpreted as success.", - "standard": "iso26262", - "level": "ASIL-A", - "asil": "ASIL-A" - }, - { - "id": "REQ-STATUS-003", - "title": "ResponseStatus::Error has value 1", - "text": "ResponseStatus::Error shall have the numeric value 1.", - "standard": "iso26262", - "level": "ASIL-A", - "asil": "ASIL-A" - }, - { - "id": "REQ-STATUS-004", - "title": "ResponseStatus::Timeout has value 2", - "text": "ResponseStatus::Timeout shall have the numeric value 2.", - "standard": "iso26262", - "level": "ASIL-A", - "asil": "ASIL-A" - }, - { - "id": "REQ-STATUS-005", - "title": "ResponseStatus::Busy has value 3", - "text": "ResponseStatus::Busy shall have the numeric value 3.", - "standard": "iso26262", - "level": "ASIL-A", - "asil": "ASIL-A" - }, - { - "id": "REQ-STATUS-006", - "title": "All ResponseStatus constants are distinct", - "text": "ResponseStatus::OK, Error, Timeout, Busy, and Unknown shall each have a different numeric value.", - "standard": "iso26262", - "level": "ASIL-B", - "asil": "ASIL-B" - }, { "id": "REQ-ERR-001", "title": "ErrClosed is truthy", diff --git a/.gitignore b/.gitignore index 246f244..234695a 100644 --- a/.gitignore +++ b/.gitignore @@ -15,3 +15,4 @@ _deps/ *.swp *.swo .DS_Store +tla/states/ diff --git a/AUDIT_PACK.md b/AUDIT_PACK.md index 3f15cba..e5b68e1 100644 --- a/AUDIT_PACK.md +++ b/AUDIT_PACK.md @@ -1,9 +1,15 @@ -# Audit Pack — cpp-RCP Certification Evidence (Milestone 43) +# Audit Pack — cpp-RCP Certification Evidence (Milestone 62) -**Document version**: 1.0.0 -**Date**: 2026-06-16 +**Document version**: 2.0.0 +**Date**: 2026-07-28 **Standards**: ISO 26262 (ASIL-B), IEC 61508 (SIL-2), ISO 21434, IEC 62443 SL-2 +This revision (ROADMAP.md milestone 62, "Certification Refresh", v2.18.0) +supersedes the pre-replacement audit pack authored at milestone 43. All +figures below (requirement count, coverage module list, CI gate +thresholds) are re-derived against the full v2.x requirement set built up +across Phase 13-16 (v2.0.0-v2.17.0). + --- ## 1. Document Index @@ -14,7 +20,7 @@ | TARA (Threat Analysis & Risk Assessment) | `TARA-ANALYSIS.md` | Complete | | Cybersecurity Architecture | `CYBERSECURITY.md` | Complete | | Formal Verification | `FORMAL_VERIFICATION.md` | Complete | -| Safety Requirements | `.fusa-reqs.json` | 198 requirements | +| Safety Requirements | `.fusa-reqs.json` | 417 requirements across 55 groups | | Safety Case | Generated via `cpfusa safety-case` | CI gate | | Release Badge | Generated via `cpfusa badge` | CI gate | @@ -22,38 +28,46 @@ ## 2. ASIL-D Gap Analysis (ISO 26262 §7) -cpp-RCP targets **ASIL-B** for the zone communication subsystem. The following -table records deliberate derogations from ASIL-D: +cpp-RCP targets **ASIL-B** for the RC Client/RC Server communication +subsystem. The following table records deliberate derogations from +ASIL-D: | ASIL-D Requirement | Derogation Rationale | ASIL-B Coverage | |--------------------|----------------------|-----------------| -| Redundant communication paths | Not required at ECU boundary for ASIL-B | Single channel with E2E protection | -| Formal proofs of absence of deadlock | TLA+ liveness proofs deferred to ASIL-C/D upgrade path | TLC exhaustive model check on bounded state space | +| Redundant communication paths | Not required at ECU boundary for ASIL-B | Single channel with E2E CRC + sequence + watchdog protection | +| Formal proofs of absence of deadlock | TLA+ liveness proofs deferred to ASIL-C/D upgrade path | TLC exhaustive model check on bounded state space (`tla/`) | | MISRA C++:2023 compliance | MISRA advisory rules selectively suppressed with justification | clang-tidy clean on safety-critical rules | -| 100% MC/DC structural coverage | 80% branch coverage enforced in CI | 80% branch + path coverage reported by cpfusa coverage | +| 100% MC/DC structural coverage | 80% branch coverage enforced in CI | 80% branch + path coverage reported by `cpfusa coverage` | -ASIL decomposition: the zonal network is decomposed as ASIL-B(D) = -ASIL-A + ASIL-B per ISO 26262-9 §5 (independent channel decomposition). +ASIL decomposition: the RC Client/RC Server link is decomposed as +ASIL-B(D) = ASIL-A + ASIL-B per ISO 26262-9 §5 (independent channel +decomposition) — see `HARA.md`'s per-hazard decomposition rationale. --- ## 3. Structural Coverage Report -Coverage is measured by the `cpfusa coverage` tool on the CI test suite. +Coverage is measured by the `cpfusa coverage` tool on the CI test suite, +against `coverage.info` collected from `ctest --test-dir build-cov`. | Module | Line | Branch | MC/DC | |--------|------|--------|-------| -| rcp.hpp (core) | 98% | 94% | 78% | -| e2e.hpp | 96% | 91% | 82% | -| watchdog.hpp | 95% | 89% | 76% | -| deadline.hpp | 94% | 87% | 74% | -| authz.hpp | 97% | 93% | 80% | -| firmware.hpp | 91% | 85% | 71% | -| **Overall** | **95%** | **89%** | **77%** | - -Required threshold: 80% branch coverage. All modules meet threshold. -MC/DC coverage target of 80% is partially met; shortfall is tracked as -open item for ASIL-C upgrade path. +| `e2e.hpp` | See `coverage-report.json` (regenerated at release) | +| `watchdog.hpp` | See `coverage-report.json` (regenerated at release) | +| `lifecycle.hpp` | See `coverage-report.json` (regenerated at release) | +| `regmap.hpp` | See `coverage-report.json` (regenerated at release) | +| `avtp.hpp` / `acf.hpp` | See `coverage-report.json` (regenerated at release) | +| `authz.hpp` | See `coverage-report.json` (regenerated at release) | +| **Overall** | See `coverage-report.json`'s `summary` block | + +`coverage-report.json` is regenerated on every tagged release by +`.github/workflows/release.yml` (`cpfusa coverage --profile coverage.info +--dal DAL-B`) — it is not hand-maintained here to avoid this document +drifting from the actual per-release measurement, the drift this revision +itself was written to correct. + +Required threshold: 80% branch coverage. MC/DC coverage target of 80% is +tracked as an open item for an ASIL-C upgrade path. --- @@ -64,7 +78,7 @@ If cpp-RCP is used in an airborne system under DO-178C DAL-C: - Source code traceability to LLR: via `// fusa:req` annotations - Tool qualification: cpfusa is a Tool Qualification Level (TQL-5) analysis tool - Decision coverage: MC/DC required at DAL-C — see shortfall above -- Structural coverage artifacts: generated by `cpfusa coverage --xml` +- Structural coverage artifacts: generated by `cpfusa coverage` --- @@ -74,33 +88,44 @@ All of the following gates must pass for a tagged release: | Gate | Tool | Threshold | |------|------|-----------| -| Static analysis | `cpfusa check --strict` | Zero errors | +| Static analysis | `cpfusa check` | Zero errors | | Lint | `cpfusa lint` | Zero violations | | MISRA/safety analysis | `cpfusa analyze` | Zero safety violations | -| Cyber review | `cpfusa cyber --strict` | Zero cyber violations | -| Requirement coverage | `cpfusa trace --req-coverage 80` | ≥ 80% covered | -| Formal verification | `cpfusa verify` | Verified | +| Cyber review | `cpfusa cyber` | Zero cyber violations | +| Requirement coverage | `cpfusa trace --req-coverage 100` | 100% covered (RELAY §20.1) | +| Formal verification | TLC on `tla/*.tla` | No error found | | ASIL qualification | `cpfusa qualify` | Qualified | | Vulnerability scan | `cpfusa vuln` | No critical/high CVEs | | Safety case | `cpfusa safety-case` | Complete | -| ISO 26262 report | `cpfusa iso26262` | Compliant | -| IEC 61508 report | `cpfusa iec61508` | Compliant | -| DO-178C report | `cpfusa do178` | Notes/advisories only | +| ISO 26262 report | `cpfusa iso26262` | Gap report generated (advisory) | +| IEC 61508 report | `cpfusa iec61508` | Gap report generated (advisory) | +| DO-178C report | `cpfusa do178` | Gap report generated (advisory) | | Coverage | `cpfusa coverage` | ≥ 80% branch | | SCI (Software Change Impact) | `cpfusa sci` | No unmitigated impacts | | Audit pack | `cpfusa audit-pack` | Generated | | Release badge | `cpfusa badge` | Green | +The requirement-coverage threshold is 100% (`cpfusa trace --req-coverage +100`, enforced in `ci.yml`'s `cpfusa-trace` job per RELAY §20.1), not the +80% this document previously recorded — the gate was tightened at +milestone 60 and this document had not been updated to match until now. +The ISO 26262/IEC 61508/DO-178C gap reports are generated by +`release.yml` with `|| true` — they record gaps against those standards' +own certification targets without blocking a release, since the seven +application-layer protocol bridges (`mqttbr.hpp`/`ddsbr.hpp`/etc.) remain +unimplemented stubs by design (see `CYBERSECURITY.md` §1 and +`TARA-ANALYSIS.md` §6). + --- ## 6. Traceability Matrix Requirements → implementation tracing is maintained in `.fusa-reqs.json` -(198 requirements across 24 groups). Traceability is validated by -`cpfusa trace --req-coverage 80` in CI. +(417 requirements across 55 groups as of this milestone). Traceability is +validated by `cpfusa trace --req-coverage 100` in CI. -Implementation → test tracing: each `// fusa:req` annotation in a header maps -to one or more test cases in `tests/`. +Implementation → test tracing: each `// fusa:req` annotation in a header +maps to one or more `// fusa:test` annotations and test cases in `tests/`. --- diff --git a/CMakeLists.txt b/CMakeLists.txt index 373826e..ba17f58 100644 --- a/CMakeLists.txt +++ b/CMakeLists.txt @@ -1,7 +1,7 @@ cmake_minimum_required(VERSION 3.21) project(cpp-rcp - VERSION 2.17.0 + VERSION 2.18.0 DESCRIPTION "Remote Control Protocol for automotive zonal architecture (C++)" HOMEPAGE_URL "https://github.com/SoundMatt/cpp-RCP" LANGUAGES CXX diff --git a/CYBERSECURITY.md b/CYBERSECURITY.md index 0e7f11b..6869cd3 100644 --- a/CYBERSECURITY.md +++ b/CYBERSECURITY.md @@ -1,50 +1,98 @@ -# Cybersecurity Architecture — cpp-RCP (Milestone 42) +# Cybersecurity Architecture — cpp-RCP (Milestone 62) ## IEC 62443 SL-2 / ISO 21434 -**Document version**: 1.0.0 -**Date**: 2026-06-16 +**Document version**: 2.0.0 +**Date**: 2026-07-28 + +This revision (ROADMAP.md milestone 62, "Certification Refresh", v2.18.0) +supersedes the pre-replacement, Zone/Command-shaped architecture authored +at milestone 42. Every layer below is re-derived against the current +stream/endpoint/register-map architecture built up across Phase 13-16 +(v2.0.0-v2.17.0); the pre-replacement `authz::AuthController`/ +`ratelimit::Controller`/`firmware::FirmwareSession` surfaces this document +used to cite are gone or superseded, per ROADMAP.md's Satellite Package +Disposition table. --- ## 1. Security Layers -### Layer 1 — Transport Security (TLS 1.3) +### Layer 1 — Transport Security (TLS 1.2+, UDP/IP variant) + +`include/rcp/tls.hpp` provides `SecureClient`/`SecureServer`, the +integration surface for mutual TLS on the UDP/IP transport variant +(`rcp/udp.hpp`, v2.13.0). The actual TLS implementation (OpenSSL / wolfSSL) +is plugged in at the application layer; neither class reports itself +usable, nor sends/accepts a request, without a real backend attached +(REQ-TLS-005, REQ-TLS-006). -`include/rcp/tls.hpp` provides the integration surface for mTLS. The actual -TLS implementation (OpenSSL / wolfSSL) is plugged in at the application layer. +- Mutual certificate authentication, verified by CA (`Config::verify_peer` + defaults to `true`) +- TLS 1.2+ enforced; weak cipher suites disabled (REQ-TLS-007, REQ-TLS-008) +- For native Ethernet deployments, MACsec (802.1AE) at layer 2 is the + specification's own preferred link-security mechanism; this package does + not implement it and flags it as the longer-term preferred approach + (`tls.hpp`'s own header note) -- Mutual certificate authentication (both HPC and zone controller present certs) -- Certificate CN is extracted and passed to the `authz::AuthController` -- Cipher suites: TLS_AES_128_GCM_SHA256, TLS_AES_256_GCM_SHA384 (mandatory) +REQ-TLS-001..REQ-TLS-010 -### Layer 2 — Command Authorization (`authz::AuthController`) +### Layer 2 — Endpoint Authorization (`authz::AccessPolicy`) -Each send() is checked against an `AccessPolicy` table. The policy is loaded -from a signed manifest at boot. ErrForbidden is returned without forwarding -the command. +Each request is checked against an `AccessPolicy` table keyed by +`(identity, stream, endpoint, request kind)`. An identity with zero policy +entries, or one not covered by any `PolicyEntry`, is denied by default +(REQ-AUTH-003, REQ-AUTH-007). `check()` returns `ErrForbidden` without +forwarding the request. REQ-AUTH-001..REQ-AUTH-008 -### Layer 3 — E2E Anti-Replay (`e2e::ReplayGuard`) +### Layer 3 — E2E Integrity & Anti-Replay (`e2e.hpp`) + +Three independent, per-stream primitives cover this layer: + +- `e2e::verify_crc` — a 32-bit CRC (polynomial `0xF4ACFB13`) computed over + the stream_id, AVTP timestamp, ACF header, and payload; a mismatch is + reported as `E2eErrc::crc_error` (REQ-E2E-001, REQ-E2E-004). +- `e2e::RxStreamGuard` — implements the per-stream `rx_enforce_e2e` + drop-vs-latch rule: with the flag clear, a CRC failure is reported for + that request alone; with it set, the first failure latches the whole + stream until `reset_latch()` is called explicitly (REQ-E2E-006). +- `e2e::RxSequenceGuard` — enforces a strictly-increasing sequence number + per stream when `rx_enforce_seq` is set, independent of the CRC and + watchdog checks (REQ-E2E-007). + +REQ-E2E-001..REQ-E2E-014 + +### Layer 4 — Rate Limiting (`ratelimit::Manager`) -A 32-entry sliding-window bitmap detects replayed sequence numbers. Sequence -numbers more than 32 behind the high-water mark are unconditionally rejected. +A token-bucket admission-control layer, keyed per `(stream, endpoint)` +domain, prevents DoS via request flooding. Safety-tagged requests may be +configured exempt from the bucket to preserve safety-function availability +(REQ-RL-004); when not exempted, they are throttled like any other request +(REQ-RL-005). -REQ-E2E-004, REQ-E2E-005, REQ-E2E-006 +REQ-RL-001..REQ-RL-008 -### Layer 4 — Rate Limiting (`ratelimit::Controller`) +### Layer 5 — Discovery Integrity (`discovery::DiscoveryClaim`) -Token-bucket rate limiter prevents DoS via command flooding. Priority::Critical -commands are exempt to preserve safety function availability. +Discovery requests are NTSCF-only, addressed at `byte_bus_id` 0 and +register-map address 0 (REQ-DISC-001, REQ-DISC-002). The first discovery +request claims the discovery stream; only the active claim holder may +issue a configuration request, and the claim lapses after +`Discovery_TimeOut` (REQ-DISC-003, REQ-DISC-004, REQ-DISC-006), bounding +how long a single client can monopolize configuration access. -REQ-RL-003, REQ-RL-004 +REQ-DISC-001..REQ-DISC-009 -### Layer 5 — Firmware Integrity (`firmware::FirmwareSession`) +### Layer 6 — Register-Map Write Protection (`regmap::Ep0`) -SHA-256 hash of the transferred image is verified by the zone controller before -activation. Rollback requires authentication. +`Ep0`'s whole-register-map read is unrestricted, but a whole-map write +requires the root client — the client that currently holds the exclusive +root-client claim (REQ-REGMAP-003, REQ-REGMAP-004). Per-endpoint write +restrictions and independent config-block locks apply to non-root clients +on top of that gate (REQ-REGMAP-005, REQ-REGMAP-006). -REQ-FW-005..REQ-FW-007 +REQ-REGMAP-001..REQ-REGMAP-015 --- @@ -52,13 +100,13 @@ REQ-FW-005..REQ-FW-007 | Requirement | Status | Notes | |------------|--------|-------| -| FR1 Identification & Authentication | Implemented | mTLS + authz | -| FR2 Use Control | Implemented | AccessPolicy per zone/command-type | -| FR3 System Integrity | Implemented | E2E CRC-16 + anti-replay | -| FR4 Data Confidentiality | Partial | TLS stub; HSM key storage external | -| FR5 Restricted Data Flow | Implemented | Zone isolation in routing | -| FR6 Timely Response | Implemented | Deadline monitor + watchdog | -| FR7 Resource Availability | Implemented | Rate limiter; Critical exempt | +| FR1 Identification & Authentication | Implemented | mTLS (UDP/IP variant) + `authz::AccessPolicy` | +| FR2 Use Control | Implemented | `AccessPolicy` per (identity, stream, endpoint, request kind) | +| FR3 System Integrity | Implemented | E2E CRC32 + `rx_enforce_e2e` latch + `rx_enforce_seq` monotonic check | +| FR4 Data Confidentiality | Partial | TLS integration surface present; concrete backend and HSM key storage are external/application-supplied | +| FR5 Restricted Data Flow | Implemented | Endpoint isolation via `byte_bus_id`-scoped dispatch and per-endpoint `AccessPolicy` entries | +| FR6 Timely Response | Implemented | `deadline::Monitor` liveness tracking + `watchdog::Manager` per-stream watchdog | +| FR7 Resource Availability | Implemented | `ratelimit::Manager` token bucket; safety-tagged requests configurably exempt | --- @@ -66,16 +114,17 @@ REQ-FW-005..REQ-FW-007 The following attack vectors are in scope for penetration testing: -1. Replay attack on the RCP wire protocol (REQ-E2E-004) -2. Unauthorized command injection (REQ-AUTH-001) -3. Watchdog silence attack (REQ-WDG-003) -4. Firmware rollback to known-vulnerable version (REQ-FW-007) -5. TLS downgrade (covered by min-version enforcement) +1. Replay or out-of-order re-injection on a stream with `rx_enforce_seq` set (REQ-E2E-007) +2. Unauthorized request injection without a valid TLS session or policy entry (REQ-AUTH-001, REQ-TLS-001) +3. Watchdog-silence DoS against a safety-tagged stream (REQ-WDG-003) +4. Discovery spoofing / discovery-claim hijack attempt (REQ-DISC-003, REQ-DISC-006) +5. Non-root register-map write attempt (REQ-REGMAP-003) +6. TLS downgrade (covered by min-version enforcement, REQ-TLS-007) --- ## 4. Incident Response -Security vulnerabilities in cpp-RCP should be reported via the secure disclosure -process defined in [`SECURITY.md`](SECURITY.md) (not yet authored; tracked as -open action item). +Security vulnerabilities in cpp-RCP should be reported via the secure +disclosure process defined in [`SECURITY.md`](SECURITY.md); operational +incident handling is defined in [`INCIDENT-RESPONSE.md`](INCIDENT-RESPONSE.md). diff --git a/FORMAL_VERIFICATION.md b/FORMAL_VERIFICATION.md index dd6f462..1b03e57 100644 --- a/FORMAL_VERIFICATION.md +++ b/FORMAL_VERIFICATION.md @@ -1,60 +1,111 @@ -# Formal Verification — cpp-RCP (Milestone 41) +# Formal Verification — cpp-RCP (Milestone 62) ## Overview -TLA+ specifications are located in [`tla/`](tla/). They cover three safety- -critical subsystems identified in the HARA (see [`HARA.md`](HARA.md)): +TLA+ specifications are located in [`tla/`](tla/). They cover the three +independent primitives `rcp/e2e.hpp` and `rcp/watchdog.hpp` provide for the +safety-critical subsystems identified in the HARA (see [`HARA.md`](HARA.md)), +re-derived at the Certification Refresh milestone (v2.18.0) against the +actual v2.6.0/v2.10.0 mechanism rather than the pre-replacement, +Zone/Command-shaped model the previous revision of this document described. | Spec | Module | Safety Property | |------|--------|----------------| -| `HealthStateMachine.tla` | Watchdog health state machine | SP1: No Healthy→Faulted direct transition | -| `AntiReplayGuard.tla` | E2E sequence-number replay guard | SP1: No double-acceptance; SP2: Old sequences rejected | -| `WatchdogProtocol.tla` | Watchdog heartbeat protocol | SP1: No Healthy→Faulted direct transition | +| `RxSequenceGuard.tla` | `e2e::RxSequenceGuard` monotonic sequence check | SP1: high-water mark never decreases; SP2: no stale acceptance | +| `CrcSafeStateLatch.tla` | `e2e::RxStreamGuard` E2E CRC drop-vs-latch rule | SP1: no latch without `rx_enforce_e2e`; SP2: latch only cleared by an explicit reset | +| `WatchdogSafeState.tla` | `e2e::RxWatchdog`/`watchdog::StreamWatchdog` timeout + safe-state latch | SP1: no latch without `rx_wd_safestate_enable`; SP2: latch only cleared by an explicit reset | + +`tla/AntiReplayGuard.tla`, `tla/HealthStateMachine.tla`, and +`tla/WatchdogProtocol.tla` are retired as of this milestone: the first +modelled the pre-replacement 32-entry sliding-window bitmap guard removed +at v2.6.0, and the latter two both modelled the same three-state +Healthy/Degraded/Faulted watchdog machine, driven by a client-side +periodic `CommandType::Watchdog` kick, discarded outright at v2.10.0. The +current watchdog mechanism has no Degraded intermediate state and is kicked +by any accepted inbound request, not a dedicated command. ## Verification Method -Specs are verified with the TLC model checker (TLA+ Toolbox ≥ 1.7): +Specs are verified with the TLC model checker (`tla2tools.jar`, TLA+ +Toolbox ≥ 1.7). Each spec's like-named `.cfg` file in `tla/` supplies the +constants, `INIT`/`NEXT`, and the invariants/properties TLC checks — TLC +loads it automatically when invoked without `-config`: ```bash -# Install TLA+ Toolbox or tlc2 JAR -java -jar tla2tools.jar -workers 4 tla/HealthStateMachine.tla -java -jar tla2tools.jar -workers 4 tla/AntiReplayGuard.tla -java -jar tla2tools.jar -workers 4 tla/WatchdogProtocol.tla +java -jar tla2tools.jar -workers 4 tla/RxSequenceGuard.tla +java -jar tla2tools.jar -workers 4 tla/CrcSafeStateLatch.tla +java -jar tla2tools.jar -workers 4 tla/WatchdogSafeState.tla ``` Expected output: `Model checking completed. No error has been found.` +`CrcSafeStateLatch.cfg` and `WatchdogSafeState.cfg` each check their +respective spec's affirmative latch behavior under +`EnforceLatch`/`SafestateEnabled = TRUE`; the complementary +`NoLatchWithoutEnforce`/`NoLatchWithoutEnable` property is non-vacuous only +under the `FALSE` configuration — flip the relevant `CONSTANT` line and +re-run to check it directly (see each `.cfg` file's own comment). + ## Safety Properties Verified -### SP1 — No Direct Health Transition (HealthStateMachine, WatchdogProtocol) +### SP1/SP2 — Sequence Monotonicity (`RxSequenceGuard`) + +A stream's high-water mark (`last_seq`) never decreases, and a sequence +number no greater than the current high-water mark is never subsequently +accepted. Unlike the pre-replacement sliding-window bitmap this spec +supersedes, there is no window to exhaust — acceptance is a single +comparison against the high-water mark. + +**ASIL tracing**: H-004 (request replay/out-of-order delivery), SG-004, +REQ-E2E-007. + +### SP1/SP2 — CRC Drop-vs-Latch Rule (`CrcSafeStateLatch`) -A zone controller in `Healthy` state may never transition directly to `Faulted`. -It must pass through `Degraded`. This prevents a single missed heartbeat from -triggering an emergency shutdown. +A stream configured with `rx_enforce_e2e = FALSE` never latches on a CRC +failure — only that request is rejected. A stream configured with +`rx_enforce_e2e = TRUE` latches on its first CRC failure, and — once +latched — only an explicit `reset_latch()` step (identifiable in the model +by every other tracked state component staying unchanged) ever clears it. -**ASIL tracing**: H-002 (watchdog miss), SG-002 (watchdog recovery), REQ-WDG-003. +**ASIL tracing**: H-011 (E2E CRC integrity — the most safety-relevant new +surface introduced across this roadmap), SG-011, REQ-E2E-004, REQ-E2E-006. -### SP2 — Anti-Replay Double-Acceptance (AntiReplayGuard) +### SP1/SP2 — Watchdog Timeout + Safe-State Latch (`WatchdogSafeState`) -A sequence number that has been accepted by the E2E guard may never be accepted -again within the replay window. Sequence numbers older than `ReplayWindowSize` -ticks are unconditionally rejected. +A stream configured with `rx_wd_safestate_enable = FALSE` never latches on +a watchdog timeout — only the overflow itself is reported. A stream +configured with `rx_wd_safestate_enable = TRUE` latches on the first +observed timeout, and only an explicit `clear_safe_state()` step ever +clears it. `kick()` alone never causes a timeout, since overflow detection +requires an elapsed-time step (`Tick`) past `rx_wd_timeout_interval`. -**ASIL tracing**: H-008 (unauthorized injection), SG-006 (mTLS + E2E), REQ-E2E-004. +**ASIL tracing**: H-003 (watchdog not kicked), H-009 (RC Server not woken), +SG-003, SG-008, SG-010, REQ-WDG-001, REQ-WDG-003, REQ-WDG-004. ## Assumptions and Abstractions -- The TLA+ models use natural numbers as simulated clocks; overflow is not - modelled (production uses 32-bit wrap-around with correct comparison). -- The `AntiReplayGuard` model does not model counter rollover; the C++ - implementation handles rollover via unsigned arithmetic. -- The `WatchdogProtocol` model assumes synchronous ticks; the C++ - implementation uses a background `std::thread` with `std::condition_variable`. +- The TLA+ models use natural numbers as simulated clocks; unsigned 32-bit + wrap-around (the C++ implementation's actual sequence-number and + watchdog-timer representation) is not modelled directly, since TLC model + checking already bounds the state space independently via each spec's + `.cfg` constants/constraints. +- `RxSequenceGuard.tla` and `CrcSafeStateLatch.tla`/`WatchdogSafeState.tla` + are modelled independently, matching `rcp/e2e.hpp`'s own separation of + `RxSequenceGuard`, `RxStreamGuard`, and `RxWatchdog` into three + independently-configurable primitives — a stream can enable any + combination of `rx_enforce_seq`, `rx_enforce_e2e`, and + `rx_wd_safestate_enable` (or none) per the register map. +- `WatchdogSafeState.tla` assumes a synchronous `Tick` action for the + elapsed-time check; the C++ implementation instead compares + caller-supplied wall-clock milliseconds on each `check()`/`poll()` call, + with no timer thread of its own (`RxWatchdog`/`StreamWatchdog` are + primitives, not a scheduler — see `rcp/watchdog.hpp`'s own header + comment). ## Mapping to C++ Implementation -| TLA+ Variable | C++ Location | -|---------------|--------------| -| `state[z]` | `watchdog::Keeper::health_[z]` | -| `accepted` | `e2e::ReplayGuard::bitmap_` + `high_water_` | -| `last_kick[z]` | `watchdog::Keeper::last_kick_[z]` | +| TLA+ Spec | TLA+ Variable | C++ Location | +|-----------|---------------|--------------| +| `RxSequenceGuard` | `last_seq`, `has_last` | `e2e::RxSequenceGuard::last_seq_`, `has_last_` | +| `CrcSafeStateLatch` | `latched` | `e2e::RxStreamGuard::latched_` | +| `WatchdogSafeState` | `kicked`, `last_kick`, `latched` | `e2e::RxWatchdog::kicked_`, `last_kick_ms_`, `in_safe_state_` | diff --git a/HARA.md b/HARA.md index ac998a4..c617235 100644 --- a/HARA.md +++ b/HARA.md @@ -1,22 +1,30 @@ # Hazard Analysis and Risk Assessment (HARA) -**Standard:** ISO 26262:2018 Part 3 -**System:** cpp-RCP — Remote Control Protocol for automotive zonal architecture -**Target ASIL:** ASIL-B (derived) +**Standard:** ISO 26262:2018 Part 3 +**System:** cpp-RCP — C++ implementation of the OPEN Alliance TC18 Remote Control Protocol +**Target ASIL:** ASIL-B (derived) **Source:** `.fusa-hara.json` (machine-readable authoritative source) +This revision (ROADMAP.md milestone 62, "Certification Refresh", v2.18.0) +supersedes the pre-replacement, Zone/Command/Controller-shaped analysis +authored at milestone 41. Hazard/safety-goal IDs are carried forward +unchanged where the underlying concern still applies to the current +stream/endpoint/register-map architecture; new hazards introduced by +Phase 13-16 work are appended as H-011/SG-011. + --- ## Operational Situations | ID | Description | |----|-------------| -| OS-001 | Normal vehicle operation — all zone controllers reachable | -| OS-002 | Partial network fault — one or more zone controllers unreachable | -| OS-003 | Safety-critical manoeuvre — emergency braking or collision avoidance active | -| OS-004 | HPC software fault — runaway process, crash, or OOM condition | -| OS-005 | Elevated network latency — congestion, EMI, or hardware degradation | -| OS-006 | Adversarial access — attacker present on the zone Ethernet bus | +| OS-001 | Normal operation — the RC Client and every discovered RC Server are reachable | +| OS-002 | Partial network fault — one or more RC Servers unreachable or a request stream lost | +| OS-003 | Safety-critical manoeuvre — a request is in flight to a safety-relevant endpoint (e.g. a GPIO/CAN endpoint driving a braking-adjacent actuator) | +| OS-004 | RC Client software fault — runaway process, crash, or OOM condition on the HPC | +| OS-005 | Elevated network latency — congestion, EMI, or hardware degradation on the AVB/TSN segment | +| OS-006 | Adversarial access — attacker present on the Ethernet segment | +| OS-007 | RC Server power-state transition — cold/hot start or a StandBy/Sleep to Normal wake sequence in progress | --- @@ -24,16 +32,17 @@ | ID | Hazard | Severity | Exposure | Controllability | ASIL | Safety Goals | |----|--------|----------|----------|-----------------|------|--------------| -| H-001 | Loss of command delivery to safety-critical zone (e.g. braking actuator) | S3 | E4 | C2 | ASIL-B | SG-001 | -| H-002 | Spurious command sent to wrong zone controller | S2 | E3 | C2 | ASIL-B | SG-002 | -| H-003 | Zone controller watchdog not kicked, leading to unintended reset | S2 | E4 | C2 | ASIL-B | SG-003 | -| H-004 | Replay of stale commands from a previous drive cycle | S2 | E3 | C2 | ASIL-B | SG-004 | -| H-005 | Zone controller falsely reported as alive when unresponsive | S2 | E3 | C2 | ASIL-B | SG-007 | -| H-006 | Priority inversion — low-priority burst starves safety-critical CmdWatchdog | S2 | E4 | C2 | ASIL-B | SG-001, SG-005 | -| H-007 | Rate limiter blocks watchdog kick during high command burst | S2 | E3 | C2 | ASIL-B | SG-003, SG-005 | -| H-008 | Unauthorized command injection via unsecured transport | S3 | E2 | C2 | ASIL-B | SG-006 | -| H-009 | Power state management failure — zone not properly woken from sleep | S3 | E3 | C2 | ASIL-B | SG-001, SG-008 | -| H-010 | Fault injection state persists across vehicle power cycles | S2 | E2 | C3 | ASIL-A | SG-009 | +| H-001 | Loss of request delivery to a safety-critical endpoint (e.g. a braking-adjacent actuator) | S3 | E4 | C2 | ASIL-B | SG-001 | +| H-002 | Request misaddressed to the wrong endpoint via a stale or corrupted stream_id/byte_bus_id pairing | S2 | E3 | C2 | ASIL-B | SG-002 | +| H-003 | Per-stream watchdog not kicked, leading to an unintended safe-state entry or endpoint reset | S2 | E4 | C2 | ASIL-B | SG-003 | +| H-004 | Replay or out-of-order re-delivery of a stale request from a previous session | S2 | E3 | C2 | ASIL-B | SG-004 | +| H-005 | RC Server falsely reported reachable/ready when actually unresponsive | S2 | E3 | C2 | ASIL-B | SG-007 | +| H-006 | Execution-priority inversion — a lower-priority request burst starves a safety-tagged or cancellation request | S2 | E4 | C2 | ASIL-B | SG-001, SG-005 | +| H-007 | Rate limiter blocks a safety-relevant request during a high-traffic burst, causing a spurious watchdog trip | S2 | E3 | C2 | ASIL-B | SG-003, SG-005 | +| H-008 | Unauthorized request injection or register-map modification via an unsecured transport, spoofed discovery response, or non-root EP0 write | S3 | E2 | C2 | ASIL-B | SG-006 | +| H-009 | RC Server not properly woken from StandBy/Sleep, causing loss of actuation during a safety manoeuvre | S3 | E3 | C2 | ASIL-B | SG-001, SG-008 | +| H-010 | Fault injection state persists across process/power cycles, masking real faults in production | S2 | E2 | C3 | ASIL-A | SG-009 | +| H-011 | Undetected payload corruption bypasses the E2E CRC check, or a stream configured to latch on CRC failure fails to enter or hold safe state | S3 | E3 | C2 | ASIL-B | SG-011 | --- @@ -41,61 +50,113 @@ | ID | Safety Goal | ASIL | Addressed By | |----|-------------|------|--------------| -| SG-001 | Commands to safety-critical zones shall be delivered within the watchdog period or a fault shall be signalled. | ASIL-B | `watchdog::Keeper`, `deadline::Monitor` | -| SG-002 | Commands shall only be processed by the zone they are addressed to; misrouted commands shall be rejected. | ASIL-B | `Controller::send()` ErrZoneMismatch check | -| SG-003 | The watchdog kick command (CmdWatchdog) shall always be deliverable at the configured priority. | ASIL-B | `ratelimit::Controller` exempt_critical, `prioqueue::Controller` Critical bypass | -| SG-004 | Replayed or duplicated commands from prior sessions shall be detected and rejected. | ASIL-B | `e2e::ReplayGuard` bitmap sliding window | -| SG-005 | Priority::Critical commands shall never be delayed by Priority::Normal or Priority::High commands queued earlier. | ASIL-B | `prioqueue::Controller` priority ordering | -| SG-006 | Transport authentication (mTLS or equivalent) shall be enforced on all external zone controller connections. | ASIL-B | `tls::Controller` (interface), mTLS Config | -| SG-007 | A zone controller that stops publishing Status shall be detected as dead within the configured deadline. | ASIL-B | `deadline::Monitor` | -| SG-008 | A zone controller shall only be declared operational after a successful Wake command response. | ASIL-B | `powerstate::Manager` Active transition gate | +| SG-001 | Requests to safety-critical endpoints shall be delivered within the configured watchdog period or a fault shall be signalled. | ASIL-B | `watchdog::Manager`/`StreamWatchdog`, `deadline::Monitor` | +| SG-002 | Requests shall only be dispatched to the endpoint they are addressed to (stream_id + byte_bus_id); misaddressed requests shall be rejected. | ASIL-B | `acf::AcfMessageInfo` byte_bus_id decode, RC Server dispatch (e.g. `mock::Server::dispatch`) | +| SG-003 | A per-stream watchdog kick shall be recorded for every accepted inbound request, regardless of request kind or safety tag. | ASIL-B | `watchdog::StreamWatchdog::kick_from_request`, `e2e::RxWatchdog` | +| SG-004 | A request stream configured with rx_enforce_seq shall reject any sequence number that is not strictly greater than the last accepted one. | ASIL-B | `e2e::RxSequenceGuard::check` | +| SG-005 | Cancellation and triggered requests shall never be delayed by a standard or compound request queued earlier on the same stream. | ASIL-B | `request::SequencerTable`/`RequestLedger` execution-priority ordering | +| SG-006 | Transport authentication (mTLS on the UDP/IP variant, or link-layer authentication on native Ethernet) and per-endpoint access policy shall be enforced on every external RC Server connection. | ASIL-B | `tls::SecureClient`/`SecureServer`, `authz::AccessPolicy`, `discovery::DiscoveryClaim` | +| SG-007 | An RC Server that stops responding shall be detected as unreachable within the configured liveness deadline. | ASIL-B | `deadline::Monitor`/`LivenessTracker` | +| SG-008 | An RC Server shall only be treated as operational after its lifecycle state machine reports RCP_CONFIGURED following a successful wake sequence. | ASIL-B | `lifecycle::ServerLifecycle`, `powerstate::PowerManager` | | SG-009 | Fault injection rules shall not persist beyond the lifetime of the injecting process. | ASIL-A | `faultinject::Controller` in-process state only | -| SG-010 | Zone controller health state transitions shall be deterministically derivable from observable send() outcomes alone. | ASIL-B | `watchdog::Keeper` deterministic state machine | +| SG-010 | A stream's watchdog/safe-state status shall be deterministically derivable from its own kick/overflow/latch history alone. | ASIL-B | `e2e::RxWatchdog`, `watchdog::StreamWatchdog` deterministic state | +| SG-011 | A request whose computed E2E CRC does not match its received trailer shall be rejected, and a stream configured with rx_enforce_e2e shall latch safe state on the first such failure until explicitly reset. | ASIL-B | `e2e::verify_crc`, `e2e::RxStreamGuard` | --- ## ASIL Decomposition Rationale -### H-001 (ASIL-B): Loss of command delivery +### H-001 (ASIL-B): Loss of request delivery -The HPC sends commands to zone controllers over an automotive Ethernet network. Network faults, ECU resets, or HPC process crashes can prevent command delivery. The required ASIL is B because: +The RC Client sends requests to RC Servers over an automotive Ethernet +network. Network faults, ECU resets, or HPC process crashes can prevent +request delivery. The required ASIL is B because: -- **S3**: Loss of braking actuation during emergency deceleration could be life-threatening. -- **E4**: Zone controllers are continuously addressable during normal driving. -- **C2**: The driver may not be able to react in time if actuation is silently lost. +- **S3**: loss of actuation on a braking-adjacent endpoint during emergency + deceleration could be life-threatening. +- **E4**: RC Servers are continuously addressable during normal driving. +- **C2**: the driver may not be able to react in time if actuation is + silently lost. **Decomposition**: ASIL-B is achieved via: -1. `watchdog::Keeper` (ASIL-B): detects non-responsive zones within `fault_after × interval`. -2. `deadline::Monitor` (ASIL-B): detects zones that stop sending Status telemetry. -3. No decomposition into lower ASIL-A + ASIL-A elements is claimed; the above mechanisms together satisfy ASIL-B. - -### H-002 (ASIL-B): Zone misrouting - -Each `Controller::send()` checks `cmd.zone == this->zone()` before processing. This check is a single-point protection; ASIL-B is met because the check is simple and directly observable (returns ErrZoneMismatch). +1. `watchdog::Manager`/`StreamWatchdog` (ASIL-B): detects a stream whose + `rx_wd_timeout_interval` has elapsed with no accepted request. +2. `deadline::Monitor` (ASIL-B): detects an RC Server whose liveness + signal (response/ack-queue heartbeat or EP0 lifecycle-state-changed + trigger) has gone silent past its configured deadline. +3. No decomposition into lower ASIL-A + ASIL-A elements is claimed; the + above mechanisms together satisfy ASIL-B. + +### H-002 (ASIL-B): Endpoint misaddressing + +Every request carries an explicit `(stream_id, byte_bus_id)` pair in its +AVTPDU/ACF framing (`rcp/avtp.hpp`, `rcp/acf.hpp`). An RC Server's dispatch +layer is responsible for routing a decoded request only to the endpoint +whose `byte_bus_id` it names — `mock::Server::dispatch` is this codebase's +own reference implementation of that check. This is a single-point +protection; ASIL-B is met because the check is simple, directly observable +in the decoded `acf::AcfMessageInfo`, and independent of request payload +content. ### H-003 (ASIL-B): Watchdog failure -SG-003 is addressed by the combination of: -1. `prioqueue::Controller` — Critical-priority CmdWatchdog bypasses queue backpressure. -2. `ratelimit::Controller` — `exempt_critical=true` bypasses the token bucket for Critical commands. - -Both mechanisms are independently verifiable and together meet ASIL-B by preventing starvation. - -### H-004 (ASIL-B): Command replay - -`e2e::ReplayGuard` implements a 32-entry bitmap sliding window. Frames are rejected if: -- The sequence number matches a previously-accepted number within the window, or -- The sequence number is more than `ReplayWindowSize` (32) behind the current high-water mark. - -The CRC-16/CCITT-FALSE also protects against accidentally-valid replays. - -### H-006 (ASIL-B): Priority inversion - -`prioqueue::Controller` uses `std::priority_queue` with Priority::Critical as the highest key. FIFO ordering within the same priority level preserves fairness. The dispatch thread always dispatches the highest-priority entry in the queue. - -### H-008 (ASIL-B): Unauthorized injection - -The `tls::Controller` interface requires mutual TLS. The stub returns `errc::function_not_supported` to ensure integrators cannot accidentally connect without authentication. Full OpenSSL backend is scoped for v0.7.0 acceptance testing. +SG-003 is addressed by `watchdog::StreamWatchdog::kick_from_request`, +called once per accepted inbound request regardless of request kind or +safety tag, wrapping `e2e::RxWatchdog`'s timeout/latch primitive +(`rx_wd_enable`/`rx_wd_timeout_interval`). A stream configured with +`rx_wd_safestate_enable` additionally latches safe state and purges queued +non-safety requests on overflow (`e2e::apply_watchdog_overflow`), leaving +safety-tagged (0x8x) requests untouched so they can still drive the +endpoint through its own safe-state sequence. + +### H-004 (ASIL-B): Request replay / out-of-order delivery + +`e2e::RxSequenceGuard::check` enforces a strictly-increasing sequence +number per stream when `rx_enforce_seq` is set: the first observed +sequence number bootstraps the comparison, and any subsequent sequence +number that is not strictly greater than the last accepted one is +rejected outright. Unlike the pre-replacement 32-entry sliding-window +bitmap this supersedes, there is no window to exhaust — the check is a +single comparison against the high-water mark, independently gated per +stream and orthogonal to the E2E CRC check in H-011. + +### H-006 (ASIL-B): Execution-priority inversion + +`request::SequencerTable`/`RequestLedger` dispatch in the specification's +fixed execution-priority ordering — cancellation, then triggered, timed, +compound, compound-wait, chained, and finally standard requests — enforced +server-side per stream rather than as a client-side send-order wrapper. +A burst of standard requests queued ahead of a cancellation or triggered +request can never delay it once dispatch reaches that stream. + +### H-008 (ASIL-B): Unauthorized injection / register-map modification + +Three independent mechanisms cover this hazard's distinct attack +surfaces: `tls::SecureClient`/`SecureServer` require mutual TLS on the +UDP/IP transport variant (native Ethernet deployments should prefer +MACsec (802.1AE) at layer 2, flagged as the longer-term mechanism this +package does not itself implement); `authz::AccessPolicy` gates requests +by `(identity, server, endpoint, request kind)`; and +`regmap::Ep0::check_write_access` restricts a whole-register-map write to +the root client, rejecting a non-root client's attempt to reconfigure an +endpoint's stream/lifecycle behavior. + +### H-011 (ASIL-B): E2E CRC integrity + +This is the hazard the roadmap identifies as the most safety-relevant new +surface introduced across this whole roadmap. `e2e::verify_crc` recomputes +the 32-bit CRC (polynomial `0xF4ACFB13`) over the stream_id, AVTP +timestamp (or its documented zero-fill under NTSCF), ACF header, and +payload, and compares it against the received trailer; a mismatch is +reported as `E2eErrc::crc_error` for that request. `e2e::RxStreamGuard` +implements the per-stream opt-in latch: with `rx_enforce_e2e` clear, a +CRC failure is reported for that request alone; with it set, the first +failure additionally latches the whole stream so every subsequent request +also reports `crc_error` until `reset_latch()` is called explicitly (e.g. +on stream reconfiguration). ASIL-B is met because both the per-request +rejection and the whole-stream latch are deterministic functions of the +received bytes and the stream's own configuration — no timing-dependent +or best-effort behavior is involved. --- @@ -103,6 +164,7 @@ The `tls::Controller` interface requires mutual TLS. The stub returns `errc::fun | Risk | Likelihood | Mitigation | Status | |------|-----------|------------|--------| -| ReplayGuard window exhausted by rapid legitimate traffic | Low | 32-entry window handles 32 in-flight commands per zone; watchdog period is at least 10 ms | Accepted | -| TLS stub returns `function_not_supported` on non-Linux CI | Low | CI explicitly tests the shmem/mock transport; TLS tested on Linux only | Accepted | -| mDNS StaticDiscoverer not sufficient for dynamic topology | Medium | Full mDNS backend deferred to v0.6.0 platform integration; static config covers initial SiL testing | Accepted | +| A stream with `rx_enforce_seq` clear accepts replayed/out-of-order requests by design | Low | Per-endpoint configuration choice; safety-relevant streams are expected to set `rx_enforce_seq` | Accepted | +| `tls::SecureClient`/`SecureServer` require an application-supplied OpenSSL/wolfSSL backend; the interface itself performs no cryptography | Low | Native Ethernet deployments should prefer MACsec (802.1AE) at layer 2 instead, per `tls.hpp`'s own header note | Accepted | +| `mdns.hpp`'s discovery-adjacent name service is rescoped to the UDP/IP transport variant only | Low | TC18's own wire-level discovery (`discovery.hpp`, v2.2.0) covers native Ethernet deployments without a name-service layer | Accepted | +| `rcp/config.hpp` and `rcp/faultinject.hpp` still build against the pre-replacement `rcp.hpp` Zone/Command/Controller model | Medium | Tracked as a separate, still-open rebind item (per milestone 60's closeout); neither is on a safety-relevant request-dispatch path introduced by Phase 13-16 | Accepted | diff --git a/ROADMAP.md b/ROADMAP.md index fb4daaf..ab6882c 100644 --- a/ROADMAP.md +++ b/ROADMAP.md @@ -1459,6 +1459,114 @@ milestone did not touch. CRC / safe-state mechanism (v2.6.0) is the most safety-relevant new surface in this whole roadmap +**Done (v2.18.0):** `.fusa-reqs.json` is pruned of the 20 requirement +entries backing the pre-replacement `REQ-ZONE-*`/`REQ-CMD-*`/ +`REQ-STATUS-*` groups (8/6/6), matching the file's own `rcp/rcp.hpp` +header-comment note added at this milestone explaining why the underlying +C++ types remain (per REPLACE, not a delete — `rcp/config.hpp` is still +their one remaining dependent, per milestone 60's closeout) while their +requirement coverage does not: carrying certified coverage for a type this +codebase has already recorded as having no TC18 analog would misrepresent +it as safety-relevant surface going forward. The matching `// fusa:req`/ +`// fusa:test` annotation lines and stale Catch2 tags are removed from +`rcp/rcp.hpp` and `tests/test_rcp.cpp`; the `REQ-PRI-*`/`REQ-ERR-*`/ +`REQ-CMDSTRUCT-*`/`REQ-RESP-*`/`REQ-STAT-*` groups this milestone's own +scope text does not name for retirement keep their existing coverage +unchanged. Every `REQ-*` prefix this milestone's scope text names as +needing its own group (`REQ-WIRE` through `REQ-RELAY`) was already present +per each phase's own closeout — this was verification, not bulk authoring, +confirming no gap-filling was needed. `.fusa-reqs.json` now carries 417 +requirements across 55 groups (down from 437 across 58 groups pre-prune). + +`HARA.md`/`.fusa-hara.json`, `TARA-ANALYSIS.md`, and `CYBERSECURITY.md` +are rewritten against the current stream/endpoint/register-map +architecture, keeping their existing OS-\*/H-\*/SG-\* and A-\*/T-\* ID +schemes stable (so `SAFETY_PLAN.md`'s existing safety-goal references stay +valid) while replacing every Zone/Command/Controller-era mechanism +reference with the real v2.x module it now maps to (`e2e::RxSequenceGuard`/ +`RxStreamGuard`/`RxWatchdog`, `watchdog::Manager`, `lifecycle:: +ServerLifecycle`, `regmap::Ep0`, `authz::AccessPolicy`, `discovery:: +DiscoveryClaim`, `tls::SecureClient`/`SecureServer`), and removing threats/ +mitigations tied to packages this roadmap has since deprecated +(`firmware.hpp`'s SHA-256 image verification, `prioqueue.hpp`'s +`Priority::Critical` bypass). A new hazard/safety-goal pair (H-011/SG-011) +and TARA threat (T-05, re-scoped) cover the E2E CRC mechanism specifically, +per this milestone's own call-out that it is the most safety-relevant new +surface in the roadmap; H-001/SG-001's ASIL-B decomposition rationale is +rewritten around the real two-mechanism combination +(`watchdog::Manager`/`StreamWatchdog` + `deadline::Monitor`) instead of the +removed `watchdog::Keeper`. `SAFETY_PLAN.md`'s two mechanism-table rows +that named now-retired ids (`REQ-CMD-005`, `REQ-PQ-001`) are repointed to +their real v2.x replacements (`REQ-WDG-002`, `REQ-SEQ-002`) as a minimal, +targeted fix — the rest of that file's zone-era language is unchanged, +being out of this milestone's own named scope. + +The formal-verification TLA+ specs are replaced, not just re-described: +`tla/AntiReplayGuard.tla` modelled the pre-replacement 32-entry +sliding-window bitmap guard removed at v2.6.0, and `tla/ +HealthStateMachine.tla`/`tla/WatchdogProtocol.tla` both modelled the same +three-state Healthy/Degraded/Faulted watchdog machine driven by a +client-side periodic `CommandType::Watchdog` kick, discarded outright at +v2.10.0 — none of the three matched any mechanism actually in this tree. +`tla/RxSequenceGuard.tla`, `tla/CrcSafeStateLatch.tla` (new: the E2E CRC +drop-vs-latch rule had no formal spec before this milestone), and `tla/ +WatchdogSafeState.tla` model `rcp/e2e.hpp`'s/`rcp/watchdog.hpp`'s actual +three independently-configurable primitives instead, each with a +like-named `.cfg` TLC now loads automatically (the pre-replacement specs +had none, so `FORMAL_VERIFICATION.md`'s own documented `java -jar +tla2tools.jar tla/*.tla` invocation would have failed with a missing-config +error had anyone actually run it — a pre-existing gap this milestone +closes). All three new specs and their safety/liveness properties are +verified with TLC 2.19 (`tla2tools.jar`), not just asserted: +`RxSequenceGuard`'s `Monotonic`/`NoStaleAcceptance`, `CrcSafeStateLatch`'s +`LatchIsSticky`/`NoLatchWithoutEnforce`, and `WatchdogSafeState`'s +`LatchIsSticky` all report "Model checking completed. No error has been +found." `FORMAL_VERIFICATION.md` is rewritten to match, including the +ASIL tracing table pointing at the new H-011/SG-011 pair. + +`AUDIT_PACK.md` is rewritten: the requirement count (198 across 24 groups +→ 417 across 55), the `cpfusa trace` coverage gate threshold (80% → 100%, +matching the gate milestone 60 actually tightened without this document +being updated to match until now), and the structural-coverage module list +(no more `rcp.hpp (core)`/`firmware.hpp` fixed numbers — the module table +now points at `coverage-report.json`, regenerated by `release.yml` on +every tag, rather than hand-copying numbers that go stale between +releases) are all corrected. Its own document version is bumped 1.0.0 → +2.0.0, alongside `TARA-ANALYSIS.md`'s and `CYBERSECURITY.md`'s — these are +each document's own independent revision counter, distinct from cpp-RCP's +own semver, and this is each document's first full-content rewrite since +its original milestone-42/43 authoring. + +`fmea.csv`/`fmea.json`, `safety-case.*`, `tara.json`/`tara.md`, `sbom.json`, +`provenance.json`, `artifact-manifest.json`, the ISO 26262/IEC 61508/ +DO-178C gap reports, `sas.*`, `sci.json`, `audit-pack.zip`, +`fusa-badge.svg`, `report.json`/`report.html`, and `qualify-report.json` +are deliberately left untouched by this PR: per `.github/workflows/ +release.yml`, every one of them is mechanically regenerated by `cpfusa` +against the current `.fusa-reqs.json`/`.fusa-hara.json`/source-tree state +on the next tag push, so hand-editing them here would just be overwritten +— committing a hand-edited copy now would only create merge noise against +what `release.yml`'s `github-actions[bot]` commit produces once v2.18.0 is +tagged, the same regeneration step every prior milestone's tag already +triggered (see e.g. `e7a8178`, the v2.17.0 regeneration commit). + +`version.hpp`/`CMakeLists.txt` are bumped to 2.18.0. Full local build +(clang, C++17) and `ctest` (53/53 tests, unchanged — no test file added, +removed, or renamed this milestone) pass; `cpfusa check`/`lint`/`cyber` +all pass with 0 errors (`lint`'s reported errors only appear when run +against a local `build/` tree that pulls in FetchContent'd Catch2 source +under `build/_deps`, which CI's `cpfusa-lint` job never has present, since +it runs `cpfusa lint` without a prior CMake configure/build step); `cpfusa +trace --req-coverage 100` reports `Total: 417 Annotated: 417 (100.0%) +Tested: 417 (100.0%)`, 0 dangling ids; RELAY `conform --strict` against +the built `cpp-rcp` CLI still passes, since this milestone touches no +wire-format or CLI-surface code. `README.md` is left unmodified: it +already predates milestones 44-61 (still documenting `rcp/firmware.hpp` +and other since-deleted packages) and bringing it in line with the current +architecture is a substantial, separately-scoped task this milestone's own +text does not name. Milestone #63 (TC18 RCP General Availability, v3.0.0) +is next and, per its own scope, is the final milestone in this roadmap. + ### 63. TC18 RCP — General Availability (v3.0.0) - First release where cpp-RCP's `RCP` conforms to the OPEN Alliance TC18 diff --git a/SAFETY_PLAN.md b/SAFETY_PLAN.md index 70ad9d0..b61d5a0 100644 --- a/SAFETY_PLAN.md +++ b/SAFETY_PLAN.md @@ -30,10 +30,10 @@ cpp-RCP is the C++ implementation of the Remote Control Protocol for automotive | Payload copy-on-send | REQ-CTRL-026 | Payload is deep-copied before handler invocation | | Payload copy-on-publish | REQ-CTRL-027 | Published payload is deep-copied before delivery to subscribers | | Context / deadline propagation | REQ-CTRL-004 | Expired context terminates Send without invoking the handler | -| Watchdog kick | REQ-CMD-005, REQ-WDG-007 | CmdWatchdog is a named constant schedulable at PriorityHigh | -| Replay guard | REQ-E2E-005 | ReplayGuard detects replayed sequence numbers within a sliding window | +| Watchdog kick | REQ-WDG-002 | Any accepted inbound request resets ("kicks") its stream's watchdog | +| Sequence guard | REQ-E2E-007 | RxSequenceGuard rejects a non-strictly-increasing sequence number when rx_enforce_seq is set | | Deadline monitor | REQ-DL-002 | Monitor detects a zone going silent within Config.Deadline | -| Priority scheduling | REQ-PQ-001 | PriorityCritical dispatched before High and Normal | +| Execution-priority ordering | REQ-SEQ-002 | Cancellation and triggered requests dispatch ahead of standard/compound requests queued earlier on the same stream | ## Verification approach diff --git a/TARA-ANALYSIS.md b/TARA-ANALYSIS.md index 4f86ffa..f000b1a 100644 --- a/TARA-ANALYSIS.md +++ b/TARA-ANALYSIS.md @@ -1,17 +1,22 @@ -# TARA — Threat Analysis and Risk Assessment (Milestone 42) +# TARA — Threat Analysis and Risk Assessment (Milestone 62) ## ISO 21434 / IEC 62443 SL-2 -**Document version**: 1.0.0 +**Document version**: 2.0.0 **ASIL level**: ASIL-B (ISO 26262) / SIL-2 (IEC 61508) -**Date**: 2026-06-16 +**Date**: 2026-07-28 --- ## 1. Scope -This TARA covers the cpp-RCP in-vehicle communication library. It identifies -cybersecurity threats to zone controller communications in a zonal HPC -architecture and assigns attack feasibility / impact ratings. +This TARA covers the cpp-RCP in-vehicle communication library as of the +Certification Refresh (v2.18.0). It identifies cybersecurity threats to +RC Client / RC Server communication under the OPEN Alliance TC18 Remote +Control Protocol Specification v0.5.1_RC's stream/endpoint/register-map +model and assigns attack feasibility / impact ratings. This revision +supersedes the pre-replacement, Zone/Command-shaped analysis authored at +milestone 42 — every asset, threat, and mitigation below is re-derived +against the current architecture rather than carried forward unchanged. --- @@ -19,13 +24,15 @@ architecture and assigns attack feasibility / impact ratings. | Asset ID | Asset | Security Property | |----------|-------|-------------------| -| A-01 | Zone command channel | Integrity, Authenticity | -| A-02 | Watchdog heartbeat | Availability, Integrity | -| A-03 | Firmware images in transit | Integrity, Authenticity | -| A-04 | E2E sequence counter | Integrity | -| A-05 | TLS session credentials | Confidentiality | -| A-06 | Zone health state | Integrity | -| A-07 | Access control policy | Integrity, Availability | +| A-01 | Request/response channel (addressed by stream_id + byte_bus_id) | Integrity, Authenticity | +| A-02 | Per-stream watchdog state (`e2e::RxWatchdog`, `watchdog::Manager`) | Availability, Integrity | +| A-03 | E2E sequence counter (`e2e::RxSequenceGuard`) | Integrity | +| A-04 | E2E CRC trailer / request-response payload integrity (`e2e::verify_crc`) | Integrity | +| A-05 | TLS session credentials (UDP/IP transport variant) | Confidentiality | +| A-06 | RC Server lifecycle/liveness state (`lifecycle::ServerLifecycle`, `deadline::Monitor`) | Integrity | +| A-07 | Access control policy (`authz::AccessPolicy`) | Integrity, Availability | +| A-08 | Register map / EP0 configuration (`regmap::Ep0`) | Integrity, Availability | +| A-09 | Discovery stream claim (`discovery::DiscoveryClaim`) | Availability, Integrity | --- @@ -33,16 +40,17 @@ architecture and assigns attack feasibility / impact ratings. | Threat ID | Asset | Threat | STRIDE | Attack Vector | |-----------|-------|--------|--------|---------------| -| T-01 | A-01 | Command injection (replay) | Spoofing | In-vehicle network | -| T-02 | A-01 | Command forgery (no auth) | Spoofing | Compromised HPC | -| T-03 | A-02 | Watchdog flood (DoS) | DoS | Local | -| T-04 | A-02 | Watchdog silence (block kick) | DoS | Kernel / driver | -| T-05 | A-03 | Corrupt firmware image | Tampering | Network | -| T-06 | A-03 | Rollback to vulnerable firmware | Repudiation | Local | -| T-07 | A-04 | Sequence counter overflow injection | Spoofing | In-vehicle | +| T-01 | A-01, A-03 | Request replay or out-of-order re-injection | Spoofing | In-vehicle network | +| T-02 | A-01, A-07 | Request forgery without authentication | Spoofing | Compromised HPC | +| T-03 | A-02 | Request flood degrading watchdog-adjacent stream throughput | DoS | Local | +| T-04 | A-02 | Watchdog silence — attacker blocks a stream's inbound requests to force a spurious safe-state latch | DoS | Kernel / driver | +| T-05 | A-04 | Payload tampering that bypasses the E2E CRC check | Tampering | Network | +| T-06 | A-04 | Unauthorized `reset_latch()` clearing a legitimately-latched safe state | Tampering | Compromised process | +| T-07 | A-03 | Sequence-counter overflow/wrap injection | Spoofing | In-vehicle | | T-08 | A-05 | TLS credential theft | Information Disclosure | Physical | -| T-09 | A-06 | Health state spoofing | Tampering | Compromised process | -| T-10 | A-07 | Policy bypass via identity forgery | Elevation of Privilege | Network | +| T-09 | A-09 | Discovery spoofing — a rogue device answers a discovery request as if it were the intended RC Server | Spoofing | In-vehicle network | +| T-10 | A-08 | Register-map write by a non-root client | Elevation of Privilege | Network | +| T-11 | A-07 | Policy bypass via identity forgery | Elevation of Privilege | Network | --- @@ -52,19 +60,21 @@ Ratings: Feasibility (1-5) × Impact (1-5) = Risk Score | Threat | Feasibility | Impact | Risk | Mitigation | |--------|-------------|--------|------|-----------| -| T-01 | 3 | 4 | 12 | E2E replay guard (`e2e::ReplayGuard`) | -| T-02 | 2 | 5 | 10 | mTLS + `authz::AuthController` | -| T-03 | 4 | 2 | 8 | Rate limiter (`ratelimit::Controller`) | -| T-04 | 2 | 5 | 10 | Watchdog health degradation state machine | -| T-05 | 2 | 5 | 10 | SHA-256 verify in `firmware::FirmwareSession` | -| T-06 | 2 | 4 | 8 | Anti-rollback counter in zone controller FW | -| T-07 | 1 | 3 | 3 | 32-bit counter with unsigned wrap-around; window rejects | -| T-08 | 1 | 5 | 5 | Hardware security module for key storage | -| T-09 | 1 | 4 | 4 | Health state stored in private memory; CRC protected | -| T-10 | 2 | 5 | 10 | Certificate CN verified via TLS chain | - -Residual risks above threshold (score ≥ 10): T-01, T-02, T-04, T-05, T-10. -All are covered by implemented mitigations. Residual risk is accepted at ASIL-B. +| T-01 | 3 | 4 | 12 | Strictly-increasing sequence check (`e2e::RxSequenceGuard::check`) | +| T-02 | 2 | 5 | 10 | mTLS (`tls::SecureClient`/`SecureServer`) + `authz::AccessPolicy` | +| T-03 | 4 | 2 | 8 | Token-bucket rate limiter (`ratelimit::Manager`) | +| T-04 | 2 | 5 | 10 | Per-stream `watchdog::StreamWatchdog` + `deadline::Monitor` liveness cross-check | +| T-05 | 2 | 5 | 10 | 32-bit E2E CRC verification (`e2e::verify_crc`, polynomial `0xF4ACFB13`) | +| T-06 | 1 | 4 | 4 | `reset_latch()` is an explicit, application-gated call, not reachable from wire input | +| T-07 | 1 | 3 | 3 | Unsigned 32-bit sequence comparison; first-seen bootstraps rather than wraps silently | +| T-08 | 1 | 5 | 5 | Hardware security module for key storage (external) | +| T-09 | 2 | 4 | 8 | Discovery-stream claim (`discovery::DiscoveryClaim`) scoped to a single active claimant | +| T-10 | 1 | 5 | 5 | `regmap::Ep0::check_write_access` restricts whole-map writes to the root client | +| T-11 | 2 | 5 | 10 | Certificate identity verified against `authz::AccessPolicy`'s `PolicyEntry` table | + +Residual risks above threshold (score ≥ 10): T-01, T-02, T-04, T-05, T-11. +All are covered by implemented mitigations. Residual risk is accepted at +ASIL-B. --- @@ -72,24 +82,28 @@ All are covered by implemented mitigations. Residual risk is accepted at ASIL-B | Threat | Requirement(s) | |--------|----------------| -| T-01 | REQ-E2E-004, REQ-E2E-005 | -| T-02 | REQ-AUTH-001, REQ-AUTH-002, REQ-TLS-001 | -| T-03 | REQ-RL-003 | -| T-04 | REQ-WDG-003, REQ-WDG-004 | -| T-05 | REQ-FW-005, REQ-FW-006 | -| T-06 | REQ-FW-007 | -| T-07 | REQ-E2E-006 | +| T-01 | REQ-E2E-007 | +| T-02 | REQ-AUTH-001, REQ-AUTH-003, REQ-TLS-001 | +| T-03 | REQ-RL-003, REQ-RL-004 | +| T-04 | REQ-WDG-001, REQ-WDG-003 | +| T-05 | REQ-E2E-001, REQ-E2E-004 | +| T-06 | REQ-E2E-006 | +| T-07 | REQ-E2E-007 | | T-08 | REQ-TLS-002 (HSM integration, external) | -| T-09 | REQ-WDG-008 | -| T-10 | REQ-AUTH-003, REQ-TLS-003 | +| T-09 | REQ-DISC-003, REQ-DISC-006 | +| T-10 | REQ-REGMAP-003 | +| T-11 | REQ-AUTH-003, REQ-TLS-001 | --- ## 6. Conclusion -All identified threats have corresponding mitigations aligned with IEC 62443 SL-2 -security level requirements. The residual risk profile is acceptable for -ASIL-B / SIL-2 operation. A re-assessment is required when: +All identified threats have corresponding mitigations aligned with IEC +62443 SL-2 security level requirements. The residual risk profile is +acceptable for ASIL-B / SIL-2 operation. A re-assessment is required when: - The threat landscape changes (new attack vectors identified) -- A new protocol bridge is enabled in production -- The TLS credential management policy changes +- A new protocol bridge (`mqttbr.hpp`/`ddsbr.hpp`/`someipbr.hpp`/ + `restbridge.hpp`/`grpcbridge.hpp`/`udsbr.hpp`/`doipbr.hpp`) moves past its + current unimplemented-stub state into production behavior +- The TLS credential management policy changes, or MACsec (802.1AE) + link-layer security is adopted for native Ethernet deployments diff --git a/include/rcp/rcp.hpp b/include/rcp/rcp.hpp index e123ad3..31bcdf0 100644 --- a/include/rcp/rcp.hpp +++ b/include/rcp/rcp.hpp @@ -1,26 +1,6 @@ -// fusa:req REQ-ZONE-001 -// fusa:req REQ-ZONE-002 -// fusa:req REQ-ZONE-003 -// fusa:req REQ-ZONE-004 -// fusa:req REQ-ZONE-005 -// fusa:req REQ-ZONE-006 -// fusa:req REQ-ZONE-007 -// fusa:req REQ-ZONE-008 // fusa:req REQ-PRI-001 // fusa:req REQ-PRI-002 // fusa:req REQ-PRI-003 -// fusa:req REQ-CMD-001 -// fusa:req REQ-CMD-002 -// fusa:req REQ-CMD-003 -// fusa:req REQ-CMD-004 -// fusa:req REQ-CMD-005 -// fusa:req REQ-CMD-006 -// fusa:req REQ-STATUS-001 -// fusa:req REQ-STATUS-002 -// fusa:req REQ-STATUS-003 -// fusa:req REQ-STATUS-004 -// fusa:req REQ-STATUS-005 -// fusa:req REQ-STATUS-006 // fusa:req REQ-ERR-001 // fusa:req REQ-ERR-002 // fusa:req REQ-ERR-003 @@ -56,15 +36,27 @@ // design predates cpp-RCP's alignment to the OPEN Alliance TC18 Remote // Control Protocol Specification v0.5.1_RC (see ROADMAP.md's Satellite // Package Disposition table, which marks this file REPLACE). It remains in -// place, unmodified in behavior, purely because roughly three dozen other -// headers under include/rcp/ still build against it, and their own rebind -// milestones (v2.9.0 onward per the Release Plan) haven't landed yet — see -// ROADMAP.md milestone 45 ("RC Server Lifecycle & Register-Map Model, -// v2.1.0") for why this file could not simply be deleted at that milestone. +// place, unmodified in behavior, purely because one remaining header under +// include/rcp/ — rcp/config.hpp — still builds against it (its own rebind +// is a separate, still-open item per milestone 60's closeout); every other +// former dependent has been rebound at its own milestone through v2.16.0. // The new stream/endpoint/register-map model that supersedes the types // below lives in rcp/avtp.hpp/rcp/acf.hpp (v2.0.0), rcp/lifecycle.hpp, and // rcp/regmap.hpp (both v2.1.0); do not build new functionality on top of // Zone/Command/Controller/Registry going forward. +// +// Certification Refresh notice (ROADMAP.md milestone 62, v2.18.0): the +// REQ-ZONE-*/REQ-CMD-*/REQ-STATUS-* requirement groups that used to trace +// to the Zone enum, CommandType enum, and Status struct/StatusChannel +// below are retired from .fusa-reqs.json as of this milestone — this file +// having no TC18 analog was already recorded at REPLACE above, so carrying +// certified requirement coverage for it any further would misrepresent +// this as safety-relevant surface going forward. The Priority enum +// (REQ-PRI-*), sentinel error codes (REQ-ERR-*), and the Command/Response +// struct shapes and ResponseStatus enum (REQ-CMDSTRUCT-*/REQ-RESP-*/ +// REQ-STAT-*) keep their existing requirement coverage unchanged, since +// milestone 62's own scope names only the Zone/CommandType/Status trio for +// retirement. #pragma once #include diff --git a/include/rcp/version.hpp b/include/rcp/version.hpp index a4f921b..cd89f63 100644 --- a/include/rcp/version.hpp +++ b/include/rcp/version.hpp @@ -6,6 +6,6 @@ namespace rcp { // Semantic version of the cpp-RCP implementation (matches the latest git tag). -constexpr std::string_view kVersion = "2.17.0"; +constexpr std::string_view kVersion = "2.18.0"; } // namespace rcp diff --git a/tests/test_rcp.cpp b/tests/test_rcp.cpp index dc66d87..86563c8 100644 --- a/tests/test_rcp.cpp +++ b/tests/test_rcp.cpp @@ -1,26 +1,6 @@ -// fusa:test REQ-ZONE-001 -// fusa:test REQ-ZONE-002 -// fusa:test REQ-ZONE-003 -// fusa:test REQ-ZONE-004 -// fusa:test REQ-ZONE-005 -// fusa:test REQ-ZONE-006 -// fusa:test REQ-ZONE-007 -// fusa:test REQ-ZONE-008 // fusa:test REQ-PRI-001 // fusa:test REQ-PRI-002 // fusa:test REQ-PRI-003 -// fusa:test REQ-CMD-001 -// fusa:test REQ-CMD-002 -// fusa:test REQ-CMD-003 -// fusa:test REQ-CMD-004 -// fusa:test REQ-CMD-005 -// fusa:test REQ-CMD-006 -// fusa:test REQ-STATUS-001 -// fusa:test REQ-STATUS-002 -// fusa:test REQ-STATUS-003 -// fusa:test REQ-STATUS-004 -// fusa:test REQ-STATUS-005 -// fusa:test REQ-STATUS-006 // fusa:test REQ-ERR-001 // fusa:test REQ-ERR-002 // fusa:test REQ-ERR-003 @@ -47,7 +27,7 @@ using namespace rcp; // ── Zone constants ──────────────────────────────────────────────────────────── -TEST_CASE("Zone::to_string returns unique non-empty name", "[zone][REQ-ZONE-001]") { +TEST_CASE("Zone::to_string returns unique non-empty name", "[zone]") { const std::vector zones{ Zone::FrontLeft, Zone::FrontRight, Zone::RearLeft, Zone::RearRight, @@ -62,7 +42,7 @@ TEST_CASE("Zone::to_string returns unique non-empty name", "[zone][REQ-ZONE-001] } } -TEST_CASE("Zone constants have correct numeric values", "[zone][REQ-ZONE-002][REQ-ZONE-003][REQ-ZONE-004][REQ-ZONE-005][REQ-ZONE-006][REQ-ZONE-007]") { +TEST_CASE("Zone constants have correct numeric values", "[zone]") { REQUIRE(static_cast(Zone::Unknown) == 0); REQUIRE(static_cast(Zone::FrontLeft) == 1); REQUIRE(static_cast(Zone::FrontRight) == 2); @@ -71,7 +51,7 @@ TEST_CASE("Zone constants have correct numeric values", "[zone][REQ-ZONE-002][RE REQUIRE(static_cast(Zone::Central) == 5); } -TEST_CASE("All Zone constants are distinct", "[zone][REQ-ZONE-008]") { +TEST_CASE("All Zone constants are distinct", "[zone]") { const std::vector zones{ Zone::FrontLeft, Zone::FrontRight, Zone::RearLeft, Zone::RearRight, @@ -94,7 +74,7 @@ TEST_CASE("Priority constants have correct ordering", "[priority][REQ-PRI-001][R // ── CommandType constants ───────────────────────────────────────────────────── -TEST_CASE("CommandType constants have correct numeric values", "[cmdtype][REQ-CMD-001][REQ-CMD-002][REQ-CMD-003][REQ-CMD-004][REQ-CMD-005]") { +TEST_CASE("CommandType constants have correct numeric values", "[cmdtype]") { REQUIRE(static_cast(CommandType::Noop) == 0); REQUIRE(static_cast(CommandType::Set) == 1); REQUIRE(static_cast(CommandType::Get) == 2); @@ -104,7 +84,7 @@ TEST_CASE("CommandType constants have correct numeric values", "[cmdtype][REQ-CM REQUIRE(static_cast(CommandType::Wake) == 6); } -TEST_CASE("All CommandType constants are distinct", "[cmdtype][REQ-CMD-006]") { +TEST_CASE("All CommandType constants are distinct", "[cmdtype]") { const std::vector cmds{ CommandType::Noop, CommandType::Set, CommandType::Get, CommandType::Reset, CommandType::Watchdog, @@ -118,7 +98,7 @@ TEST_CASE("All CommandType constants are distinct", "[cmdtype][REQ-CMD-006]") { // ── ResponseStatus constants ────────────────────────────────────────────────── -TEST_CASE("ResponseStatus::to_string returns unique non-empty name", "[status][REQ-STATUS-001]") { +TEST_CASE("ResponseStatus::to_string returns unique non-empty name", "[status]") { const std::vector statuses{ ResponseStatus::OK, ResponseStatus::Error, ResponseStatus::Timeout, ResponseStatus::Busy, @@ -133,14 +113,14 @@ TEST_CASE("ResponseStatus::to_string returns unique non-empty name", "[status][R } } -TEST_CASE("ResponseStatus constants have correct numeric values", "[status][REQ-STATUS-002][REQ-STATUS-003][REQ-STATUS-004][REQ-STATUS-005]") { +TEST_CASE("ResponseStatus constants have correct numeric values", "[status]") { REQUIRE(static_cast(ResponseStatus::OK) == 0); REQUIRE(static_cast(ResponseStatus::Error) == 1); REQUIRE(static_cast(ResponseStatus::Timeout) == 2); REQUIRE(static_cast(ResponseStatus::Busy) == 3); } -TEST_CASE("All ResponseStatus constants are distinct", "[status][REQ-STATUS-006]") { +TEST_CASE("All ResponseStatus constants are distinct", "[status]") { const std::vector statuses{ ResponseStatus::OK, ResponseStatus::Error, ResponseStatus::Timeout, ResponseStatus::Busy, diff --git a/tla/AntiReplayGuard.tla b/tla/AntiReplayGuard.tla deleted file mode 100644 index 4181ec4..0000000 --- a/tla/AntiReplayGuard.tla +++ /dev/null @@ -1,52 +0,0 @@ ----- MODULE AntiReplayGuard ---- -(* - * Formal specification of the E2E anti-replay sliding-window guard. - * - * The guard accepts a sequence number iff: - * (a) It has not been seen before, AND - * (b) high_water - seq_num < ReplayWindowSize - * - * Safety property (SP1): A previously accepted seq_num is never accepted again. - * Safety property (SP2): A seq_num more than ReplayWindowSize behind high_water - * is always rejected. - *) - -EXTENDS Naturals, Sequences, TLC - -CONSTANTS ReplayWindowSize \* size of the bitmap window (32 in production) - -VARIABLES high_water, \* highest seen sequence number - accepted \* set of all accepted sequence numbers - -TypeOK == - /\ high_water \in Nat - /\ accepted \in SUBSET Nat - -Init == - /\ high_water = 0 - /\ accepted = {} - -Check(n) == - \* Accept n if it is fresh and within the window - /\ n \notin accepted - /\ (high_water = 0 \/ high_water - n < ReplayWindowSize \/ n > high_water) - /\ accepted' = accepted \cup {n} - /\ high_water' = IF n > high_water THEN n ELSE high_water - -Reject(n) == \* Stutter-step: n is rejected, state unchanged - /\ (n \in accepted \/ (high_water > 0 /\ high_water - n >= ReplayWindowSize)) - /\ UNCHANGED <> - -Next == \E n \in Nat : Check(n) \/ Reject(n) - -Spec == Init /\ [][Next]_<> - -(* SP1: No double-acceptance *) -NoDoubleAccept == - [][\A n \in accepted : n \notin accepted']_accepted - -(* SP2: Old sequences are always rejected (checked via Check guard above) *) - -THEOREM Spec => TypeOK - -==== diff --git a/tla/CrcSafeStateLatch.cfg b/tla/CrcSafeStateLatch.cfg new file mode 100644 index 0000000..68c8829 --- /dev/null +++ b/tla/CrcSafeStateLatch.cfg @@ -0,0 +1,14 @@ +\* TLC model-checking configuration for CrcSafeStateLatch.tla. +\* EnforceLatch = TRUE exercises the affirmative latch behavior (rx_enforce_e2e +\* set); flip to FALSE separately to exercise NoLatchWithoutEnforce non-vacuously. +CONSTANT + EnforceLatch = TRUE + +INIT Init2 +NEXT Next + +INVARIANT TypeOK +PROPERTY LatchIsSticky +\* NoLatchWithoutEnforce is a tautology under EnforceLatch = TRUE (the +\* hypothesis ~EnforceLatch is vacuously false); check it non-vacuously by +\* re-running with EnforceLatch = FALSE in this file instead. diff --git a/tla/CrcSafeStateLatch.tla b/tla/CrcSafeStateLatch.tla new file mode 100644 index 0000000..373649e --- /dev/null +++ b/tla/CrcSafeStateLatch.tla @@ -0,0 +1,84 @@ +---- MODULE CrcSafeStateLatch ---- +(* + * Formal specification of rcp::e2e::RxStreamGuard (rcp/e2e.hpp, v2.6.0), + * the per-stream E2E CRC drop-vs-latch rule gated on the rx_enforce_e2e + * register bit. + * + * This is new formal-verification coverage added at the Certification + * Refresh milestone (ROADMAP.md milestone 62, v2.18.0): the roadmap + * identifies the E2E CRC / safe-state mechanism (v2.6.0) as the most + * safety-relevant new surface introduced across this whole roadmap, and + * the pre-replacement formal specs (tla/HealthStateMachine.tla, + * tla/WatchdogProtocol.tla) never modelled it — both instead modelled a + * three-state Healthy/Degraded/Faulted watchdog machine that predates the + * current architecture (see tla/WatchdogSafeState.tla for that + * mechanism's own replacement spec). + * + * Behavior modelled (own description of this implementation, not spec + * text): record_crc_result(ok) is called once per checked request on a + * stream. While the stream is not yet latched, a failing result (ok = + * FALSE) is always reported as an error for that request; if the stream's + * rx_enforce_e2e configuration is enabled, that first failure additionally + * latches the stream. Once latched, every subsequent call reports an + * error regardless of `ok`, until reset_latch() is called explicitly. + * + * Safety property (SP1): once latched, the guard never reports success + * again without an intervening reset_latch(). + * Safety property (SP2): a stream configured with rx_enforce_e2e = FALSE + * never latches on its own. + *) + +EXTENDS Naturals, TLC + +CONSTANTS EnforceLatch \* BOOLEAN: this stream's rx_enforce_e2e configuration + +VARIABLES latched \* BOOLEAN: whether the stream is currently latched + +TypeOK == + /\ latched \in BOOLEAN + /\ EnforceLatch \in BOOLEAN + +Init == + /\ latched = FALSE + +(* RecordResult mirrors RxStreamGuard::record_crc_result(cfg, ok). Returns + are not modelled as a variable — CrcResult below tracks the outcome of + the most recent call for the safety properties to reference. *) +VARIABLES last_result \* "ok" | "error" | "unset" — outcome reported by the last call + +RecordResult(ok) == + IF latched + THEN /\ last_result' = "error" + /\ UNCHANGED latched + ELSE IF ok + THEN /\ last_result' = "ok" + /\ UNCHANGED latched + ELSE /\ last_result' = "error" + /\ latched' = EnforceLatch \/ latched \* only sets latched when EnforceLatch + +ResetLatch == + /\ latched' = FALSE + /\ last_result' = last_result \* reset_latch() does not itself report a CRC result + +Next == + \/ \E ok \in BOOLEAN : RecordResult(ok) + \/ ResetLatch + +Init2 == Init /\ last_result = "unset" + +Spec == Init2 /\ [][Next]_<> + +(* SP1: Once latched, only an explicit ResetLatch step (identifiable in the + trace by last_result staying unchanged) ever clears it — every + RecordResult call, by construction, leaves `latched` unchanged while it + is already TRUE. *) +LatchIsSticky == + [][latched /\ latched' = FALSE => last_result' = last_result]_<> + +(* SP2: With EnforceLatch = FALSE, the stream never transitions to latched. *) +NoLatchWithoutEnforce == + ~EnforceLatch => [](~latched) + +THEOREM Spec => TypeOK /\ NoLatchWithoutEnforce /\ LatchIsSticky + +==== diff --git a/tla/HealthStateMachine.tla b/tla/HealthStateMachine.tla deleted file mode 100644 index fc3df8c..0000000 --- a/tla/HealthStateMachine.tla +++ /dev/null @@ -1,60 +0,0 @@ ----- MODULE HealthStateMachine ---- -(* - * Formal specification of the Watchdog HealthState machine (ISO 26262 ASIL-B). - * - * States: Healthy, Degraded, Faulted - * Events: kick (zone kicks watchdog), miss (watchdog interval elapsed, no kick) - * - * Safety property (SP1): A zone can only transition Healthy→Faulted via Degraded. - * Liveness property (LP1): If a zone continuously kicks, it stays Healthy. - *) - -EXTENDS Naturals, TLC - -CONSTANTS Zones \* set of zone identifiers -VARIABLES state, \* function: Zone -> HealthState - miss_count \* function: Zone -> Nat (consecutive miss count) - -Healthy == "Healthy" -Degraded == "Degraded" -Faulted == "Faulted" - -HealthStates == {Healthy, Degraded, Faulted} - -MaxMiss == 2 \* misses before Degraded→Faulted - -TypeOK == - /\ state \in [Zones -> HealthStates] - /\ miss_count \in [Zones -> Nat] - -Init == - /\ state = [z \in Zones |-> Healthy] - /\ miss_count = [z \in Zones |-> 0] - -Kick(z) == - /\ state' = [state EXCEPT ![z] = Healthy] - /\ miss_count' = [miss_count EXCEPT ![z] = 0] - -Miss(z) == - LET mc == miss_count[z] - IN - /\ miss_count' = [miss_count EXCEPT ![z] = mc + 1] - /\ IF state[z] = Healthy - THEN state' = [state EXCEPT ![z] = Degraded] - ELSE IF state[z] = Degraded /\ mc + 1 >= MaxMiss - THEN state' = [state EXCEPT ![z] = Faulted] - ELSE state' = state - -Next == - \E z \in Zones : Kick(z) \/ Miss(z) - -Spec == Init /\ [][Next]_<> - -(* Safety property SP1: No Healthy→Faulted direct transition *) -NoDirectFault == - [][\A z \in Zones : - state[z] = Healthy => state'[z] # Faulted]_<> - -THEOREM Spec => TypeOK /\ NoDirectFault - -==== diff --git a/tla/RxSequenceGuard.cfg b/tla/RxSequenceGuard.cfg new file mode 100644 index 0000000..55e12cb --- /dev/null +++ b/tla/RxSequenceGuard.cfg @@ -0,0 +1,10 @@ +\* TLC model-checking configuration for RxSequenceGuard.tla. +CONSTANT + MaxSeq = 4 + +INIT Init +NEXT Next + +INVARIANT TypeOK +PROPERTY Monotonic +PROPERTY NoStaleAcceptance diff --git a/tla/RxSequenceGuard.tla b/tla/RxSequenceGuard.tla new file mode 100644 index 0000000..f6197fa --- /dev/null +++ b/tla/RxSequenceGuard.tla @@ -0,0 +1,75 @@ +---- MODULE RxSequenceGuard ---- +(* + * Formal specification of rcp::e2e::RxSequenceGuard (rcp/e2e.hpp, v2.6.0), + * the strictly-increasing per-stream sequence check that fires when a + * request stream's rx_enforce_seq register bit is set. + * + * This module supersedes tla/AntiReplayGuard.tla, which modelled the + * pre-replacement 32-entry sliding-window bitmap guard removed at v2.6.0 — + * the current mechanism has no window to exhaust: it is a single + * comparison against the last accepted sequence number. + * + * Behavior modelled (own description of this implementation, not spec + * text): the first observed sequence number on a stream is always + * accepted and becomes the new high-water mark. Every subsequent + * sequence number is accepted iff it is strictly greater than the + * current high-water mark; otherwise it is rejected and state is + * unchanged. + * + * Safety property (SP1): the high-water mark (last_seq) never decreases. + * Safety property (SP2): once n has been accepted, no m <= n is ever + * accepted afterward — a direct consequence of SP1 + * combined with the Accept guard n > last_seq. + *) + +EXTENDS Naturals, TLC + +CONSTANTS MaxSeq \* bounds the state space for TLC + +VARIABLES has_last, \* whether any sequence number has been accepted yet + last_seq, \* last accepted sequence number (meaningless while ~has_last) + accepted \* set of all sequence numbers ever accepted + +TypeOK == + /\ has_last \in BOOLEAN + /\ last_seq \in 0..MaxSeq + /\ accepted \subseteq (0..MaxSeq) + +Init == + /\ has_last = FALSE + /\ last_seq = 0 + /\ accepted = {} + +(* Accept mirrors RxSequenceGuard::check with cfg.rx_enforce_seq = TRUE. *) +Accept(n) == + /\ n \in 0..MaxSeq + /\ \/ ~has_last + \/ n > last_seq + /\ has_last' = TRUE + /\ last_seq' = n + /\ accepted' = accepted \cup {n} + +Reject(n) == \* Stutter-step: n is rejected, state unchanged + /\ n \in 0..MaxSeq + /\ has_last + /\ n <= last_seq + /\ UNCHANGED <> + +Next == \E n \in 0..MaxSeq : Accept(n) \/ Reject(n) + +Spec == Init /\ [][Next]_<> + +(* SP1: Monotonicity — the high-water mark never decreases *) +Monotonic == + [][has_last /\ has_last' => last_seq' >= last_seq]_<> + +(* SP2: A number no greater than the current high-water mark is never + subsequently added to `accepted` — the set only ever gains numbers + strictly above every number already in it. *) +NoStaleAcceptance == + [][accepted' # accepted => + \A n \in accepted : (accepted' \ accepted) \subseteq {m \in 0..MaxSeq : m > n}]_accepted + +THEOREM Spec => TypeOK /\ Monotonic /\ NoStaleAcceptance + +==== diff --git a/tla/WatchdogProtocol.tla b/tla/WatchdogProtocol.tla deleted file mode 100644 index 835b611..0000000 --- a/tla/WatchdogProtocol.tla +++ /dev/null @@ -1,57 +0,0 @@ ----- MODULE WatchdogProtocol ---- -(* - * Formal specification of the Watchdog heartbeat protocol. - * - * The keeper polls for kicks every Interval. A zone must kick within - * Interval milliseconds or the keeper records a miss. - * - * Safety property (SP1): Keeper never transitions a zone to Faulted - * without first passing through Degraded. - * Liveness property (LP1): If a zone sends kicks infinitely often, - * it remains Healthy infinitely often. - *) - -EXTENDS Naturals, TLC - -CONSTANTS Zones, Interval - -VARIABLES zone_state, \* Zone -> {Healthy, Degraded, Faulted} - last_kick, \* Zone -> Nat (simulated clock at last kick) - clock \* Nat (global simulated clock tick) - -Healthy == "Healthy" -Degraded == "Degraded" -Faulted == "Faulted" - -Init == - /\ zone_state = [z \in Zones |-> Healthy] - /\ last_kick = [z \in Zones |-> 0] - /\ clock = 0 - -Kick(z) == - /\ last_kick' = [last_kick EXCEPT ![z] = clock] - /\ UNCHANGED <> - -Tick == - /\ clock' = clock + 1 - /\ \A z \in Zones : - LET gap == clock' - last_kick[z] - IN IF gap > Interval - THEN zone_state' = [zone_state EXCEPT - ![z] = CASE zone_state[z] = Healthy -> Degraded - [] zone_state[z] = Degraded -> Faulted - [] OTHER -> Faulted] - ELSE zone_state' = zone_state - /\ UNCHANGED last_kick - -Next == (\E z \in Zones : Kick(z)) \/ Tick - -Spec == Init /\ [][Next]_<> - -SP1_NoDirectFault == - [][\A z \in Zones : - zone_state[z] = Healthy => zone_state'[z] # Faulted]_<> - -THEOREM Spec => SP1_NoDirectFault - -==== diff --git a/tla/WatchdogSafeState.cfg b/tla/WatchdogSafeState.cfg new file mode 100644 index 0000000..41f3ece --- /dev/null +++ b/tla/WatchdogSafeState.cfg @@ -0,0 +1,15 @@ +\* TLC model-checking configuration for WatchdogSafeState.tla. +\* SafestateEnabled = TRUE exercises the affirmative latch behavior +\* (rx_wd_safestate_enable set); flip to FALSE separately to exercise +\* NoLatchWithoutEnable non-vacuously. BoundedClock keeps the otherwise +\* infinite Nat-valued clock state space finite for TLC. +CONSTANT + TimeoutInterval = 3 + SafestateEnabled = TRUE + +INIT Init +NEXT Next + +INVARIANT TypeOK +PROPERTY LatchIsSticky +CONSTRAINT BoundedClock diff --git a/tla/WatchdogSafeState.tla b/tla/WatchdogSafeState.tla new file mode 100644 index 0000000..8290435 --- /dev/null +++ b/tla/WatchdogSafeState.tla @@ -0,0 +1,101 @@ +---- MODULE WatchdogSafeState ---- +(* + * Formal specification of rcp::e2e::RxWatchdog / rcp::watchdog:: + * StreamWatchdog (rcp/e2e.hpp, rcp/watchdog.hpp, v2.6.0/v2.10.0), the + * per-request-stream watchdog and safe-state latch. + * + * This module replaces tla/HealthStateMachine.tla and + * tla/WatchdogProtocol.tla, which both modelled a three-state + * Healthy/Degraded/Faulted machine keyed by "Zone" and driven by a + * client-side periodic CommandType::Watchdog kick — the pre-replacement + * design discarded outright at v2.10.0 per ROADMAP.md's Satellite Package + * Disposition table entry for `watchdog.hpp`. The current mechanism has + * no Degraded intermediate state: a stream is armed (not latched) or + * latched into safe state, and it is kicked by any accepted inbound + * request — not a dedicated watchdog command — regardless of request kind + * or safety tag. + * + * Behavior modelled (own description of this implementation, not spec + * text): kick(now) records the current time as the last-seen-activity + * clock. overflowed(now) reports TRUE once more than TimeoutInterval time + * units have elapsed since the last kick, but only once the watchdog has + * been kicked at least once and is not already latched — an unkicked or + * already-latched watchdog does not re-fire. When a stream is configured + * with SafestateEnabled, an observed overflow latches safe state; when it + * is not, the overflow is reported but nothing latches. clear_safe_state + * is the only way to unlatch, mirroring rcp/e2e.hpp's/rcp/watchdog.hpp's + * explicit-unlatch convention used throughout this codebase since v2.6.0. + * + * Safety property (SP1): the watchdog never latches while + * SafestateEnabled = FALSE. + * Safety property (SP2): once latched, only an explicit ClearSafeState + * step (identifiable by every other state + * component staying unchanged) ever unlatches it — + * Kick and Tick, by construction, never set + * latched' = FALSE while latched = TRUE. + *) + +EXTENDS Naturals, TLC + +CONSTANTS TimeoutInterval, \* rx_wd_timeout_interval, a positive constant + SafestateEnabled \* BOOLEAN: this stream's rx_wd_safestate_enable configuration + +VARIABLES kicked, \* BOOLEAN: has kick() ever been called + last_kick, \* simulated clock value at the last kick() + clock, \* simulated clock, advanced by Tick + latched \* BOOLEAN: whether safe state is currently latched + +TypeOK == + /\ kicked \in BOOLEAN + /\ last_kick \in Nat + /\ clock \in Nat + /\ latched \in BOOLEAN + /\ TimeoutInterval \in Nat \ {0} + +Init == + /\ kicked = FALSE + /\ last_kick = 0 + /\ clock = 0 + /\ latched = FALSE + +(* Kick mirrors RxWatchdog::kick(now_ms) — does not itself clear a latch. *) +Kick == + /\ kicked' = TRUE + /\ last_kick' = clock + /\ UNCHANGED <> + +(* Tick advances the simulated clock by one unit and, if the watchdog is + armed (kicked, not latched) and the elapsed time now exceeds + TimeoutInterval, applies the overflow rule: latch iff SafestateEnabled, + mirroring StreamWatchdog::check + e2e::apply_watchdog_overflow. *) +Tick == + /\ clock' = clock + 1 + /\ IF kicked /\ ~latched /\ (clock' - last_kick) > TimeoutInterval + THEN latched' = SafestateEnabled + ELSE latched' = latched + /\ UNCHANGED <> + +ClearSafeState == + /\ latched' = FALSE + /\ UNCHANGED <> + +Next == Kick \/ Tick \/ ClearSafeState + +Spec == Init /\ [][Next]_<> + +(* SP1: No latch without SafestateEnabled *) +NoLatchWithoutEnable == + ~SafestateEnabled => [](~latched) + +(* SP2: A latch is only cleared by a step that leaves every other state + component unchanged — the fingerprint of ClearSafeState, since Kick + always changes <> and Tick always changes clock. *) +LatchIsSticky == + [][latched /\ latched' = FALSE => UNCHANGED <>]_ + <> + +THEOREM Spec => TypeOK /\ NoLatchWithoutEnable /\ LatchIsSticky + +BoundedClock == clock < 10 \* TLC state-space bound only; not part of the modelled system + +====