Model and Verify a Security Invariant

Protection need

Choose one high-impact claim that ordinary examples do not establish. For example: after administrative authority is revoked, no new policy change is accepted through any normal, cached, delegated, emergency, or restored path. Name the protected resource, adverse consequence, operating environment, and maximum allowed delay.

Keep the question bounded. Formal analysis is useful when a small state machine controls a large consequence, when concurrent transitions interact, or when review cannot enumerate every state sequence.

Security objectives and requirements

Define subjects, credentials, resources, actions, policy, state variables, trusted inputs, channels, clocks or epochs, and transitions. Include issue, delegate, approve, deny, revoke, cache, expire, retry, race, partition, reconcile, restore, and recover where each can affect the property.

Write the invariant in precise language before tool syntax. State safety properties that must never fail and liveness properties that must eventually hold. Separate the model's assumptions from the invariant. A model that assumes authentic current group data cannot prove that the identity provider supplies it.

Select the method. Manual state tables and attack trees can expose missing transitions. Model checking can search bounded interleavings and produce counterexamples. Theorem proving can establish a property for the modeled rules. Symbolic protocol analysis can examine message and attacker knowledge. Use the smallest method that provides the required confidence.

Security invariants and evidence

Map every modeled element to a real owner and interface. Connect the result to source, policy compiler, configuration, storage, clock, network channel, deployment, enforcement point, direct-path control, and application state transition.

Create tests from counterexamples and transition boundaries. Exercise wrong subject, wrong object, stale state, replay, concurrent revoke and use, partition, old replica, backup restore, and recovery. Record the exact model and implementation versions. Use runtime evidence to confirm that deployed transitions and assumptions still match.

Failure cases

• The property uses authorized without defining subject, resource, action, context, and policy.
• The model omits administration, emergency access, cache, retry, partition, rollback, or restore.
• A proof about policy evaluation is presented as proof of complete mediation.
• Real implementation behavior has no trace to a modeled transition.
• The team changes the policy language, compiler, storage, or distribution path without invalidating the result.
• Tests repeat the happy path and never exercise a counterexample or assumption failure.

Design tradeoffs and residual risk

More detail improves fidelity and can make analysis intractable. Abstraction makes proof possible and can remove the failure that matters. Stronger methods cost specialist time and can produce artifacts that operators cannot maintain.

Residual risk includes a wrong protection need, omitted path, false identity or context input, implementation defect below the model, tool error, compromised deployment, side channel, and harmful application behavior outside the modeled action.

Pomerium boundary

Pomerium behavior can participate in an invariant for configured routes and policy. The full model must include identity data, direct upstream reachability, application authorization, control-plane access, evidence, and recovery. Operators own the correspondence between the model and their deployed system.

Exercise

Model a route policy with a subject grant, cached decision, five-minute expiry, emergency grant, revocation, two enforcement replicas, a network partition, and backup restore. State the maximum last-accept time after ordinary and emergency revocation.

Find or construct one counterexample. Change the design to remove or bound it. Turn the counterexample into a deployed negative test and identify one assumption that the test still cannot establish.

Evaluation checklist

• Is the invariant precise about subject, resource, action, state, environment, and time bound?
• Does the model include every transition and failure that can change the result?
• Are assumptions separate, owned, and tested where possible?
• Can every model element be traced to current implementation and deployment evidence?
• Does the conclusion state exactly what was established and what remains outside the model?