Secret rotation — a revoked credential never logs in again
In 2016, attackers found Uber's AWS keys sitting in a private GitHub repo. The keys were long-lived — never rotated — and unlocked data on 57 million riders and drivers. The pattern repeats everywhere: a credential leaks, someone "disables" it in a dashboard, and months later a recovery script or a confused admin re-enables it. Here the credential lifecycle is a machine where `revoked` and `retired` are TERMINAL — `soma verify` proves no handler, script, or 3 a.m. admin can resurrect a dead key. Authentication consults the machine, so a revoked key fails closed. Key age sits behind a memory invariant: a credential older than the 90-day rotation policy cannot even be recorded, which makes "we forgot to rotate" a write error.
A Soma program from the devops part of the verified corpus: 115 lines, cells SecretVault, VaultTests. It passes soma check with soma 3.2.4.
How it is built
The cell SecretVault declares 6 signals in its face: mint(key: String) -> Map, begin_rotation(key: String) -> Map, retire(key: String) -> Map, revoke(key: String) -> Map, authenticate(key: String) -> Map and record_age(key: String, days: Int) -> Map; keeps 1 memory slot: age_days (Map<String, Int>, persistent and consistent) under the invariant age_days >= 0 && age_days <= 90. Its state machine credential starts in minted and allows 5 transitions: minted -> active, active -> rotating, rotating -> retired, active -> revoked and rotating -> revoked. retired and revoked are terminal. Handlers: mint (line 45), begin_rotation (line 52), retire (line 58), revoke (line 64), authenticate (line 71) and record_age (line 79).
The file also holds 1 test cell (VaultTests) with 16 assertions, run by soma test.
The source
secret_rotation.cell
// ============================================================================
// SECRET ROTATION — a revoked credential never logs in again
// ============================================================================
//
// In 2016, attackers found Uber's AWS keys sitting in a private GitHub
// repo. The keys were long-lived — never rotated — and unlocked data on
// 57 million riders and drivers. The pattern repeats everywhere: a
// credential leaks, someone "disables" it in a dashboard, and months
// later a recovery script or a confused admin re-enables it.
//
// Here the credential lifecycle is a machine where `revoked` and
// `retired` are TERMINAL — `soma verify` proves no handler, script, or
// 3 a.m. admin can resurrect a dead key. Authentication consults the
// machine, so a revoked key fails closed. Key age sits behind a memory
// invariant: a credential older than the 90-day rotation policy cannot
// even be recorded, which makes "we forgot to rotate" a write error.
// ============================================================================
cell SecretVault {
face {
signal mint(key: String) -> Map
signal begin_rotation(key: String) -> Map
signal retire(key: String) -> Map
signal revoke(key: String) -> Map
signal authenticate(key: String) -> Map
signal record_age(key: String, days: Int) -> Map
}
memory {
age_days: Map<String, Int> [persistent, consistent]
invariant age_days >= 0 && age_days <= 90
}
// `revoked` (compromise) and `retired` (rotated out) have no exit.
// An active key may rotate or be revoked; nothing comes back.
state credential {
initial: minted
minted -> active
active -> rotating
rotating -> retired
active -> revoked
rotating -> revoked
}
on mint(key: String) {
let r = try { transition(key, "active") }
if r.error != () { return map("ok", false, "reason", "{r.error}") }
age_days.set(key, 0)
return map("ok", true, "state", "active")
}
on begin_rotation(key: String) {
let r = try { transition(key, "rotating") }
if r.error != () { return map("ok", false, "reason", "{r.error}") }
return map("ok", true, "state", "rotating")
}
on retire(key: String) {
let r = try { transition(key, "retired") }
if r.error != () { return map("ok", false, "reason", "{r.error}") }
return map("ok", true, "state", "retired")
}
on revoke(key: String) {
let r = try { transition(key, "revoked") }
if r.error != () { return map("ok", false, "reason", "{r.error}") }
return map("ok", true, "state", "revoked")
}
// fails closed: only `active` and `rotating` (overlap window) serve
on authenticate(key: String) {
let s = get_status(key)
if s == "active" || s == "rotating" {
return map("ok", true, "state", s)
}
return map("ok", false, "reason", "credential is {s}")
}
on record_age(key: String, days: Int) {
let w = try { age_days.set(key, days) }
if w.error != () {
return map("ok", false, "reason", "rotation policy: {w.error}")
}
return map("ok", true, "age", days)
}
}
cell test VaultTests {
rules {
// a leaked key is revoked...
assert mint("AKIA-uber-prod").ok == true
assert authenticate("AKIA-uber-prod").ok == true
assert revoke("AKIA-uber-prod").ok == true
assert authenticate("AKIA-uber-prod").ok == false
// ...and THE RESURRECTION does not exist as an edge
assert_fails transition("AKIA-uber-prod", "active")
assert_fails transition("AKIA-uber-prod", "rotating")
assert_fails transition("AKIA-uber-prod", "minted")
// healthy rotation: overlap window authenticates, retired never
assert mint("AKIA-v2").ok == true
assert begin_rotation("AKIA-v2").ok == true
assert authenticate("AKIA-v2").ok == true
assert retire("AKIA-v2").ok == true
assert authenticate("AKIA-v2").ok == false
assert_fails transition("AKIA-v2", "active")
// the 90-day policy is a wall, not a wiki page
assert record_age("AKIA-v3", 89).ok == true
assert_fails age_days.set("AKIA-v3", 91)
assert_fails age_days.set("AKIA-v3", -1)
}
}What the toolchain says
$ soma check secret_rotation.cell
✓ All checks passed.$ soma test secret_rotation.cell
test VaultTests ...
✓ assert mint("AKIA-uber-prod").ok == true
✓ assert authenticate("AKIA-uber-prod").ok == true
✓ assert revoke("AKIA-uber-prod").ok == true
✓ assert authenticate("AKIA-uber-prod").ok == false
✓ assert_fails transition("AKIA-uber-prod", "active") — raised invalid transition: revoked → active. Current state: 'revoked'. Valid targets: []
✓ assert_fails transition("AKIA-uber-prod", "rotating") — raised invalid transition: revoked → rotating. Current state: 'revoked'. Valid targets: []
✓ assert_fails transition("AKIA-uber-prod", "minted") — raised invalid transition: revoked → minted. Current state: 'revoked'. Valid targets: []
✓ assert mint("AKIA-v2").ok == true
✓ assert begin_rotation("AKIA-v2").ok == true
✓ assert authenticate("AKIA-v2").ok == true
✓ assert retire("AKIA-v2").ok == true
✓ assert authenticate("AKIA-v2").ok == false
✓ assert_fails transition("AKIA-v2", "active") — raised invalid transition: retired → active. Current state: 'retired'. Valid targets: []
✓ assert record_age("AKIA-v3", 89).ok == true
✓ assert_fails age_days.set("AKIA-v3", 91) — raised memory invariant violated on 'age_days': age_days >= 0 && age_days <= 90 — rejected write of 91 (key "AKIA-v3"); the slot is unchanged
✓ assert_fails age_days.set("AKIA-v3", -1) — raised memory invariant violated on 'age_days': age_days >= 0 && age_days <= 90 — rejected write of -1 (key "AKIA-v3"); the slot is unchanged
16 tests: 16 passed, 0 failed$ soma verify secret_rotation.cell
Verifying secret_rotation.cell...
State machine 'credential': 5 states, initial 'minted'
States: [active, minted, retired, revoked, rotating]
✓ 5 states, 5 transitions
✓ all states reachable from 'minted'
✓ terminal states: [retired, revoked]
✓ no deadlocks
✓ liveness: every state can eventually reach a terminal state
✓ think-isolated: CTL safety properties hold regardless of LLM output (4 handlers, 4 literal transitions, 0 dynamic)
✓ termination: all 6 handlers structurally terminate
✓ refinement: handler `mint` ⟶ {active}
✓ refinement: handler `begin_rotation` ⟶ {rotating}
✓ refinement: handler `retire` ⟶ {retired}
✓ refinement: handler `revoke` ⟶ {revoked}
· transition sources: `mint`, `begin_rotation`, `retire`, `revoke` call transition(id, target) without declaring the source — the runtime refuses a move the graph forbids, but the proof does not see where the handler starts; `transition(id, from, to)` names the edge (checked by `soma check`, refused at run time from any other state)
SecretVault/invariants:
✓ invariant age_days >= 0 && age_days <= 90 — writer 'mint' proven (writes 0)
⚠ invariant age_days >= 0 && age_days <= 90 — runtime-checked (computed values): record_age → age_days because `days` is a parameter (narrow it: `require days >= 0 && days <= 90 else …`)
12 passed, 1 warnings, 0 failures
Temporal properties for 'credential':
✓ deadlock_free — no deadlocks in any reachable state
Temporal: 1 passed, 0 failed
VERIFY OK