Document
Threat Model
**Verifiable Semantic Execution Layer (VSEL)**
Verifiable Semantic Execution Layer (VSEL)
1. Scope and Security Objective
VSEL does not aim to prove that execution is correct with respect to a circuit. That bar is too low and already insufficient.
The objective is stronger:
Ensure that every proven execution belongs to the set of valid executions defined by a formally specified system.
This implies resistance against adversaries exploiting:
- semantic gaps between specification and implementation
- inconsistencies across system layers
- underconstrained proof systems
- divergence between real execution and formal semantics
The adversary is not required to break cryptography. They only need to find where the system definition is incomplete or ambiguous.
2. System Boundaries
VSEL consists of the following layers:
- Formal Specification Layer (FSL)
- Semantic Intermediate Representation (SIR)
- Execution Layer (EL)
- Constraint Derivation Layer (CDL)
- Proof Layer (PL)
- Verification Layer (VL)
Security depends on semantic preservation across all layers.
Any divergence between layers is considered a security failure.
3. Assets and Security Properties
3.1 Primary Assets
-
Semantic Correctness All accepted executions must conform to the formal specification.
-
State Integrity System state must remain within the valid state space ( S ).
-
Transition Validity All transitions must belong to the transition relation ( T ).
-
Trace Validity Execution traces must be valid sequences under ( (S, I, T) ).
-
Invariant Preservation Local, global, and temporal invariants must hold at all times.
3.2 Secondary Assets
- Proof integrity
- Consistency between execution and proof
- Integrity of observable outputs
- State reconstructability
4. Adversary Classes
4.1 Malicious Prover
Controls proof generation.
Objectives:
- produce valid proofs for invalid executions
- exploit underconstrained circuits
- manipulate witness data
Capabilities:
- full control over witness inputs
- knowledge of constraint system
- ability to search constraint edge cases
4.2 Malicious Executor
Controls the execution environment.
Objectives:
- produce state transitions outside the formal model
- introduce invalid states
- diverge from specified semantics
Capabilities:
- control over runtime behavior
- manipulation of execution ordering and timing
- modification of internal state
4.3 Specification Manipulator
Targets the system through its specification.
Objectives:
- introduce ambiguity
- omit edge cases
- define incomplete invariants
Capabilities:
- influence over formal definitions
- exploitation of underspecified semantics
This adversary is frequently internal and consistently underestimated.
4.4 Constraint-Level Attacker
Targets the constraint system.
Objectives:
- find executions that satisfy constraints but violate semantics
Capabilities:
- circuit analysis
- underconstraint discovery
- witness manipulation
4.5 Verifier-Limited Adversary
Exploits limitations of the verifier.
Objectives:
- cause acceptance of invalid proofs
- bypass contextual validation
Capabilities:
- interaction with simplified verifiers
- exploitation of incomplete validation logic
4.6 Economic Adversary
Rational, profit-driven attacker.
Objectives:
- exploit inconsistencies for financial gain
- manipulate cross-system composition
Capabilities:
- multi-system interaction
- timing and ordering exploitation
- arbitrage of inconsistencies
5. Attack Surfaces
5.1 Semantic Gap
Mismatch between:
- formal specification
- real execution
- constraint system
Impact:
- invalid execution accepted as valid
5.2 Underconstrained Systems
Constraints fail to fully encode semantics.
Impact:
- multiple valid witnesses for semantically invalid behavior
5.3 State Encoding Mismatch
Mismatch between:
- real state
- encoded state
Impact:
- valid proofs over incorrect state representations
5.4 Trace Incompleteness
Incomplete capture of execution history.
Impact:
- validation of partial behavior only
5.5 Non-Determinism
Execution is not deterministic.
Impact:
- inability to reconstruct or verify traces
- multiple valid outcomes
5.6 Composition Failure
System interactions violate invariants.
Impact:
- locally correct systems produce globally invalid behavior
5.7 Temporal Attacks
Exploitation across time rather than single execution.
Impact:
- invariants violated across sequences, not snapshots
6. Explicit Non-Goals
VSEL does not attempt to address:
- hardware-level faults
- side-channel attacks outside the formal model
- cryptographic breaks of assumed-secure primitives
- behavior not captured in the formal specification
If it is not modeled, it is not protected.
7. Security Assumptions
- cryptographic primitives are secure (classical and post-quantum)
- SIR → constraint transformation is correct
- verifier executes correctly
- formal specification is complete
The last assumption is the weakest and most dangerous.
8. Failure Definitions
A failure occurs if:
- an invalid execution is accepted
- an invalid state is reached
- invariants are violated without detection
- a valid proof represents semantically invalid behavior
9. Defense Strategy
9.1 Semantic Closure
All system behavior must be explicitly defined in the specification.
No implicit behavior is allowed.
9.2 Constraint Completeness
Constraints must be:
- sound (no invalid execution passes)
- complete (all valid executions are representable)
9.3 Trace-Level Verification
Validation must operate over execution traces, not isolated steps.
9.4 Cross-Layer Consistency
All layers must preserve semantic equivalence.
9.5 Adversarial Testing
System must be tested under:
- invalid inputs
- edge-case transitions
- adversarial compositions
10. Residual Risk
Remaining risks include:
- incomplete specification
- incorrect semantic transformation
- emergent behavior under composition
- human error
11. Closing Statement
VSEL assumes a deliberately uncomfortable position:
The primary source of failure is not execution or proof, but the definition of correctness itself.
If correctness is underspecified, the system can be perfectly verified and completely wrong.