docs: security assessment specs (fleet-fixes, host-hardening, 1.0 §10, threat model)
This commit is contained in:
@@ -0,0 +1,320 @@
|
||||
# tines fleet deployment v1 — fixes from the security assessment
|
||||
|
||||
Date: 2026-10-19
|
||||
Status: draft v1. Not yet reviewed.
|
||||
Fixes: findings F1–F5 and F17 in `THREAT_MODEL.md` (assessed at `3b1a644`)
|
||||
Amends: `2026-10-18-tines-fleet-deployment-design.md` (milestone M3)
|
||||
|
||||
## Intent
|
||||
|
||||
The fleet milestone's code has landed, but the security assessment found
|
||||
that several of its promises don't hold even with no attacker present:
|
||||
|
||||
- custody is lost when a store is full;
|
||||
- the standalone service never exchanges anything;
|
||||
- BLE can't accept connections and doesn't keep frames intact;
|
||||
- restarts repeat sequence numbers and forget released messages;
|
||||
- one corrupt log record deletes the rest of the log;
|
||||
- the service's clock runs in the wrong units.
|
||||
|
||||
This spec fixes those six findings so M3 does what its spec says. It adds
|
||||
no features.
|
||||
|
||||
## Why now, and why not in 1.0
|
||||
|
||||
These are M3 bugs. M3 can't ship with them, so they can't wait for 1.0.
|
||||
All but F1 live in host crates (`tines-store`, `tines-bt`, `tines`,
|
||||
`tines-ros2`), which stay 0.x and aren't covered by the 1.0 promise (1.0
|
||||
spec, D4). The core-side hardening that does belong with 1.0 (F6, F8, F9,
|
||||
F13) is in the 1.0 spec, §10. Host hardening (F10–F12) has its own spec,
|
||||
`2026-10-19-tines-host-hardening.md`.
|
||||
|
||||
## Goals
|
||||
|
||||
1. Custody is never released for a message the receiver didn't keep (F1).
|
||||
2. The standalone `tines` service exchanges observations over its
|
||||
transport (F2).
|
||||
3. `tines-bt` has the following properties (F3):
|
||||
- it accepts as well as initiates connections;
|
||||
- it preserves frame boundaries;
|
||||
- it binds each connection to the advertised NodeId;
|
||||
- it reports `Contact`/`Lost`.
|
||||
4. A robot's `next_seq` never repeats across restarts, and released flags
|
||||
survive restarts (F4).
|
||||
5. Log recovery loses only a torn tail. A corrupt record elsewhere costs
|
||||
that record, not the rest of the log (F5).
|
||||
6. Every host uses one monotonic millisecond clock for `Tick` (F17).
|
||||
|
||||
## Non-goals
|
||||
|
||||
- **Authentication or encryption of any kind.** The NodeId binding in
|
||||
goal 3 is only as trustworthy as an unauthenticated advertisement. It
|
||||
stops accidents and makes `from` checks meaningful; it doesn't stop an
|
||||
attacker (1.1, 1.0 spec §2b).
|
||||
- Growth bounds, trimming defaults, bounded channels, IPC permissions, ROS2
|
||||
isolation: host hardening spec.
|
||||
- Peer eviction, summary rate limits, identity pinning in core: 1.0 spec
|
||||
§10.
|
||||
- Multi-peer configuration of the service beyond what F3 needs (see §3).
|
||||
|
||||
## Constraints
|
||||
|
||||
- tines-core invariants are unchanged (no_std, no I/O, no panics on
|
||||
untrusted input, `Addr` ↔ NodeId mapping stays in the transport).
|
||||
- **The F1 fix is a core behaviour change** and must keep the fleet sim
|
||||
properties green, plus add the one they missed.
|
||||
- No robots run tines yet, so log formats may change without migration:
|
||||
existing logs are wiped (1.0 spec, D5).
|
||||
- TDD per AGENTS.md: each finding gets a failing regression test first.
|
||||
|
||||
## The how
|
||||
|
||||
### 1. F1 — ack only what was kept (tines-core)
|
||||
|
||||
`Exchange::accept` (exchange.rs ~795-820) currently enqueues an ack for
|
||||
every receive except a released addressed duplicate, including when
|
||||
`insert` fails.
|
||||
|
||||
New rule, matching the fleet spec's own eligibility rule ("B never acks a
|
||||
… store-full receive"):
|
||||
|
||||
| `insert` result | Addressed | Broadcast |
|
||||
|---|---|---|
|
||||
| `Ok(true)` (new) | ack | ack |
|
||||
| `Ok(false)`, local copy not released | ack | ack |
|
||||
| `Ok(false)`, local copy released | **no ack** (existing rule) | n/a |
|
||||
| `Err(_)` (full, backend error) | **no ack** | **no ack** |
|
||||
|
||||
- Broadcasts follow the same rule. Acking an unstored broadcast would fire
|
||||
a false confidence event at the sender.
|
||||
- No bounce record on `Err` (already true).
|
||||
- **Tests:**
|
||||
- A unit test with a store that returns `Full`: no Ack frame is
|
||||
emitted, and the sender's copy stays unreleased.
|
||||
- A sim property: the "≥ 1 holder" invariant holds when some nodes use a
|
||||
store with a small capacity that returns `Full`. Add a capped wrapper
|
||||
store to tines-sim for this; `MemStore` never fills.
|
||||
- Fix the `accept` comment ("even an un-stored id").
|
||||
|
||||
### 2. F2 — the service runs the exchange (tines)
|
||||
|
||||
The service gets a poll loop. Today `serve()` only answers IPC.
|
||||
|
||||
- **Structure:**
|
||||
- `Node` lives behind a `Mutex`, shared by the IPC thread and a new
|
||||
exchange thread.
|
||||
- The exchange thread loops:
|
||||
1. `poll(now)` until it returns 0 or a per-iteration cap is reached;
|
||||
2. sleep for `poll_interval_ms` (config, default 20 ms);
|
||||
3. on schedule, `trim(policy, now)` and `store.flush()`. The trim
|
||||
policy and its defaults are in the host hardening spec; this spec
|
||||
only requires that the hook exists and is called.
|
||||
- **Lock poisoning:** a panic in either thread exits the process with a
|
||||
non-zero code. Systemd restarts it (host hardening spec). Continuing with
|
||||
a node in an unknown state isn't allowed.
|
||||
- **Generic over `Transport`:** the service's core loop is generic over
|
||||
`Transport`, so tests can run it on an in-memory link.
|
||||
- **Test:** two service instances over an in-memory transport. An
|
||||
observation made through one's IPC becomes a belief readable through the
|
||||
other's IPC.
|
||||
|
||||
### 3. F3 — tines-bt: framing, roles, binding, contact events
|
||||
|
||||
1. **Preserve frame boundaries.** Switch from `l2cap::Stream` to
|
||||
`l2cap::SeqPacket` (`SeqPacket::connect` and `SeqPacketListener`, both
|
||||
in bluer 0.17). One L2CAP SDU is one frame.
|
||||
- The negotiated MTU is still reported through `mtu()`, clamped to
|
||||
`MAX_FRAME`.
|
||||
- If SeqPacket proves unusable on the Jetson or Pi BlueZ versions, the
|
||||
fallback is an explicit `u16` length prefix on a stream. The builder
|
||||
records which was chosen and why.
|
||||
2. **Roles.** Every node both advertises and scans.
|
||||
- When a node discovers an eligible peer (see binding), the one with the
|
||||
numerically smaller NodeId dials, per the fleet spec rule
|
||||
(`is_central`).
|
||||
- The larger one only accepts, on a `SeqPacketListener` bound to the
|
||||
tines PSM (`0x008D`).
|
||||
- So every node runs a listener for the whole session, not only after it
|
||||
loses a race.
|
||||
3. **Binding.** The scanner decodes the advertised NodeId from service data
|
||||
(UUID `0xFE7E`, checking the UUID, which `decode_node_id` doesn't do
|
||||
today) and records `bt address → NodeId` for each eligible advertiser.
|
||||
- **Eligible** means either a NodeId in the configured allowlist
|
||||
(`peers`, a list; empty means any tines advertiser), or any tines
|
||||
advertiser if no allowlist is set.
|
||||
- **Outbound connection:** bound to the NodeId that was advertised by the
|
||||
address it dials.
|
||||
- **Inbound connection:** bound via `peer_addr()` looked up in the scan
|
||||
map. An inbound connection from an address with no recent eligible
|
||||
advertisement is closed immediately.
|
||||
- **Use the discovered address type.** Today it's hard-coded to
|
||||
`LePublic` (transport.rs:307).
|
||||
4. **Addr and the `from` check.**
|
||||
- `Addr` is the bound NodeId of the connection a frame arrived on.
|
||||
`read_loop` stamps frames with that bound NodeId, not the configured
|
||||
`peer`.
|
||||
- `BtTransport::poll` drops any frame whose decoded `from` differs from
|
||||
that bound `Addr`. The check now means something; it remains
|
||||
unauthenticated.
|
||||
- The transport doesn't decode frames; it peeks at the `from` field.
|
||||
Because core's `Frame` layout is private after 1.0, core exposes a
|
||||
`pub fn frame_sender(bytes) -> Option<NodeId>` for this. That's new
|
||||
public API, called out per AGENTS.md, and the only one this spec adds.
|
||||
It's added to the 1.0 public surface (1.0 spec §3).
|
||||
5. **Contact and Lost.**
|
||||
- A connection that is up emits `Event::Contact(addr)`.
|
||||
- Its end (EOF, error, adapter loss) emits `Event::Lost(addr)`. Today
|
||||
neither is emitted, so core's per-contact state never resets.
|
||||
- After a loss, scanning and listening continue, so the node reconnects.
|
||||
6. **Several peers.** The radio supports up to `MAX_PEERS` concurrent
|
||||
connections, one per bound NodeId; a second connection to the same
|
||||
NodeId replaces the first. The single `peer` config field becomes the
|
||||
optional `peers` allowlist (see 3). This is the minimum needed for a
|
||||
fleet of more than two robots to work at all.
|
||||
7. **Errors aren't swallowed.** Failures of the radio thread, adapter
|
||||
power-on and advertising are surfaced, either through `RadioEvent` or as
|
||||
a returned error the host logs. The radio thread's exit is reported.
|
||||
Today all of these are discarded or only logged.
|
||||
|
||||
**Tests** (the `Radio` trait already makes the transport testable without
|
||||
hardware):
|
||||
- frame boundaries are preserved for back-to-back frames;
|
||||
- a frame with a mismatched `from` is dropped;
|
||||
- `Contact`/`Lost` are emitted;
|
||||
- an inbound connection from an unknown address is rejected;
|
||||
- the role is decided by NodeId order.
|
||||
|
||||
The SeqPacket and BlueZ path gets a manual two-device check, written up in
|
||||
`tines-bt/README.md`.
|
||||
|
||||
### 4. F4 — seq continuity and durable releases (tines-store, both hosts)
|
||||
|
||||
1. **Boot counter.** `LogStore` keeps a persisted boot counter.
|
||||
- `LogStore::open` increments it and durably writes it (`fsync`) before
|
||||
returning.
|
||||
- It then exposes `first_seq() -> u64 = boot_count << 32`, which is
|
||||
core's documented contract.
|
||||
- Both hosts seed `Node::new` from `store.first_seq()`, never from
|
||||
config. The `first_seq` config field is removed.
|
||||
- A boot can make up to 2³² observations, which is enough for any
|
||||
robot.
|
||||
2. **Remove the insert-counting `next_seq`.** `LogStore::next_seq`
|
||||
(log.rs:352) counts received observations too, so it isn't the node's
|
||||
seq. It's removed along with the `Meta` record's `next_seq` field.
|
||||
3. **Releases are written when they happen.**
|
||||
- `Store::release` appends a `Release { id }` record immediately, rather
|
||||
than relying on a later `flush` to write the whole released set in
|
||||
`Meta`. `Meta`'s `released` list goes away, which also removes the
|
||||
oversized-`Meta` self-truncation in F5.
|
||||
- `release` stays infallible (1.0 spec §4): an append error is logged,
|
||||
and the worst case is a duplicate custodian after a reboot.
|
||||
4. **Flush on a schedule.** Both hosts call `store.flush()` at least every
|
||||
`flush_interval_ms` (config, default 1000 ms) and on clean shutdown.
|
||||
`flush` is `fsync`.
|
||||
5. **Clock marker for ages across reboot.** The fleet spec promised that
|
||||
pre-reboot elapsed time is folded into ages, but there's no clock-marker
|
||||
record today.
|
||||
- `flush` appends a `Clock { tick }` record. On load,
|
||||
`age += last_clock_tick − stored_at` for each live observation,
|
||||
saturating, before rebasing.
|
||||
- Downtime stays invisible (no RTC), as the fleet spec accepted.
|
||||
- The marker is only meaningful within a boot, so the hosts must use
|
||||
the F17 clock.
|
||||
6. **Tests:**
|
||||
- Reopen twice: `first_seq` strictly increases, and observations made
|
||||
after each reopen don't collide.
|
||||
- Release, kill without flush, reopen: the release survives.
|
||||
- Ages after reopen include the time since `stored_at` up to the last
|
||||
clock marker.
|
||||
|
||||
### 5. F5 — log integrity and recovery (tines-store)
|
||||
|
||||
New log format, version 1. Old logs are refused, and logs are wiped
|
||||
(D5).
|
||||
|
||||
```
|
||||
file = header record*
|
||||
header = magic "TINESLOG" ‖ format_version: u16 ‖ reserved: u16
|
||||
record = sync: u32 (constant) ‖ len: u32 ‖ crc32c: u32 ‖ body[len]
|
||||
```
|
||||
|
||||
- **CRC32C** covers `len ‖ body`. A per-record checksum protects against
|
||||
accidental corruption only; a keyed MAC is out of scope (threat model
|
||||
F5, A5).
|
||||
- **Write cap.** `write_record` refuses a record over `MAX_RECORD_BYTES`
|
||||
(8 KiB) with `StoreError::Backend`, so the writer can no longer produce
|
||||
a record the reader rejects.
|
||||
- **Recovery rule:**
|
||||
- A record whose CRC, length or decode is bad is **skipped**: scan
|
||||
forward for the next `sync` value, and check that candidate's CRC
|
||||
before accepting it.
|
||||
- Only bad bytes at the end, with no valid record after them, count as a
|
||||
torn tail.
|
||||
- A torn tail is truncated, then the file and its directory are fsynced.
|
||||
- Skipped corrupt records are counted and reported once on open (stderr,
|
||||
and a counter the host can read).
|
||||
- **Ids are recomputed** from the decoded observation on load. The stored
|
||||
`id` field is dropped from the format.
|
||||
- **Exclusive lock.** `open` takes an exclusive lock (`File::try_lock`,
|
||||
stable since Rust 1.89; the toolchain is 1.99). A second opener gets a
|
||||
clear error instead of interleaving.
|
||||
- **Permissions.** Create the file with mode `0600`, and create its parent
|
||||
directory (mode `0700`) if it's missing.
|
||||
- **Header errors.** A missing or unknown header is an error that names
|
||||
the fix (delete the log), per 1.0 spec §9. The 1.0 work then bumps
|
||||
`format_version` for the new `Observation` encoding, and doesn't
|
||||
introduce the header itself.
|
||||
- **Tests:**
|
||||
- corrupt middle record: the records after it survive;
|
||||
- torn tail: truncated;
|
||||
- an oversized record is refused at write;
|
||||
- a second `open` fails while the first holds the lock;
|
||||
- permissions are `0600`.
|
||||
|
||||
### 6. F17 — one monotonic millisecond clock (tines, tines-ros2)
|
||||
|
||||
- Each host has one `HostClock`: an `Instant` captured at process start.
|
||||
`now() -> Tick` is the milliseconds elapsed since then.
|
||||
- It replaces `now_ms()` in `tines/src/ipc.rs`, which returns
|
||||
wall-clock *seconds*.
|
||||
- It's the clock the ROS2 host documents for callers of
|
||||
`TinesNode::poll(now)`.
|
||||
- `LogStore::open` takes `now` from the same clock. That's `0` at
|
||||
startup, which is now correct by construction: the clock starts at 0.
|
||||
- **Wall-clock time is used only for `observed_at`** (1.0 spec §2,
|
||||
milliseconds since the Unix epoch), and only when the host is configured
|
||||
to trust its clock.
|
||||
- **Test:** the service's tick advances in milliseconds, and an addressed
|
||||
observation with `lifetime_ms = 1000` expires after about 1 s, not
|
||||
about 1000 s.
|
||||
|
||||
## Acceptance
|
||||
|
||||
- `sh scripts/ci.sh` is green, with every regression test above added
|
||||
first and seen failing.
|
||||
- The fleet sim properties still pass, plus the new full-store custody
|
||||
property.
|
||||
- A manual two-robot BLE check is done: both directions connect, frames
|
||||
round-trip, the connection is lost and re-established, and an
|
||||
observation propagates.
|
||||
- `THREAT_MODEL.md` marks F1–F5 and F17 fixed, with the fixing commit.
|
||||
- The fleet spec's claims that were false (F3 binding, released flags
|
||||
across reboot, ages across reboot) are now true, so no errata are
|
||||
needed.
|
||||
|
||||
## Left to the builder
|
||||
|
||||
- SeqPacket vs length-prefixed stream, if SeqPacket misbehaves on the
|
||||
target BlueZ (record the outcome).
|
||||
- The `sync` constant value, and the CRC crate (`crc32c` or equivalent,
|
||||
`std` only).
|
||||
- The poll loop's per-iteration cap and lock granularity.
|
||||
- The scan-map retention time for "recent eligible advertisement".
|
||||
|
||||
## Sequencing
|
||||
|
||||
1. F1 (core, small).
|
||||
2. F17 (both hosts; the other fixes depend on the clock).
|
||||
3. F4 and F5 together (one log format change).
|
||||
4. F2.
|
||||
5. F3 (largest; needs `frame_sender` from core).
|
||||
Reference in New Issue
Block a user