soma.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.

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.

Generated from soma describe on this file.

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

Run on a fresh copy of the program at build time; the outputs are pasted unedited.

$ 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

Builtins used

get_status, map, transition

Source file: /corpus/devops/secret_rotation.cell · examples/corpus/devops/secret_rotation.cell