Auth Platform PoC with Formal Verification
CoRISE contributed to an authentication and authorization platform PoC that combined Rust implementation with formal verification and model checking. The work used existing formal-verification assets alongside Kani at the implementation level and Tamarin at the protocol level to examine properties at different layers.
- Domain
- Product Engineering / Security & Resilience
- Type
- Proof of Concept
- Techniques
- Formal verification / Model checking / Protocol verification
- Implementation
- Rust
- Tools and existing assets
- Kani / Tamarin / Project Everest
Background
Working behavior is one part of the question.
Authentication and authorization require considering which properties hold under unexpected inputs, complex state transitions and adversarial behavior. Alongside conventional tests, this PoC examined four questions.
- What assumptions are being made?
- Which inputs and states are explored?
- Which security properties should hold?
- Where does each result correspond to the implementation?
CoRISE’s role
Connecting technical direction to implementation and verification.
↔ Scroll horizontally to see the full diagram.
View diagram as text
Kani examines the central Rust implementation through a harness. Tamarin examines a separately authored protocol model. The dashed connection between code and model denotes correspondence to examine, not automatic translation or a proven refinement.
01
Rust implementation
Contributed to platform functionality in Rust, making code concrete with attention to the boundaries and state transitions under examination.
02
Model checking with Kani
Contributed to checking Rust properties through harnesses that define inputs, assumptions, exploration bounds and conditions to examine.
03
Protocol verification with Tamarin
Contributed to examining symbolic models of message exchange, state transitions and security properties, including adversarial behavior.
Verification layers
Different verification layers, explicit assumptions.
Kani examines Rust code; Tamarin examines a symbolic protocol model. Each result is interpreted with its subject, assumptions and scope. The following diagram is a conceptual view of these relationships.
↔ Scroll horizontally to see the full diagram.
View diagram as text
Existing verified assets are integrated into Rust. Kani checks code reachable from a harness; Tamarin verifies a separately authored symbolic model. Model-to-code correspondence remains a relationship to examine. Results are collected with assumptions and scope, informing implementation revisions. Boxes distinguish verification subjects, not system trust boundaries.
Existing verified assets
Use existing verification work within its assurance scope.
This PoC used outputs from Project Everest. Integrating existing formal-verification assets requires distinguishing the guarantees of each asset from the properties that the consuming system must establish.
What the asset guarantees
Identify the specific properties established by the existing work.
Assumptions it depends on
Check the conditions required for those guarantees to apply.
Integration boundaries
Distinguish the asset’s scope from the code that consumes it.
Remaining responsibility
Identify properties the integrating system must still establish.
05 — Implementation-level checking
Examine Rust properties under harness-defined conditions.
Kani analyzes Rust code through a verification harness. The harness provides an entry point into reachable code, with explicit assumptions and bounds for the analysis.
Verification harnesses
Define the entry point and the operations to examine.
Inputs and exploration bounds
Use nondeterministic inputs and set analysis bounds, such as loop-unwinding limits, where required.
Explicit assumptions
State constraints in the harness rather than leaving preconditions implicit.
Selected properties
Use assertions and safety checks to specify what is examined.
Interpreting results
Read a successful result together with analysis completion, assumptions and configured bounds. It does not establish correctness of the entire application.
↔ Scroll horizontally to see the full diagram.
View diagram as text
A harness defines inputs and assumptions for reachable Rust code. Analysis bounds and properties define the check. Exhaustive checking within the configured scope is distinct from proving the entire application.
06 — Protocol-level verification
Examine protocol behavior with an explicit adversary model.
Tamarin works on a symbolic protocol model rather than Rust code itself. It considers participant communication, state transitions and the adversary capabilities defined in the model.
Symbolic protocol model
An abstraction of protocol logic, rather than a trace of running code.
Message exchange and state transitions
How participants communicate and how their state evolves.
Adversary capabilities and assumptions
Include the modeled ability to intercept or alter messages in the analysis.
Security properties
Express properties such as secrecy or event correspondence. These examples do not claim completed proofs in this PoC.
Model–implementation correspondence
Examine how model states and actions relate to the implementation. That correspondence is not automatically proven.
↔ Scroll horizontally to see the full diagram.
View diagram as text
A symbolic exchange between parties A and B includes modeled adversary capabilities. Properties are checked against that model. Secrecy and event correspondence are illustrative properties, not claims of completed PoC proofs. Correspondence to the Rust implementation is examined separately.
Development loop
Iterate across design, implementation and verification.
Implementation and verification proceeded together, connecting the properties under examination to the code. The diagram illustrates a development approach in which assumptions and counterexamples inform revisions.
↔ Scroll horizontally to see the full diagram.
View diagram as text
Define properties, implement, build a model or harness, verify, inspect assumptions and counterexamples, revise design or implementation, then return to property definition. This is a conceptual iterative development loop.
Capabilities applied
Connect formal methods to software development.
- 01Rust implementation
- 02Formal-method-aware development
- 03Model checking with Kani
- 04Symbolic protocol verification with Tamarin
- 05Use of existing formally verified assets
- 06Explicit verification and assurance scope
- 07Connecting assumptions to evidence
- 08Implementation and verification feedback
Assurance boundary
Distinguish verified properties from what remains outside scope.
This case does not mean that the security of the entire authentication and authorization platform has been formally proven.
Results depend on the implementation or model examined, assumptions, exploration bounds and adversary model. Work at the PoC stage is also distinct from assurance of reliability in production.
Making the limits of a result explicit is part of engineering high-assurance systems, alongside explaining what has been established.