Verification walkthrough

Deterministic verification of fail-closed execution enforcement: step-by-step proof that invariants hold without trusting the system.

If I trust the keys, I can verify the enforcement without trusting the system.

Purpose

This walkthrough demonstrates that a third party can verify fail-closed enforcement using only publicly available artifacts—without trusting the system's internal state.

The verifier needs:
1. The specification (INV-1 through INV-6)
2. Cryptographic keys (public keys only)
3. Raw request/response data
4. Audit log export

The verifier does NOT need:
• Access to internal state
• Trust in the Control Plane's honest behavior
• Trust in the Gate's routing decisions

Setup

Preconditions for this walkthrough:

IDENTITY KEYS (public):
• user_identity_key: ed25519/abc123 (registered in identity store)
• control_plane_key: ed25519/cp789 (signs approval envelopes)

SYSTEM COMPONENTS:
• Gate: proxy.example.com:8443
• Control Plane: api.example.com:8080
• Execution Layer: exec.example.com:9000
• Audit Store: audit.example.com:5432

TIMESTAMP REFERENCE:
• Wall clock: 2024-04-11T15:00:00Z
• Acceptance window: 300 seconds (5 minutes)

Step 1: Raw Request

Input data provided to this walkthrough:

{
  "request_id": "req_xyz789",
  "identity": "user_abc123",
  "action": "execute_tool",
  "tool": "database_query",
  "parameters": {
    "query": "SELECT * FROM users WHERE id = 'user_42'",
    "params": ["user_42"]
  },
  "timestamp": 1712841600,
  "nonce": "nonce_abc123def",
  "signature": "MEUCIQ...<base64>"
}

CRITICAL: This is the ONLY input the verifier receives from external observation.

Step 2: Identity Verification

Verifier action: Verify request signature against registered identity key.

CODE:
verify_signature(
  payload = "req_xyz789|user_abc123|execute_tool|...",
  signature = "MEUCIQ...<base64>",
  public_key = identity_store["user_abc123"]
)

RESULT: VALID

OUTPUT:
{
  "identity_verified": true,
  "signer": "user_abc123",
  "timestamp_valid": true,
  "nonce_unused": true
}

If VALID → proceed to policy evaluation.
If INVALID → INV-3 fails. Execution MUST NOT proceed.

Step 3: Policy Evaluation

Verifier does NOT have visibility into Control Plane policy evaluation. This is an external walkthrough—the verifier observes the APPROVAL ENVELOPE returned.

Observation: Approval envelope retrieved from cache or re-request:

{
  "approval_id": "apr_xyz789",
  "identity": "user_abc123",
  "action": "execute_tool",
  "bounds": {
    "tool": "^database_query$",
    "query": "^SELECT.*FROM users WHERE id = .+$",
    "params": "^[a-zA-Z0-9_]+$"
  },
  "timestamp": 1712841600,
  "expires_at": 1712841900,
  "nonce": "nonce_approval_xyz",
  "signature": "MGOEQ...<base64>"
}

VERIFIER CHECK: Control Plane signature valid against control_plane_key?
RESULT: VALID

VERIFIER CHECK: Timestamp within window?
RESULT: VALID (300 second window)

VERIFIER CHECK: Nonce format valid?
RESULT: VALID

Step 4: Parameter Bounds Verification

CRITICAL STEP: Verify execution parameters match approved bounds.

APPROVED BOUNDS:
{
  "tool": "^database_query$",
  "query": "^SELECT.*FROM users WHERE id = .+$", 
  "params": "^[a-zA-Z0-9_]+$"
}

ORIGINAL PARAMETERS:
{
  "query": "SELECT * FROM users WHERE id = 'user_42'",
  "params": ["user_42"]
}

VERIFIER CHECKS:
1. "database_query" matches "^database_query$" → VALID
2. query starts with "SELECT" matches "^SELECT.*FROM users..." → VALID
3. params "user_42" matches "^[a-zA-Z0-9_]+$" → VALID

EXECUTION PARAMETERS = APPROVED PARAMETERS (no narrowing needed)

If ANY check FAILS → DENY. INV-2 would be violated.

Step 5: Execution

Observation: Execution completed. Execution layer returns:

{
  "trace_id": "trace_xyz789",
  "approval_id": "apr_xyz789", 
  "identity": "user_abc123",
  "parameters_executed": {
    "query": "SELECT * FROM users WHERE id = 'user_42'",
    "params": ["user_42"]
  },
  "outcome": "SUCCESS",
  "timestamp": 1712841700
}

VERIFIER CHECK:
parameters_executed == original parameters → CONFIRMED
parameters_executed within bounds → CONFIRMED

This confirms INV-2: parameters within approved bounds.

Step 6: Audit Chain Verification

Retrieve audit records for this execution:

RECORD 1 (Gate):
{
  "record_id": "log_001",
  "sequence": 1,
  "previous_hash": "0000000000000000",
  "timestamp": 1712841600,
  "identity": "user_abc123",
  "decision": "APPROVED",
  "approval_id": "apr_xyz789",
  "trace_id": "trace_xyz789",
  "request_hash": "sha256(req_xyz789)",
  "data_hash": "sha256(log_001)"
}

RECORD 2 (Control Plane):
{
  "record_id": "log_002",
  "sequence": 2,
  "previous_hash": "sha256(log_001)",
  "timestamp": 1712841600,
  "identity": "user_abc123", 
  "decision": "APPROVED_WITH_BOUNDS",
  "approval_id": "apr_xyz789",
  "trace_id": "trace_xyz789",
  "request_hash": "sha256(req_xyz789)",
  "bounds_used": {
    "query": "^SELECT.*FROM users WHERE id = .+$"
  },
  "data_hash": "sha256(log_002)"
}

RECORD 3 (Execution):
{
  "record_id": "log_003",
  "sequence": 3,
  "previous_hash": "sha256(log_002)",
  "timestamp": 1712841700,
  "identity": "user_abc123",
  "decision": "EXECUTED",
  "approval_id": "apr_xyz789",
  "trace_id": "trace_xyz789",
  "request_hash": "sha256(req_xyz789)",
  "parameters_executed": {
    "query": "SELECT * FROM users WHERE id = 'user_42'",
    "params": ["user_42"]
  },
  "outcome": "SUCCESS",
  "data_hash": "sha256(log_003)"
}

VERIFIER CHECKS:
1. Hash chain: log_003.previous_hash == sha256(log_002) → VALID
2. Chain continuity: log_002.previous_hash == sha256(log_001) → VALID
3. trace_id consistent across all records → CONFIRMED
4. request_hash matches request → CONFIRMED

This confirms INV-5: audit attribution.

Step 7: Invariant Mapping

MAP each verification step to specification invariants:

STEP 1 (Request signature)
→ INV-3: Cryptographic Attribution
  ✓ Identity verified, timestamp valid, nonce unused

STEP 3 (Approval envelope)
→ INV-1: Pre-Execution Policy Check
  ✓ Signed approval envelope present, valid signature

STEP 4 (Parameter bounds)
→ INV-2: Parameter Binding
  ✓ Parameters within approved bounds

STEP 5 (Execution parameters)
→ INV-2: No silent truncation
  ✓ Executed parameters == original parameters

STEP 6 (Audit records)
→ INV-5: Audit Attribution
  ✓ All decisions logged, hash chain intact

IMPLICIT CHECK:
→ INV-6: Enforcement Completeness
  No unauthenticated interfaces were accessed.
  All traffic passed through Gate.

RESULT: All six invariants VERIFIED.

What the verifier concluded

VERIFIER CONCLUSION:

Given ONLY:
• Raw request with identity signature
• Approval envelope with Control Plane signature
• Execution trace with parameters
• Audit log export with hash chain

The verifier can independently confirm:

1. Identity was verified → INV-3 holds
2. Policy was evaluated → INV-1 holds  
3. Parameters are bound → INV-2 holds
4. Parameters were not truncated → INV-2 holds
5. Decision was attributed → INV-5 holds
6. No bypass occurred → INV-6 holds

FAILURE SCENARIOS DETECTED:

If identity signature INVALID → INV-3 fails
If no approval envelope → INV-1 fails  
If parameters outside bounds → INV-2 fails
If silent truncation detected → INV-2 fails
If no audit record → INV-5 fails
If audit chain broken → INV-5 fails

If ANY invariant fails → fail-closed enforcement worked correctly (denial occurred)

Adversarial Validation

Attempt to violate invariants and observe system response:

SCENARIO 1: Modify parameters after approval
Input: query = "SELECT * FROM users; DROP TABLE users;"
Bounds: query must start with "SELECT"

Expected: DENIED_BOUNDS_EXCEEDED
Actual: DENIED_BOUNDS_EXCEEDED
Result: INV-2 holds

SCENARIO 2: Replay previous request
Input: same nonce as previous request

Expected: DENIED_REPLAY
Actual: DENIED_REPLAY  
Result: INV-3 holds

SCENARIO 3: Execute bypassing Gate
Input: Direct call to execution.example.com

Expected: REJECTED (no envelope)
Result: REJECTED (no envelope)
Result: INV-6 holds

SCENARIO 4: Expired approval
Input: timestamp outside 5-minute window

Expected: DENIED_EXPIRED
Actual: DENIED_EXPIRED
Result: INV-1 holds

SCENARIO 5: Control Plane unavailable
Input: Control Plane returns 503

Expected: DENIED_CONTROL_PLAN_UNAVAILABLE
Actual: DENIED_CONTROL_PLAN_UNAVAILABLE
Result: INV-4 holds

All adversarial scenarios correctly denied.

Independent Verification Procedure

FULL VERIFICATION PROCEDURE (for auditors):

Prerequisites:
1. Specification v1.0 (this document)
2. Public keys (identity + control plane)
3. Raw request export
4. Audit log export

Steps:
1. Extract request from export
2. Verify identity signature
3. Retrieve approval envelope
4. Verify control plane signature
5. Extract approved bounds
6. Compare parameters to bounds
7. Verify no truncation occurred
8. Retrieve audit records
9. Verify hash chain continuity
10. Confirm trace_id matches

Expected output per step:
• Step 2: VALID or INVALID
• Step 3: APPROVED or DENIED
• Step 4: VALID or INVALID
• Step 5: MATCH or EXCEEDS_BOUNDS
• Step 6: MATCH or TRUNCATED
• Step 7: LOGGED or MISSING
• Step 8: CONTINUOUS or BROKEN
• Step 9: MATCH or MISMATCH

PASS CRITERIA:
All steps report expected output → enforcement verified
Any step reports unexpected → invariant violation detected