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>
484 lines
18 KiB
Rust
484 lines
18 KiB
Rust
//! Proptest state-machine verification of AuthzEngine.
|
||
//!
|
||
//! Drives the auth engine through random sequences of grant/revoke/check/sign
|
||
//! operations and verifies safety + liveness properties against a reference model.
|
||
//!
|
||
//! Properties verified:
|
||
//! S1 check_node(n) = Allowed ⟹ n = owner ∨ n ∈ authorized_keys
|
||
//! S2 Invalid signature → Denied(InvalidSignature)
|
||
//! S3 Expired timestamp → Denied(RequestExpired)
|
||
//! S4 Replayed nonce → Denied(ReplayDetected)
|
||
//! S5 Non-owner cannot mutate ACL
|
||
//! S6 Owner access irremovable over arbitrary op sequences
|
||
//! L1 Grant leads to access until revoke
|
||
//! L2 GC enables nonce reuse after window
|
||
|
||
use std::collections::{HashMap, HashSet};
|
||
|
||
use proptest::prelude::*;
|
||
use proptest_state_machine::{prop_state_machine, ReferenceStateMachine, StateMachineTest};
|
||
|
||
use distribution::crypto::Keypair;
|
||
use swactor_datastore::auth::{
|
||
sign_request, AccessControlList, AuthzEngine, AuthzResult, DatastoreAction, DeniedReason,
|
||
SignedRequestPayload,
|
||
};
|
||
|
||
const NUM_KEYS: usize = 4; // index 0 = owner, 1..3 = clients
|
||
|
||
// ─── Reference Model ────────────────────────────────────────────────────────
|
||
|
||
#[derive(Clone, Debug)]
|
||
struct RefAuthModel {
|
||
owner_idx: usize,
|
||
authorized: HashSet<usize>,
|
||
used_nonces: HashSet<[u8; 16]>,
|
||
/// Maps nonce → timestamp it was recorded at
|
||
nonce_timestamps: HashMap<[u8; 16], u64>,
|
||
clock: u64,
|
||
/// Track the last nonce used per signer for the reuse_nonce transition
|
||
last_nonce: Option<[u8; 16]>,
|
||
}
|
||
|
||
// ─── Transitions ────────────────────────────────────────────────────────────
|
||
|
||
#[derive(Clone, Debug)]
|
||
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,
|
||
}
|
||
|
||
// ─── Reference State Machine ────────────────────────────────────────────────
|
||
|
||
struct AuthModel;
|
||
|
||
impl ReferenceStateMachine for AuthModel {
|
||
type State = RefAuthModel;
|
||
type Transition = AuthOp;
|
||
|
||
fn init_state() -> BoxedStrategy<Self::State> {
|
||
Just(RefAuthModel {
|
||
owner_idx: 0,
|
||
authorized: HashSet::new(),
|
||
used_nonces: HashSet::new(),
|
||
nonce_timestamps: HashMap::new(),
|
||
clock: 1_000_000,
|
||
last_nonce: None,
|
||
})
|
||
.boxed()
|
||
}
|
||
|
||
fn transitions(state: &Self::State) -> BoxedStrategy<Self::Transition> {
|
||
let has_last_nonce = state.last_nonce.is_some();
|
||
|
||
prop_oneof![
|
||
// Grant: any requester, any target
|
||
3 => (0..NUM_KEYS, 0..NUM_KEYS).prop_map(|(r, t)| AuthOp::Grant {
|
||
requester_idx: r,
|
||
target_idx: t,
|
||
}),
|
||
// Revoke: any requester, any target
|
||
3 => (0..NUM_KEYS, 0..NUM_KEYS).prop_map(|(r, t)| AuthOp::Revoke {
|
||
requester_idx: r,
|
||
target_idx: t,
|
||
}),
|
||
// CheckNode: any key
|
||
3 => (0..NUM_KEYS).prop_map(|k| AuthOp::CheckNode { key_idx: k }),
|
||
// SignedRequest: fresh nonce, fresh or stale timestamp
|
||
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,
|
||
}),
|
||
// SignedRequest: reuse nonce (only when we have one)
|
||
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,
|
||
}),
|
||
// AdvanceClock: 0..600
|
||
2 => (0u64..600).prop_map(|d| AuthOp::AdvanceClock { delta: d }),
|
||
// GcNonces
|
||
1 => Just(AuthOp::GcNonces),
|
||
]
|
||
.boxed()
|
||
}
|
||
|
||
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
|
||
}
|
||
|
||
fn preconditions(_state: &Self::State, _transition: &Self::Transition) -> bool {
|
||
true
|
||
}
|
||
}
|
||
|
||
// ─── System Under Test ──────────────────────────────────────────────────────
|
||
|
||
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>,
|
||
}
|
||
|
||
struct AuthTest;
|
||
|
||
impl StateMachineTest for AuthTest {
|
||
type SystemUnderTest = SutAuth;
|
||
type Reference = AuthModel;
|
||
|
||
fn init_test(_ref_state: &RefAuthModel) -> Self::SystemUnderTest {
|
||
let keys: Vec<Keypair> = (0..NUM_KEYS).map(|_| Keypair::generate()).collect();
|
||
let acl = AccessControlList {
|
||
owner: keys[0].node_id(),
|
||
authorized_keys: HashSet::new(),
|
||
key_labels: HashMap::new(),
|
||
};
|
||
SutAuth {
|
||
engine: AuthzEngine::new(acl),
|
||
keys,
|
||
clock: 1_000_000,
|
||
last_nonce: None,
|
||
known_nonces: HashSet::new(),
|
||
nonce_timestamps: HashMap::new(),
|
||
authorized_indices: HashSet::new(),
|
||
}
|
||
}
|
||
|
||
fn apply(
|
||
mut sut: Self::SystemUnderTest,
|
||
_ref_state: &RefAuthModel,
|
||
transition: AuthOp,
|
||
) -> Self::SystemUnderTest {
|
||
match transition {
|
||
AuthOp::Grant {
|
||
requester_idx,
|
||
target_idx,
|
||
} => {
|
||
let owner_idx = 0; // owner is always key index 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);
|
||
}
|
||
}
|
||
}
|
||
AuthOp::CheckNode { key_idx } => {
|
||
let node = sut.keys[key_idx].node_id();
|
||
let result = sut.engine.check_node(&node);
|
||
let expected_allowed =
|
||
key_idx == 0 || sut.authorized_indices.contains(&key_idx);
|
||
|
||
// S1: check_node matches reference model
|
||
if expected_allowed {
|
||
assert_eq!(
|
||
result,
|
||
AuthzResult::Allowed,
|
||
"S1 violated: key_idx={key_idx} should be allowed"
|
||
);
|
||
} else {
|
||
assert_eq!(
|
||
result,
|
||
AuthzResult::Denied(DeniedReason::NotAuthorized),
|
||
"S1 violated: key_idx={key_idx} should be denied"
|
||
);
|
||
}
|
||
}
|
||
AuthOp::SignedRequest {
|
||
signer_idx,
|
||
fresh_timestamp,
|
||
reuse_nonce,
|
||
nonce_bytes,
|
||
} => {
|
||
let nonce = if reuse_nonce {
|
||
sut.last_nonce.unwrap_or(nonce_bytes)
|
||
} else {
|
||
nonce_bytes
|
||
};
|
||
|
||
let ts = if fresh_timestamp {
|
||
sut.clock
|
||
} else {
|
||
sut.clock.saturating_sub(400)
|
||
};
|
||
|
||
// Compute expected result BEFORE the engine call mutates state.
|
||
// We use sut.known_nonces (pre-transition) instead of ref_state
|
||
// (post-transition) to avoid the off-by-one on nonce insertion.
|
||
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 {
|
||
// S3: Expired timestamp
|
||
AuthzResult::Denied(DeniedReason::RequestExpired)
|
||
} else if is_replay {
|
||
// S4: Replayed nonce
|
||
AuthzResult::Denied(DeniedReason::ReplayDetected)
|
||
} else if is_authorized {
|
||
AuthzResult::Allowed
|
||
} else {
|
||
// S1: Not authorized (nonce still consumed at step 3)
|
||
AuthzResult::Denied(DeniedReason::NotAuthorized)
|
||
};
|
||
|
||
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}"
|
||
);
|
||
|
||
// Update our nonce tracker to mirror what the engine did
|
||
if diff <= 300 && !is_replay {
|
||
sut.known_nonces.insert(nonce);
|
||
sut.nonce_timestamps.insert(nonce, ts);
|
||
}
|
||
|
||
sut.last_nonce = Some(nonce);
|
||
}
|
||
AuthOp::AdvanceClock { delta } => {
|
||
sut.clock += delta;
|
||
}
|
||
AuthOp::GcNonces => {
|
||
sut.engine.gc_nonces(sut.clock);
|
||
// Mirror GC in our nonce tracker
|
||
let now = sut.clock;
|
||
sut.known_nonces.retain(|nonce| {
|
||
if let Some(&ts) = sut.nonce_timestamps.get(nonce) {
|
||
let diff = if now >= ts { now - ts } else { ts - now };
|
||
diff <= 300
|
||
} else {
|
||
false
|
||
}
|
||
});
|
||
sut.nonce_timestamps.retain(|_, ts| {
|
||
let diff = if now >= *ts { now - *ts } else { *ts - now };
|
||
diff <= 300
|
||
});
|
||
}
|
||
}
|
||
sut
|
||
}
|
||
|
||
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"
|
||
);
|
||
}
|
||
|
||
// L2 (partial): After GC, nonce count in SUT should match reference model
|
||
// The reference model tracks which nonces should survive GC.
|
||
// Full L2 is exercised by the SignedRequest transition postconditions —
|
||
// a nonce reuse after GC + clock advance should succeed when the
|
||
// reference model says it's been freed.
|
||
}
|
||
}
|
||
|
||
// ─── Launch ─────────────────────────────────────────────────────────────────
|
||
|
||
prop_state_machine! {
|
||
#![proptest_config(proptest::test_runner::Config {
|
||
cases: 512,
|
||
max_shrink_iters: 1000,
|
||
.. proptest::test_runner::Config::default()
|
||
})]
|
||
|
||
/// Given random sequences of grant/revoke/check/sign/clock/gc operations,
|
||
/// the AuthzEngine always agrees with the reference model on authorization
|
||
/// decisions and maintains all safety and liveness properties.
|
||
#[test]
|
||
fn auth_engine_state_machine(sequential 1..100 => AuthTest);
|
||
}
|