Zachery Aaron Shores-Chmielewski
33a217c96a
Initial experiments in 'formal verification' of authorization tooling. Current state is not to be trusted, but we are not in a security critical situation, so that is fine. Signed-off-by: Zachery Aaron Shores-Chmielewski <zacheryasc@gmail.com>
60 KiB
Formal Verification Report: Datastore Auth System
Date: 2026-02-19
Branch: formal-verification
Tools: proptest-state-machine 0.3 (Phase 1), Kani (Phase 2), Stateright 0.31 (Phase 3)
Abstract
The authorization system is the security boundary of the swactor datastore — every external request must pass through GatewayActor, which delegates decisions to AuthzEngine. Three complementary verification techniques are applied to this boundary. Phase 1 randomizes operation sequences against a deliberately simple reference model, catching emergent bugs across thousands of grant/revoke/sign/gc interactions with real ed25519 crypto (high coverage, function level). Phase 2 symbolically executes all possible inputs through bounded proofs using Kani's SMT solver, proving that every reachable branch satisfies its specification (exhaustive within bounds, function level). Phase 3 model-checks all message orderings at the dispatch level using Stateright, exhaustively exploring every interleaving of grants, revokes, signed requests, signature checks, GC ticks, and clock advances to verify that unauthorized messages never reach internal actors (exhaustive, actor level). Together these three phases cover seven safety properties (S1–S7) and five liveness/reachability properties (L1–L5). One real bug was found and fixed during Phase 1: grant(owner, owner) was adding the owner to the explicit authorized set, creating an irremovable entry that violated the design invariant of purely implicit owner access.
1. Architecture Overview
The Two-Layer Design
The auth system has two verification targets:
-
AuthzEngine(function level) — a pure decision engine. Given a request, it returnsAllowedorDenied. It holds the ACL, nonce replay state, and timestamp window. This is the subject of Phases 1 and 2. -
GatewayActor(dispatch level) — the actor that holds anAuthzEngineinstance and uses its decisions to route messages. The security-critical question isn't just "does the engine return the right answer?" but "does the actor act on it correctly?" This is the subject of Phase 3.
The Auth Pipeline
External Client → GatewayActor → DatastoreNode → MetadataActor/BlobStoreActor
(auth check) (dispatch) (auth-unaware)
The gateway is the ONLY path to internal actors. If the gateway dispatches incorrectly, the entire auth system is bypassed.
The Handler Inventory
The gateway has 11 message handlers. Of these, EXACTLY ONE (handle_signed_request) sends to self.datastore_node. The other 10 send exclusively to reply_to. This asymmetry is the foundation of property S7: "unauthorized messages never reach internal actors."
The critical dispatch path — handle_signed_request at gateway.rs:69-80:
fn handle_signed_request(&mut self, ctx: &Ctx, request: crate::auth::SignedRequest, reply_to: ActorAddress) {
let now = Self::now_secs();
match self.engine.check_signed_request(&request, now) {
AuthzResult::Allowed => {
let msg = action_to_node_msg(request.payload.action, reply_to);
let _ = ctx.send(self.datastore_node, msg); // ← THE ONLY send to datastore_node
}
AuthzResult::Denied(reason) => {
let _ = ctx.send(reply_to, DatastoreResponse::Denied { reason });
}
}
}
Line 74 — ctx.send(self.datastore_node, msg) — is the ONLY place in the entire gateway that sends to datastore_node. The full handle() match confirms this (gateway.rs:176-221):
fn handle(&mut self, ctx: &Ctx, msg: GatewayMsg) {
match msg {
GatewayMsg::HandleSignedRequest { request, reply_to } => {
self.handle_signed_request(ctx, request, reply_to); // → datastore_node on Allowed
}
GatewayMsg::CheckConnection { node_id, reply_to } => {
self.handle_check_connection(ctx, node_id, reply_to); // → reply_to only
}
GatewayMsg::Grant { requester, key, label, reply_to } => {
self.handle_grant(ctx, requester, key, label, reply_to); // → reply_to only
}
GatewayMsg::Revoke { requester, key, reply_to } => {
self.handle_revoke(ctx, requester, key, reply_to); // → reply_to only
}
GatewayMsg::Authorize { request, reply_to } => {
self.handle_authorize(ctx, request, reply_to); // → reply_to only
}
GatewayMsg::VerifySignature { request, reply_to } => {
self.handle_verify_signature(ctx, request, reply_to); // → reply_to only
}
GatewayMsg::SubmitAccessRequest { key, name, message, reply_to } => {
self.handle_submit_access_request(ctx, key, name, message, reply_to); // → reply_to only
}
GatewayMsg::ListAccessRequests { requester, reply_to } => {
self.handle_list_access_requests(ctx, requester, reply_to); // → reply_to only
}
GatewayMsg::DenyAccessRequest { requester, key, reply_to } => {
self.handle_deny_access_request(ctx, requester, key, reply_to); // → reply_to only
}
GatewayMsg::ListAuthorizedKeys { requester, reply_to } => {
self.handle_list_authorized_keys(ctx, requester, reply_to); // → reply_to only
}
GatewayMsg::NonceGcTick => {
self.engine.gc_nonces(Self::now_secs()); // no send at all
}
}
}
AuthzEngine State
The engine (auth.rs:191-206) holds three fields:
pub struct AuthzEngine {
pub acl: AccessControlList, // owner + authorized_keys
seen_nonces: HashMap<[u8; 16], u64>, // replay protection
timestamp_window: u64, // freshness window (300s)
}
impl AuthzEngine {
pub fn new(acl: AccessControlList) -> Self {
Self {
acl,
seen_nonces: HashMap::new(),
timestamp_window: 300,
}
}
}
The engine is stateful because nonce tracking requires memory — each seen nonce is recorded with its timestamp so that GC can evict expired entries.
2. Property Catalog
Safety Properties (S1–S7)
Things that must NEVER happen. Each is a universal claim: "for all states, for all inputs, X holds."
| ID | Property | Formal Statement |
|---|---|---|
| S1 | ACL integrity | check_node(n) = Allowed implies n == owner or n ∈ authorized_keys |
| S2 | Signature verification | Invalid signature always yields Denied(InvalidSignature) |
| S3 | Timestamp freshness | |now - ts| > 300 always yields Denied(RequestExpired) |
| S4 | Replay protection | Seen nonce always yields Denied(ReplayDetected) |
| S5 | ACL immutability | Non-owner grant()/revoke() always returns Err(NotAuthorized) |
| S6 | Owner persistence | check_node(owner) = Allowed holds after any operation sequence |
| S7 | Dispatch integrity | DatastoreNodeMsg is only sent when the signer is authorized |
Liveness / Reachability Properties (L1–L5)
Things that CAN happen. Existential claims that prove the system isn't trivially safe by being non-functional.
| ID | Property | Meaning |
|---|---|---|
| L1 | Grant leads to access | A granted key has Allowed status until revoked |
| L2 | GC enables nonce reuse | After time advances past the window, GC frees expired nonces |
| L3 | Authorized dispatch reachable | There exists a reachable state where authorized dispatch happened |
| L4 | Granted key can dispatch | A non-owner granted key can trigger dispatch to datastore_node |
| L5 | Dispatch after GC reachable | Dispatch occurs with an empty nonce table (after GC clears all) |
Coverage Matrix
| Property | Phase 1 (proptest) | Phase 2 (Kani) | Phase 3 (Stateright) | Scenario Tests |
|---|---|---|---|---|
| S1 | postcondition + invariant | proof_s1_check_node |
— | unknown_key_is_denied |
| S2 | — | proof_signed_request_4step_ordering |
— | tampered_signature_is_rejected |
| S3 | postcondition | proof_signed_request_4step_ordering |
— | stale_timestamp_is_rejected |
| S4 | postcondition | proof_signed_request_4step_ordering |
— | replayed_nonce_is_rejected |
| S5 | postcondition | proof_s5_non_owner_cannot_mutate_acl |
— | non_owner_cannot_grant/revoke |
| S6 | invariant | proof_s6_owner_irremovable |
S6-gw (always) |
revoking_owner_is_noop |
| S7 | — | — | S7 (always) + L3 canary |
actor-level tests |
| L1 | invariant | — | — | grant_then_revoke_lifecycle |
| L2 | emergent | proof_gc_preserves_owner_and_frees_expired |
— | nonce_gc_frees_old_nonces |
| L3 | — | — | L3 (sometimes) |
— |
| L4 | — | — | L4 (sometimes) |
— |
| L5 | — | — | L5 (sometimes) |
— |
Why Proptest Cannot Test S2
Proptest uses real ed25519 signing — the state machine always generates valid signatures by construction. It never produces an invalid signature, so it can never trigger the InvalidSignature branch. Kani stubs crypto as a boolean (sig_valid: bool), making S2 testable symbolically — Kani explores both sig_valid = true and sig_valid = false, proving the signature check rejects correctly. The scenario test tampered_signature_is_rejected covers S2 concretely by bit-flipping a real signature.
3. Production Code Under Verification
These are the actual production functions. They serve as the reference for judging mirror faithfulness in Phases 2 and 3.
check_node (auth.rs:211-217)
The simplest check — the oracle for all authorization decisions. S1 and S7 both depend on this function.
pub fn check_node(&self, node_id: &NodeId) -> AuthzResult {
if *node_id == self.acl.owner || self.acl.authorized_keys.contains(node_id) {
AuthzResult::Allowed
} else {
AuthzResult::Denied(DeniedReason::NotAuthorized)
}
}
check_signed_request (auth.rs:252-273)
The most critical function. Four-step pipeline in strict order:
pub fn check_signed_request(&mut self, request: &SignedRequest, now: u64) -> AuthzResult {
// 1. Signature
if !verify_signed_request(request) {
return AuthzResult::Denied(DeniedReason::InvalidSignature);
}
// 2. Timestamp freshness
let ts = request.payload.timestamp;
let diff = if now >= ts { now - ts } else { ts - now };
if diff > self.timestamp_window {
return AuthzResult::Denied(DeniedReason::RequestExpired);
}
// 3. Nonce uniqueness
if self.seen_nonces.contains_key(&request.payload.nonce) {
return AuthzResult::Denied(DeniedReason::ReplayDetected);
}
self.seen_nonces.insert(request.payload.nonce, ts);
// 4. ACL check
self.check_node(&request.public_key)
}
Key design detail: the nonce is consumed at step 3 BEFORE the ACL check at step 4. This means an unauthorized request with a valid signature and fresh timestamp still consumes the nonce. This is deliberate — it prevents an attacker from probing ACL membership without cost. All mirrors must replicate this ordering.
check_signature_only (auth.rs:223-243)
Steps 1–3 only, no ACL check. Used by VerifySignature and Authorize handlers. Important: it shares nonce state with check_signed_request — a nonce consumed by check_signature_only is also consumed for check_signed_request.
pub fn check_signature_only(&mut self, request: &SignedRequest, now: u64) -> AuthzResult {
// 1. Signature
if !verify_signed_request(request) {
return AuthzResult::Denied(DeniedReason::InvalidSignature);
}
// 2. Timestamp freshness
let ts = request.payload.timestamp;
let diff = if now >= ts { now - ts } else { ts - now };
if diff > self.timestamp_window {
return AuthzResult::Denied(DeniedReason::RequestExpired);
}
// 3. Nonce uniqueness
if self.seen_nonces.contains_key(&request.payload.nonce) {
return AuthzResult::Denied(DeniedReason::ReplayDetected);
}
self.seen_nonces.insert(request.payload.nonce, ts);
AuthzResult::Allowed
}
grant and revoke (auth.rs:277-305)
Both have an owner guard. grant has the owner self-grant no-op guard (the bug that was found and fixed). revoke has the owner-revoke no-op guard. Both are idempotent.
pub fn grant(&mut self, requester: &NodeId, key: NodeId, label: Option<String>) -> Result<(), DeniedReason> {
if *requester != self.acl.owner {
return Err(DeniedReason::NotAuthorized);
}
if key == self.acl.owner {
return Ok(()); // Owner has implicit access — no-op ← THE FIX
}
self.acl.authorized_keys.insert(key);
if let Some(name) = label {
let hex: String = key.0.iter().map(|b| format!("{b:02x}")).collect();
self.acl.key_labels.insert(hex, name);
}
Ok(())
}
pub fn revoke(&mut self, requester: &NodeId, key: NodeId) -> Result<(), DeniedReason> {
if *requester != self.acl.owner {
return Err(DeniedReason::NotAuthorized);
}
// Owner's implicit access cannot be removed.
if key != self.acl.owner {
self.acl.authorized_keys.remove(&key);
let hex: String = key.0.iter().map(|b| format!("{b:02x}")).collect();
self.acl.key_labels.remove(&hex);
}
Ok(())
}
gc_nonces (auth.rs:321-326)
Retains nonces where |now - ts| <= window. Simple, but critical for L2 and L5.
pub fn gc_nonces(&mut self, now: u64) {
self.seen_nonces.retain(|_nonce, ts| {
let diff = if now >= *ts { now - *ts } else { *ts - now };
diff <= self.timestamp_window
});
}
4. Phase 1: Proptest State Machine
4a. Technique: State Machine Testing
State machine testing runs two implementations — a reference model and the system under test (SUT) — through the same randomly-generated transition sequence. After every transition, invariants are checked and postconditions are asserted. Any disagreement is a bug: in the SUT if the reference model is correct, or in the reference model if the SUT is correct. The reference model is kept simple enough that its correctness is visually obvious.
The proptest-state-machine crate provides:
ReferenceStateMachine: defines state type, transition type,init_state(),transitions()(weighted generator), andapply().StateMachineTest: wraps the SUT withinit_test(),apply()(postconditions), andcheck_invariants().prop_state_machine!macro: wires them together and runs the test.
Configuration (auth_state_machine.rs:472-484):
prop_state_machine! {
#![proptest_config(proptest::test_runner::Config {
cases: 512, // 512 random sequences
max_shrink_iters: 1000, // shrink failures to minimal repros
.. proptest::test_runner::Config::default()
})]
#[test]
fn auth_engine_state_machine(sequential 1..100 => AuthTest);
// up to 100 transitions per sequence
}
512 random sequences × up to 100 transitions = up to 51,200 transitions explored.
The six transition types with their weights (auth_state_machine.rs:46-68, 90-128):
enum AuthOp {
Grant { requester_idx: usize, target_idx: usize },
Revoke { requester_idx: usize, target_idx: usize },
CheckNode { key_idx: usize },
SignedRequest { signer_idx: usize, fresh_timestamp: bool, reuse_nonce: bool, nonce_bytes: [u8; 16] },
AdvanceClock { delta: u64 },
GcNonces,
}
Transition weights: Grant(3), Revoke(3), CheckNode(3), SignedRequest-fresh(5), SignedRequest-reuse(2), AdvanceClock(2), GcNonces(1). SignedRequest is weighted highest because it exercises the most complex code path. The reuse-nonce variant specifically targets S4 (replay detection).
Generator logic:
fn transitions(state: &Self::State) -> BoxedStrategy<Self::Transition> {
let has_last_nonce = state.last_nonce.is_some();
prop_oneof![
3 => (0..NUM_KEYS, 0..NUM_KEYS).prop_map(|(r, t)| AuthOp::Grant {
requester_idx: r, target_idx: t,
}),
3 => (0..NUM_KEYS, 0..NUM_KEYS).prop_map(|(r, t)| AuthOp::Revoke {
requester_idx: r, target_idx: t,
}),
3 => (0..NUM_KEYS).prop_map(|k| AuthOp::CheckNode { key_idx: k }),
5 => (0..NUM_KEYS, any::<bool>(), prop::array::uniform16(any::<u8>()))
.prop_map(|(s, fresh, nonce)| AuthOp::SignedRequest {
signer_idx: s, fresh_timestamp: fresh,
reuse_nonce: false, nonce_bytes: nonce,
}),
2 => (0..NUM_KEYS, any::<bool>(), prop::array::uniform16(any::<u8>()))
.prop_map(move |(s, fresh, fallback_nonce)| AuthOp::SignedRequest {
signer_idx: s, fresh_timestamp: fresh,
reuse_nonce: has_last_nonce, nonce_bytes: fallback_nonce,
}),
2 => (0u64..600).prop_map(|d| AuthOp::AdvanceClock { delta: d }),
1 => Just(AuthOp::GcNonces),
].boxed()
}
4b. The Reference Model
The reference model is the TRUST ANCHOR of Phase 1. If it's wrong, the test is wrong. So it must be simple enough to audit by inspection.
RefAuthModel (auth_state_machine.rs:32-41):
struct RefAuthModel {
owner_idx: usize,
authorized: HashSet<usize>, // which key indices are authorized
used_nonces: HashSet<[u8; 16]>, // which nonces have been consumed
nonce_timestamps: HashMap<[u8; 16], u64>, // nonce → timestamp for GC
clock: u64,
last_nonce: Option<[u8; 16]>, // for reuse_nonce transitions
}
The full apply() function — the entire reference model transition logic (auth_state_machine.rs:130-210):
fn apply(mut state: Self::State, transition: &Self::Transition) -> Self::State {
match transition {
AuthOp::Grant { requester_idx, target_idx } => {
if *requester_idx == state.owner_idx && *target_idx != state.owner_idx {
state.authorized.insert(*target_idx);
}
// Non-owner grant or owner self-grant: no change
}
AuthOp::Revoke { requester_idx, target_idx } => {
if *requester_idx == state.owner_idx && *target_idx != state.owner_idx {
state.authorized.remove(target_idx);
}
}
AuthOp::CheckNode { .. } => {
// Read-only — no state change
}
AuthOp::SignedRequest { fresh_timestamp, reuse_nonce, nonce_bytes, .. } => {
let nonce = if *reuse_nonce {
state.last_nonce.unwrap_or(*nonce_bytes)
} else {
*nonce_bytes
};
// Model the 4-step verification to determine if nonce gets consumed:
// Step 1 (sig): always passes in our model (we use real signing)
// Step 2 (timestamp): check freshness
let ts = if *fresh_timestamp { state.clock }
else { state.clock.saturating_sub(400) };
let diff = if state.clock >= ts { state.clock - ts }
else { ts - state.clock };
if diff > 300 {
// Expired — nonce NOT consumed (step 2 rejects before step 3)
} else if state.used_nonces.contains(&nonce) {
// Replay detected — nonce already in set (step 3 rejects)
} else {
// Nonce consumed at step 3 (before ACL check at step 4)
state.used_nonces.insert(nonce);
state.nonce_timestamps.insert(nonce, ts);
}
state.last_nonce = Some(nonce);
}
AuthOp::AdvanceClock { delta } => {
state.clock += delta;
}
AuthOp::GcNonces => {
let window = 300u64;
let now = state.clock;
state.used_nonces.retain(|nonce| {
if let Some(&ts) = state.nonce_timestamps.get(nonce) {
let diff = if now >= ts { now - ts } else { ts - now };
diff <= window
} else { false }
});
state.nonce_timestamps.retain(|_, ts| {
let diff = if now >= *ts { now - *ts } else { *ts - now };
diff <= window
});
}
}
state
}
Each arm is 1–5 lines. Grant is literally: if requester == owner && target != owner { authorized.insert(target) }. The SignedRequest arm mirrors the 4-step pipeline, computing whether the nonce would be consumed based on timestamp freshness and replay status, and updating used_nonces accordingly. The nonce-consumed-before-ACL-check design is replicated here — the nonce is inserted regardless of whether the signer passes the ACL check.
4c. SUT Wiring and the Pre-Transition Problem
The SUT wraps a real AuthzEngine with real Keypairs. All operations use real ed25519 crypto.
SutAuth struct (auth_state_machine.rs:219-233):
struct SutAuth {
engine: AuthzEngine,
keys: Vec<Keypair>,
clock: u64,
last_nonce: Option<[u8; 16]>,
/// Mirror of the engine's nonce set — used to compute expected results
/// before the engine call mutates state. We can't use ref_state because
/// proptest-state-machine passes the *post-transition* reference state.
known_nonces: HashSet<[u8; 16]>,
/// Nonce → timestamp, mirrors engine's seen_nonces for GC
nonce_timestamps: HashMap<[u8; 16], u64>,
/// Track which key indices are authorized (pre-transition mirror).
/// Needed because ref_state.authorized is post-transition for Grant/Revoke.
authorized_indices: HashSet<usize>,
}
The pre-transition problem: proptest-state-machine passes the POST-transition reference state to apply(). But for SignedRequest, we need to know the PRE-transition nonce set to compute the expected result (because the engine call mutates state). Solution: the SUT maintains its own known_nonces and authorized_indices mirrors, updated after each transition.
The SignedRequest postcondition (auth_state_machine.rs:332-397):
AuthOp::SignedRequest { signer_idx, fresh_timestamp, reuse_nonce, nonce_bytes } => {
// 1. Resolve nonce
let nonce = if reuse_nonce {
sut.last_nonce.unwrap_or(nonce_bytes)
} else { nonce_bytes };
// 2. Compute expected timestamp
let ts = if fresh_timestamp { sut.clock }
else { sut.clock.saturating_sub(400) };
// 3. Using PRE-transition state, determine expected result
let diff = if sut.clock >= ts { sut.clock - ts } else { ts - sut.clock };
let is_replay = sut.known_nonces.contains(&nonce);
let is_authorized = signer_idx == 0 || sut.authorized_indices.contains(&signer_idx);
let expected = if diff > 300 {
AuthzResult::Denied(DeniedReason::RequestExpired) // S3
} else if is_replay {
AuthzResult::Denied(DeniedReason::ReplayDetected) // S4
} else if is_authorized {
AuthzResult::Allowed
} else {
AuthzResult::Denied(DeniedReason::NotAuthorized) // S1
};
// 4. Call engine and assert
let payload = SignedRequestPayload {
action: DatastoreAction::List { name_filter: None },
timestamp: ts, nonce,
};
let request = sign_request(&sut.keys[signer_idx], payload);
let result = sut.engine.check_signed_request(&request, sut.clock);
assert_eq!(result, expected,
"SignedRequest mismatch: signer_idx={signer_idx}, fresh_ts={fresh_timestamp}, \
reuse_nonce={reuse_nonce}, diff={diff}");
// 5. Update pre-transition mirror
if diff <= 300 && !is_replay {
sut.known_nonces.insert(nonce);
sut.nonce_timestamps.insert(nonce, ts);
}
sut.last_nonce = Some(nonce);
}
The Grant/Revoke postconditions assert S5 directly (auth_state_machine.rs:264-310):
AuthOp::Grant { requester_idx, target_idx } => {
let owner_idx = 0;
let requester = sut.keys[requester_idx].node_id();
let target = sut.keys[target_idx].node_id();
let result = sut.engine.grant(&requester, target, None);
// S5: Non-owner cannot mutate ACL
if requester_idx != owner_idx {
assert_eq!(result, Err(DeniedReason::NotAuthorized),
"S5 violated: non-owner grant succeeded");
} else {
assert!(result.is_ok(), "Owner grant should succeed");
if target_idx != owner_idx {
sut.authorized_indices.insert(target_idx);
}
}
}
AuthOp::Revoke { requester_idx, target_idx } => {
let owner_idx = 0;
let requester = sut.keys[requester_idx].node_id();
let target = sut.keys[target_idx].node_id();
let result = sut.engine.revoke(&requester, target);
// S5: Non-owner cannot mutate ACL
if requester_idx != owner_idx {
assert_eq!(result, Err(DeniedReason::NotAuthorized),
"S5 violated: non-owner revoke succeeded");
} else {
assert!(result.is_ok(), "Owner revoke should succeed");
if target_idx != owner_idx {
sut.authorized_indices.remove(&target_idx);
}
}
}
4d. Invariants: Three Checks After Every Transition
These are not postconditions (which are per-transition). These run after EVERY transition regardless of type (auth_state_machine.rs:422-467):
fn check_invariants(sut: &Self::SystemUnderTest, ref_state: &RefAuthModel) {
// S6: Owner access is irremovable — must hold after every transition
let owner_id = sut.keys[ref_state.owner_idx].node_id();
assert_eq!(
sut.engine.check_node(&owner_id), AuthzResult::Allowed,
"S6 violated: owner lost access"
);
// S1: Reference model agrees with SUT on every key
for idx in 0..NUM_KEYS {
let node = sut.keys[idx].node_id();
let sut_result = sut.engine.check_node(&node);
let ref_allowed = idx == ref_state.owner_idx || ref_state.authorized.contains(&idx);
if ref_allowed {
assert_eq!(sut_result, AuthzResult::Allowed,
"S1 invariant: key_idx={idx} should be allowed");
} else {
assert_eq!(sut_result, AuthzResult::Denied(DeniedReason::NotAuthorized),
"S1 invariant: key_idx={idx} should be denied");
}
}
// L1: Every granted (non-revoked) key has access
for &idx in &ref_state.authorized {
let node = sut.keys[idx].node_id();
assert_eq!(
sut.engine.check_node(&node), AuthzResult::Allowed,
"L1 violated: granted key_idx={idx} denied"
);
}
}
S6 catches owner-persistence bugs from interaction effects (e.g., a grant followed by a revoke that accidentally removes the owner). S1 is a full consistency check across all 4 key indices — not just the key involved in the current transition. L1 ensures that every key the reference model considers authorized is actually allowed by the engine.
4e. Phase 1 Boundaries
- S2 is NOT tested — real crypto is used, so signatures are always valid. The
InvalidSignaturebranch is never reached. - S7 is NOT tested — the state machine drives
AuthzEnginedirectly, not throughGatewayActor. Dispatch behavior is not exercised. - Coverage is probabilistic, not exhaustive. 512 × 100 = up to 51,200 transitions is high coverage, and proptest shrinks failing cases to minimal repros, but rare edge cases might survive.
- No concurrency testing —
AuthzEngineis driven single-threaded.
5. Phase 2: Kani Bounded Proofs
5a. Why a Bounded Mirror Is Necessary
Kani performs symbolic execution: instead of concrete values, it reasons over ALL possible values simultaneously using SMT solvers. This provides exhaustive coverage within bounds — every reachable branch is explored.
The problem: HashMap/HashSet use SipHash internally. SipHash involves bitwise operations that create exponential symbolic path explosion. Kani cannot tractably reason about hash-based collections.
The solution: replace hash collections with fixed-size arrays. KaniAuthzEngine uses [Option<KaniNodeId>; MAX_KEYS] instead of HashSet<NodeId>, and [Option<([u8; 2], u64)>; MAX_NONCES] instead of HashMap<[u8; 16], u64>.
KaniNodeId([u8; 2]) — 2 bytes giving 65,536 unique values. This is sufficient because the control flow depends only on equality comparisons, not key magnitude. If the logic is correct for 65K values, it's correct for 32-byte values — the branches are identical.
Crypto is stubbed: sig_valid: bool replaces verify_signed_request(). This enables S2 testing (which proptest can't do) — Kani explores both sig_valid = true and sig_valid = false.
Bounded types and engine struct (kani_auth.rs:17-36):
const MAX_KEYS: usize = 3;
const MAX_NONCES: usize = 2;
#[derive(Clone, Copy, PartialEq, Eq)]
struct KaniNodeId([u8; 2]);
struct KaniAuthzEngine {
owner: KaniNodeId,
authorized_keys: [Option<KaniNodeId>; MAX_KEYS],
key_count: usize,
seen_nonces: [Option<([u8; 2], u64)>; MAX_NONCES],
nonce_count: usize,
timestamp_window: u64,
}
Mirror check_node (kani_auth.rs:115-121) — compare with production (auth.rs:211-217):
// Mirror (kani_auth.rs:115-121) | Production (auth.rs:211-217)
fn check_node(&self, node_id: &KaniNodeId) | pub fn check_node(&self, node_id: &NodeId)
-> AuthzResult { | -> AuthzResult {
if *node_id == self.owner | if *node_id == self.acl.owner
|| self.keys_contains(node_id) { | || self.acl.authorized_keys.contains(node_id) {
AuthzResult::Allowed | AuthzResult::Allowed
} else { | } else {
AuthzResult::Denied( | AuthzResult::Denied(
DeniedReason::NotAuthorized) | DeniedReason::NotAuthorized)
} | }
} | }
Mirror check_signed_request (kani_auth.rs:156-187) — compare with production (auth.rs:252-273):
// Mirror (kani_auth.rs) | Production (auth.rs)
fn check_signed_request(&mut self, | pub fn check_signed_request(&mut self,
sig_valid: bool, | request: &SignedRequest,
public_key: &KaniNodeId, | now: u64) -> AuthzResult {
timestamp: u64, nonce: [u8; 2], |
now: u64) -> AuthzResult { |
// 1. Signature | // 1. Signature
if !sig_valid { | if !verify_signed_request(request) {
return Denied(InvalidSignature); } | return Denied(InvalidSignature); }
|
// 2. Timestamp freshness | // 2. Timestamp freshness
let diff = if now >= timestamp | let ts = request.payload.timestamp;
{ now - timestamp } | let diff = if now >= ts { now - ts }
else { timestamp - now }; | else { ts - now };
if diff > self.timestamp_window { | if diff > self.timestamp_window {
return Denied(RequestExpired); } | return Denied(RequestExpired); }
|
// 3. Nonce uniqueness | // 3. Nonce uniqueness
if self.nonces_contains(&nonce) { | if self.seen_nonces.contains_key(
return Denied(ReplayDetected); } | &request.payload.nonce) {
self.nonces_insert(nonce, timestamp); | return Denied(ReplayDetected); }
| self.seen_nonces.insert(
| request.payload.nonce, ts);
// 4. ACL check |
self.check_node(public_key) | // 4. ACL check
} | self.check_node(&request.public_key)
| }
The branch structure is identical: if !sig → return, if diff > window → return, if nonces_contains → return, nonces_insert; check_node.
5b. The Five Proof Harnesses
All five #[kani::proof] functions (kani_auth.rs:216-381):
S5: proof_s5_non_owner_cannot_mutate_acl — For ALL owner, requester, target where requester != owner: both grant() and revoke() return Err(NotAuthorized). No loops, no unwind needed. The simplest harness — proves the owner guard is total.
#[kani::proof]
fn proof_s5_non_owner_cannot_mutate_acl() {
let owner = KaniNodeId(kani::any());
let requester = KaniNodeId(kani::any());
let target = KaniNodeId(kani::any());
kani::assume(requester != owner);
let mut engine = KaniAuthzEngine::new(owner);
assert!(engine.grant(&requester, target) == Err(DeniedReason::NotAuthorized));
assert!(engine.revoke(&requester, target) == Err(DeniedReason::NotAuthorized));
}
S1: proof_s1_check_node — Creates an engine, grants 0..MAX_KEYS symbolic keys, then queries with a symbolic node. If the result is Allowed, asserts the query is either the owner or one of the granted keys. The contrapositive: no ungranted, non-owner key can ever get Allowed. #[kani::unwind(5)] bounds loop iterations.
#[kani::proof]
#[kani::unwind(5)]
fn proof_s1_check_node() {
let owner = KaniNodeId(kani::any());
let mut engine = KaniAuthzEngine::new(owner);
let num_keys: usize = kani::any();
kani::assume(num_keys <= MAX_KEYS);
let mut granted = [KaniNodeId([0; 2]); MAX_KEYS];
let mut i = 0;
while i < num_keys {
granted[i] = KaniNodeId(kani::any());
engine.keys_insert(granted[i]);
i += 1;
}
let query = KaniNodeId(kani::any());
let result = engine.check_node(&query);
if result == AuthzResult::Allowed {
let mut is_authorized = query == owner;
let mut j = 0;
while j < num_keys {
if query == granted[j] { is_authorized = true; }
j += 1;
}
assert!(is_authorized);
}
}
S6: proof_s6_owner_irremovable — 5 symbolic grant/revoke operations with arbitrary requesters and targets. After all 5, asserts check_node(owner) == Allowed. Proves owner persistence survives ANY sequence of up to 5 ACL mutations by any requester. #[kani::unwind(7)] bounds the main loop.
#[kani::proof]
#[kani::unwind(7)]
fn proof_s6_owner_irremovable() {
let owner = KaniNodeId(kani::any());
let mut engine = KaniAuthzEngine::new(owner);
const MAX_OPS: usize = 5;
let mut i = 0;
while i < MAX_OPS {
let requester = KaniNodeId(kani::any());
let target = KaniNodeId(kani::any());
let is_grant: bool = kani::any();
if is_grant {
let _ = engine.grant(&requester, target);
} else {
let _ = engine.revoke(&requester, target);
}
i += 1;
}
assert!(engine.check_node(&owner) == AuthzResult::Allowed);
}
S2/S3/S4: proof_signed_request_4step_ordering — The most complex harness. Optionally grants one key, optionally pre-inserts a nonce. Then calls check_signed_request with fully symbolic inputs. Pattern-matches the result and asserts the correct preconditions for each denial branch:
#[kani::proof]
#[kani::unwind(4)]
fn proof_signed_request_4step_ordering() {
let owner = KaniNodeId(kani::any());
let mut engine = KaniAuthzEngine::new(owner);
// Optionally grant one key
let has_granted: bool = kani::any();
let granted_key = KaniNodeId(kani::any());
if has_granted { engine.keys_insert(granted_key); }
// Optionally pre-insert a nonce (to test replay detection)
let pre_nonce: bool = kani::any();
let nonce: [u8; 2] = kani::any();
if pre_nonce {
let old_ts: u64 = kani::any();
engine.nonces_insert(nonce, old_ts);
}
let sig_valid: bool = kani::any();
let public_key = KaniNodeId(kani::any());
let timestamp: u64 = kani::any();
let now: u64 = kani::any();
let diff = if now >= timestamp { now - timestamp }
else { timestamp - now };
let result = engine.check_signed_request(sig_valid, &public_key, timestamp, nonce, now);
match result {
AuthzResult::Denied(DeniedReason::InvalidSignature) => {
assert!(!sig_valid); // Step 1 rejected
}
AuthzResult::Denied(DeniedReason::RequestExpired) => {
assert!(sig_valid); // Step 1 passed
assert!(diff > 300); // Step 2 rejected
}
AuthzResult::Denied(DeniedReason::ReplayDetected) => {
assert!(sig_valid); // Step 1 passed
assert!(diff <= 300); // Step 2 passed
assert!(pre_nonce); // Step 3 rejected
}
AuthzResult::Denied(DeniedReason::NotAuthorized) => {
assert!(sig_valid); // Step 1 passed
assert!(diff <= 300); // Step 2 passed
assert!(public_key != owner); // Step 4 rejected: not in ACL
}
AuthzResult::Allowed => {
assert!(sig_valid); // All 4 steps passed
assert!(diff <= 300);
assert!(public_key == owner || engine.keys_contains(&public_key));
}
}
}
This is the strongest harness — it proves the 4-step ordering is correct for ALL possible input combinations. Each denial reason implies exactly the correct preconditions:
DeniedBadSig→!sig_valid(step 1 rejected correctly)DeniedExpired→sig_valid && diff > 300(step 2 rejected, step 1 passed)DeniedReplay→sig_valid && diff <= 300 && pre_nonce(step 3 rejected, steps 1–2 passed)DeniedNotAuthorized→sig_valid && diff <= 300 && key ∉ ACL(step 4 rejected, steps 1–3 passed)Allowed→ all 4 steps passed
GC: proof_gc_preserves_owner_and_frees_expired — Inserts a symbolic nonce at time t1, runs GC at t2 >= t1. Asserts: (a) owner access survives GC, (b) if t2 - t1 > 300, the nonce is freed.
#[kani::proof]
#[kani::unwind(4)]
fn proof_gc_preserves_owner_and_frees_expired() {
let owner = KaniNodeId(kani::any());
let mut engine = KaniAuthzEngine::new(owner);
let nonce: [u8; 2] = kani::any();
let t1: u64 = kani::any();
let t2: u64 = kani::any();
kani::assume(t2 >= t1);
engine.nonces_insert(nonce, t1);
engine.gc_nonces(t2);
// Owner always survives GC
assert!(engine.check_node(&owner) == AuthzResult::Allowed);
// Expired nonces must be freed
if t2 - t1 > 300 {
assert!(!engine.nonces_contains(&nonce));
}
}
5c. Mirror Faithfulness
The proofs are only as strong as the mirror's correspondence to production code. If the mirror has different branch structure, the proofs prove the wrong thing.
Each mirror function has a doc comment citing exact production source lines. The bounded-set helpers are semantically equivalent to their HashSet counterparts (kani_auth.rs:52-109):
fn keys_contains(&self, id: &KaniNodeId) -> bool {
let mut i = 0;
while i < self.key_count {
if let Some(k) = self.authorized_keys[i] {
if k == *id { return true; }
}
i += 1;
}
false
}
fn keys_insert(&mut self, id: KaniNodeId) {
if self.keys_contains(&id) { return; }
if self.key_count < MAX_KEYS {
self.authorized_keys[self.key_count] = Some(id);
self.key_count += 1;
}
}
fn keys_remove(&mut self, id: &KaniNodeId) {
let mut i = 0;
while i < self.key_count {
if let Some(k) = self.authorized_keys[i] {
if k == *id {
self.authorized_keys[i] = self.authorized_keys[self.key_count - 1];
self.authorized_keys[self.key_count - 1] = None;
self.key_count -= 1;
return;
}
}
i += 1;
}
}
fn nonces_contains(&self, nonce: &[u8; 2]) -> bool {
let mut i = 0;
while i < self.nonce_count {
if let Some((n, _)) = self.seen_nonces[i] {
if n == *nonce { return true; }
}
i += 1;
}
false
}
fn nonces_insert(&mut self, nonce: [u8; 2], ts: u64) {
if self.nonce_count < MAX_NONCES {
self.seen_nonces[self.nonce_count] = Some((nonce, ts));
self.nonce_count += 1;
}
}
These perform linear scans over fixed arrays — semantically identical to HashSet::contains/insert/remove within the bounded capacity.
5d. Bounds and Limitations
The proofs are exhaustive WITHIN bounds. Beyond the bounds, they don't apply directly — but the argument for generalization is strong because the bounded types cover all reachable branch combinations.
| Bound | Value | Rationale |
|---|---|---|
KaniNodeId |
[u8; 2] (65,536 values) |
Control flow only depends on ==/!=, so this is sufficient |
MAX_KEYS |
3 | Covers: empty ACL, single key, full capacity. Auth logic is a linear scan, so 3 entries cover all loop-count cases |
MAX_NONCES |
2 | Covers: empty, single, full capacity |
MAX_OPS (S6) |
5 | 5 grant/revoke operations with arbitrary requesters/targets. Each op is binary (grant or revoke), so this explores 2^5 = 32 operation sequences × symbolic key values |
What is NOT proven:
- The
HashMap/HashSetimplementation (trusted stdlib) - Hash collision behavior (irrelevant —
NodeIdequality is byte-exact) - Concurrent access (not applicable — engine is single-threaded within the actor)
6. Phase 3: Stateright Model Checking
6a. Why Phase 3 Is Needed: The Function-Dispatch Gap
Phases 1–2 prove AuthzEngine returns correct results. But the security property we actually care about is: "unauthorized messages never reach DatastoreNode." This depends on GatewayActor USING the engine's result correctly.
A hypothetical bug: imagine handle_signed_request dispatches on Denied instead of Allowed (the match arms are swapped). Phases 1–2 would all pass because the engine itself is correct — they never test the gateway. Only Phase 3 catches this.
What Stateright adds: exhaustive exploration of all MESSAGE SEQUENCES. Not just "does the engine handle one request correctly?" but "after grant(A), revoke(A), advance_clock, gc_tick, request(A) — in every possible ordering — is dispatch correct?"
Stateright is a Rust model checker. The Model trait (not Actor) is used because we're verifying a single actor's internal logic, not multi-actor communication.
6b. Model Structure: Bounded State and Actions
Bounded parameters (gateway_model_check.rs:12-27):
const OWNER: u8 = 0;
const KEY_A: u8 = 1;
const KEY_B: u8 = 2;
const NONCES: [u8; 2] = [0, 1];
const TIMESTAMPS: [u8; 4] = [0, 1, 2, 3];
const WINDOW: u8 = 1; // scaled from production's 300s
const KEYS: [u8; 3] = [OWNER, KEY_A, KEY_B];
3 node IDs (owner + 2 clients), 2 nonces, 4 timestamps, window=1. Small but covers all interesting combinations: authorized vs unauthorized keys, fresh vs expired timestamps, fresh vs replayed nonces, pre-GC vs post-GC states.
GatewayState (gateway_model_check.rs:34-46):
#[derive(Clone, Debug, Hash, PartialEq, Eq)]
struct GatewayState {
acl: Vec<u8>, // sorted — Hash requirement
seen_nonces: Vec<(u8, u8)>, // sorted (nonce, timestamp) pairs
now: u8, // current wall clock
s7_violated: bool, // monotonic violation flag
has_dispatched: bool, // true after any dispatch to datastore_node
}
Sorted Vecs instead of HashSet because State must implement Hash for Stateright's state deduplication.
GatewayAction (gateway_model_check.rs:51-83):
enum GatewayAction {
SignedRequest { signer: u8, nonce: u8, timestamp: u8, sig_valid: bool },
Authorize { signer: u8, nonce: u8, timestamp: u8, sig_valid: bool },
VerifySignature { signer: u8, nonce: u8, timestamp: u8, sig_valid: bool },
Grant { requester: u8, target: u8 },
Revoke { requester: u8, target: u8 },
GcTick,
AdvanceClock,
}
7 variants mapping to the 6 modeled production handlers plus AdvanceClock. Total actions per state: 3×2×4×2 (SignedRequest) + 3×2×4×2 (Authorize) + 3×2×4×2 (VerifySignature) + 3×3 (Grant) + 3×3 (Revoke) + 1 (GcTick) + 1 (AdvanceClock) = 48+48+48+9+9+1+1 = 164 actions per state.
Handlers modeled vs skipped: 6 modeled (HandleSignedRequest, Grant, Revoke, Authorize, VerifySignature, NonceGcTick). 5 skipped (CheckConnection, SubmitAccessRequest, ListAccessRequests, DenyAccessRequest, ListAuthorizedKeys). Skipped handlers either only read state or only touch pending_requests — they cannot affect the ACL, nonce set, or dispatch behavior.
The full cross-product generation (gateway_model_check.rs:255-321):
fn actions(&self, _state: &Self::State, actions: &mut Vec<Self::Action>) {
for &signer in &KEYS {
for &nonce in &NONCES {
for &ts in &TIMESTAMPS {
for &sig_valid in &[true, false] {
actions.push(GatewayAction::SignedRequest {
signer, nonce, timestamp: ts, sig_valid });
}
}
}
}
// Same cross-product for Authorize and VerifySignature...
for &requester in &KEYS {
for &target in &KEYS {
actions.push(GatewayAction::Grant { requester, target });
}
}
for &requester in &KEYS {
for &target in &KEYS {
actions.push(GatewayAction::Revoke { requester, target });
}
}
actions.push(GatewayAction::GcTick);
actions.push(GatewayAction::AdvanceClock);
}
6c. Mirror Functions: Production Logic with Bounded Types
Each mirror function has the SAME control-flow branches as production code, operating on u8 types instead of NodeId/[u8; 16]/u64.
is_authorized — mirrors check_node (gateway_model_check.rs:92-94):
fn is_authorized(key: u8, acl: &[u8]) -> bool {
key == OWNER || acl.contains(&key)
}
check_signed_request_model — mirrors the 4-step pipeline (gateway_model_check.rs:124-159):
fn check_signed_request_model(
state: &mut GatewayState, signer: u8, nonce: u8,
timestamp: u8, sig_valid: bool,
) -> CheckResult {
// 1. Signature
if !sig_valid { return CheckResult::DeniedBadSig; }
// 2. Timestamp freshness: |now - ts| <= WINDOW
let diff = if state.now >= timestamp { state.now - timestamp }
else { timestamp - state.now };
if diff > WINDOW { return CheckResult::DeniedExpired; }
// 3. Nonce uniqueness (consumed before ACL — matches production)
let nonce_entry = (nonce, timestamp);
if state.seen_nonces.contains(&nonce_entry) {
return CheckResult::DeniedReplay;
}
sorted_insert(&mut state.seen_nonces, nonce_entry);
// 4. ACL check
if is_authorized(signer, &state.acl) {
CheckResult::Allowed
} else {
CheckResult::DeniedNotAuthorized
}
}
check_signature_only_model — steps 1–3 only (gateway_model_check.rs:164-193):
fn check_signature_only_model(
state: &mut GatewayState, nonce: u8, timestamp: u8, sig_valid: bool,
) -> CheckResult {
if !sig_valid { return CheckResult::DeniedBadSig; }
let diff = if state.now >= timestamp { state.now - timestamp }
else { timestamp - state.now };
if diff > WINDOW { return CheckResult::DeniedExpired; }
let nonce_entry = (nonce, timestamp);
if state.seen_nonces.contains(&nonce_entry) {
return CheckResult::DeniedReplay;
}
sorted_insert(&mut state.seen_nonces, nonce_entry);
CheckResult::Allowed
}
grant_model, revoke_model, gc_nonces_model (gateway_model_check.rs:196-231):
fn grant_model(state: &mut GatewayState, requester: u8, target: u8) {
if requester != OWNER { return; } // Owner guard
if target == OWNER { return; } // Self-grant no-op
sorted_insert(&mut state.acl, target);
}
fn revoke_model(state: &mut GatewayState, requester: u8, target: u8) {
if requester != OWNER { return; } // Owner guard
if target == OWNER { return; } // Owner-revoke no-op
sorted_remove(&mut state.acl, &target);
}
fn gc_nonces_model(state: &mut GatewayState) {
state.seen_nonces.retain(|&(_, ts)| {
let diff = if state.now >= ts { state.now - ts }
else { ts - state.now };
diff <= WINDOW
});
}
6d. The Dual-Rail S7 Check
This is the most important design decision in Phase 3. The naive approach: "if the mirror says Allowed, set has_dispatched = true." But this makes S7 tautological — it would pass even if the mirror were wrong.
The dual-rail approach uses TWO INDEPENDENT functions:
check_signed_request_model()— the mirror of production logic. Decides whether to dispatch.is_authorized()— a simple, obviously-correct predicate. Used ONLY in the S7 check.
The SignedRequest arm of next_state (gateway_model_check.rs:326-341):
GatewayAction::SignedRequest { signer, nonce, timestamp, sig_valid } => {
let result =
check_signed_request_model(&mut next, signer, nonce, timestamp, sig_valid);
if result == CheckResult::Allowed {
// Dual-rail S7 check: independently verify the signer IS authorized
// using the PRE-transition state (before nonce insertion)
if !is_authorized(signer, &state.acl) {
next.s7_violated = true;
}
next.has_dispatched = true;
}
}
Why this works: if the mirror has a bug (e.g., skips the ACL check), the independent is_authorized catches the discrepancy. If is_authorized has a bug, S7 could have a false negative — but is_authorized is 1 line (key == OWNER || acl.contains(&key)), trivially auditable.
The violation flag is MONOTONIC: once set, never cleared. This means S7 catches even transient violations in multi-step paths.
6e. Properties and Liveness Canaries
The full properties() function (gateway_model_check.rs:403-428):
fn properties(&self) -> Vec<Property<Self>> {
vec![
// S7: No unauthorized dispatch — the critical safety property.
Property::<Self>::always("S7: no unauthorized dispatch", |_, state| {
!state.s7_violated
}),
// S6-gw: Owner is always authorized (never removed from implicit access).
Property::<Self>::always("S6-gw: owner always authorized", |_, state| {
is_authorized(OWNER, &state.acl)
}),
// L3: Authorized dispatch is reachable (canary — model isn't vacuously safe).
Property::<Self>::sometimes(
"L3: authorized dispatch reachable",
|_, state| state.has_dispatched && !state.s7_violated,
),
// L4: A granted (non-owner) key can dispatch.
Property::<Self>::sometimes("L4: granted key can dispatch", |_, state| {
!state.acl.is_empty() && state.has_dispatched
}),
// L5: Nonce reuse after GC is reachable (GC actually enables re-dispatch).
Property::<Self>::sometimes(
"L5: dispatch with empty nonce table reachable",
|_, state| state.has_dispatched && state.seen_nonces.is_empty(),
),
]
}
- S7 (always):
!state.s7_violated— the critical safety property. Must hold in every reachable state. - S6-gw (always):
is_authorized(OWNER, &state.acl)— owner can never be removed from implicit access, verified at the gateway level (not just engine level). - L3 (sometimes):
state.has_dispatched && !state.s7_violated— there EXISTS a reachable state where authorized dispatch happened. If this fails, the model is too restrictive (nothing ever dispatches), which would make S7 vacuously true. Without L3, S7 could pass by being meaningless. - L4 (sometimes):
!state.acl.is_empty() && state.has_dispatched— a non-owner key was granted AND dispatch happened. Proves the grant→dispatch path works. - L5 (sometimes):
state.has_dispatched && state.seen_nonces.is_empty()— dispatch occurred with an empty nonce table. This can only happen after GC clears all nonces. Proves the GC→nonce-reuse→dispatch path is reachable.
"Canary" means: if any liveness property fails, the safety property is suspect because the model may not be exploring the interesting states.
6f. State Pruning and Exploration
State-space reduction in next_state (gateway_model_check.rs:385-401):
GatewayAction::AdvanceClock => {
if next.now < *TIMESTAMPS.last().unwrap() {
next.now += 1;
} else {
return None; // no-op, prune
}
}
// ... after the match:
// Prune: if state didn't change, no need to explore further
if next == *state {
return None;
}
Some(next)
next_state returns None (no new state) in two cases: (a) action produced no state change (next == *state), (b) clock already at maximum. This prunes the search tree significantly.
Stateright runs DFS with hash-based state deduplication. Each unique state is explored exactly once regardless of how many paths reach it.
The test function (gateway_model_check.rs:433-455):
#[test]
fn gateway_dispatch_model_check() {
let result = GatewayModel
.checker()
.spawn_dfs()
.join();
let unique_states = result.unique_state_count();
println!("Stateright: explored {} unique states, max depth {}",
unique_states, result.max_depth());
result.assert_properties();
// Sanity: the model actually explored a meaningful state space.
assert!(unique_states > 100,
"Model explored too few states ({unique_states}); check action generation");
}
The sanity check unique_states > 100 ensures the model isn't collapsing to a trivial set.
Edge cases covered by exhaustive exploration:
- Grant→Revoke→Request (stale ACL after revoke)
- Nonce reuse after GC (Request→AdvanceClock×2→GcTick→Request succeeds)
- Authorize consumes nonce (Authorize→SignedRequest gets ReplayDetected)
- VerifySignature bypasses ACL but never dispatches
- Non-owner grant is no-op
7. Mutation Sensitivity
Tests are only trustworthy if known-bad code changes cause failures. Mutation testing systematically introduces small code changes and verifies that the test suite catches each one. If a mutation survives (tests still pass), there's a gap in coverage.
Phase 1 has a manual mutation catalog — 5 specific mutations, each targeting a specific property. These were verified during Phase 1 development:
| # | Mutation | Property Violated |
|---|---|---|
| 1 | Remove owner check from check_node (delete *node_id == self.acl.owner || at line 212) |
S6: "owner lost access" |
| 2 | Remove owner-revoke guard (delete if key != self.acl.owner at line 299) |
S6: Grant+Revoke sequence removes owner from authorized_keys |
| 3 | Change > self.timestamp_window to >= self.timestamp_window at line 261 |
S3: boundary requests at diff=300 rejected by engine but expected to pass |
| 4 | Remove nonce check (delete lines 266-268) | S4: replayed nonces accepted |
| 5 | Remove ACL check from grant (delete lines 278-280) |
S5: "non-owner grant succeeded" |
Phase 2 (Kani) is inherently mutation-sensitive: any change to the mirror's control flow that differs from the assertion's specification produces a symbolic counterexample. Kani doesn't just "fail to find a proof" — it produces a concrete input that violates the assertion.
Phase 3's dual-rail design: corrupting check_signed_request_model (e.g., removing the ACL check) triggers S7 because is_authorized independently catches it. Corrupting is_authorized would hide bugs, but it's a 1-line function.
8. Bug Found and Fixed
The Phase 1 state machine discovered that grant(owner, owner) added the owner to authorized_keys. Since revoke(owner, owner) is a no-op (owner's implicit access cannot be removed), the owner would get "stuck" in the explicit set with no way to remove them.
This is a correctness bug, not a security bug — the owner retains access regardless. But it violates the design invariant that the owner's access is purely implicit.
The bug was caught because the reference model's Grant transition doesn't add the owner to the authorized set, but the engine was adding them. The invariant check (S1: reference and SUT agree on every key) caught the disagreement.
Fix — 2-line guard in grant() at auth.rs:281-283:
pub fn grant(&mut self, requester: &NodeId, key: NodeId, label: Option<String>) -> Result<(), DeniedReason> {
if *requester != self.acl.owner {
return Err(DeniedReason::NotAuthorized);
}
if key == self.acl.owner {
return Ok(()); // ← THE FIX: owner has implicit access, no-op
}
self.acl.authorized_keys.insert(key);
// ...
}
9. Supporting Test Coverage
These aren't formal verification, but they provide concrete coverage for specific scenarios.
12 scenario tests (tests/auth_scenario_tests.rs): owner always allowed, unknown key denied, grant/revoke lifecycle, non-owner cannot grant, non-owner cannot revoke, revoking owner is no-op, signed request happy path, tampered signature rejected (S2), stale timestamp rejected, replayed nonce rejected, nonce GC frees old nonces, unauthorized key with valid signature denied. The tampered signature test is the primary S2 coverage alongside Kani.
4 actor-level tests (tests/gateway_tests.rs): authorized signed GET flows through to datastore (returns NotFound, not Denied), unauthorized signed GET returns Denied(NotAuthorized), CheckConnection allows owner, CheckConnection denies stranger. These exercise the real GatewayActor with the real swactor runtime — the concrete integration tests that complement Phase 3's model check.
10. Trust Argument and Boundaries
The Layered Coverage Argument
| Technique | Coverage Type | Scope | Crypto | Collections |
|---|---|---|---|---|
| proptest (Phase 1) | Randomized, high-confidence | Function level | Real ed25519 | Real HashMap/HashSet |
| Kani (Phase 2) | Exhaustive within bounds | Function level | Stubbed (bool) |
Bounded arrays |
| Stateright (Phase 3) | Exhaustive over orderings | Actor (dispatch) level | Stubbed (bool) |
Sorted Vec |
Why the Three Phases Are Complementary, Not Redundant
- Proptest uses real crypto but is randomized — might miss rare cases.
- Kani is exhaustive but stubs crypto and uses bounded collections — might miss
HashSet-specific bugs. - Stateright is exhaustive over orderings but uses bounded parameters — might miss bugs that only manifest with many keys/nonces.
Together: every axis is covered by at least one technique.
| Axis | proptest | Kani | Stateright |
|---|---|---|---|
| Real crypto | Yes | No | No |
| All inputs | No | Yes (within bounds) | Yes (within bounds) |
| All message orderings | No | No | Yes |
| Function correctness | Yes | Yes | No (mirrors) |
| Dispatch correctness | No | No | Yes |
What Is Explicitly NOT Verified
- Network/transport layer (TLS, iroh connections)
- Actor runtime correctness (swactor's message delivery guarantees)
- Ed25519 implementation (
distribution::crypto) - Persistence (ACL load/save to disk)
- UI/API layer above
GatewayActor - Concurrency bugs within the actor runtime
- Mirror faithfulness — the correspondence between mirror functions and production code is a manual property that the reader must verify by comparing the code excerpts in sections 5b, 5c, 6c, and 6d against the production code in section 3
11. Running the Suite
# Phase 1: proptest state machine (~70-80s, real ed25519 crypto)
cargo test -p swactor-datastore --test auth_state_machine
# Phase 2: Kani bounded proofs (requires cargo-kani)
cargo xtask test kani
# Phase 3: Stateright model check (<1s)
cargo xtask test stateright
# Scenario tests
cargo test -p swactor-datastore --test auth_scenario_tests
# Everything except Kani (Kani requires separate toolchain)
cargo test -p swactor-datastore
12. Files Changed
| File | Change |
|---|---|
src/auth.rs |
Owner self-grant guard (2 lines) |
src/kani_auth.rs |
New — bounded mirror + 5 Kani proof harnesses |
src/lib.rs |
#[cfg(kani)] mod kani_auth; |
tests/auth_state_machine.rs |
New — proptest state machine (485 lines) |
tests/auth_scenario_tests.rs |
New — 12 scenario tests |
tests/gateway_model_check.rs |
New — Stateright model check (456 lines) |
Cargo.toml |
Added dev-deps: proptest, proptest-state-machine, stateright |
xtask/src/main.rs |
Added kani and stateright test groups |