Cryptographic Verification Suite

The Cryptographic Verification Suite is OpenForge's primary differentiator — a collection of eight specialized analysis engines purpose-built for verifying post-quantum cryptographic hardware implementations. These tools address security verification gaps that no commercial EDA vendor currently covers, providing pre-silicon confidence in constant-time execution, side-channel resistance, entropy integrity, FIPS compliance, and algorithmic correctness.

Overview #

Traditional EDA verification focuses on functional correctness — does the design produce the right outputs? Cryptographic hardware verification requires an additional dimension: security correctness. A functionally correct AES implementation that leaks key bits through power consumption is a catastrophic failure. OpenForge's crypto verification suite addresses this gap with eight specialized engines that operate as a unified pipeline.

All eight engines can be invoked individually via CLI, configured through openforge.yaml, or orchestrated as a unified pipeline through the workflow engine. Results feed into a unified security dashboard with SARIF export for CI/CD integration.

Cryptographic Security Pod #

The Cryptographic Security Pod runs as an isolated Docker container (or Kubernetes pod) within the OpenForge verification pipeline. It executes after simulation completes, consuming simulation artifacts (waveforms, power traces, coverage data) and producing security analysis reports.

The pod's execution follows a dependency-aware DAG:

# Crypto verification execution order (parallel where possible)

Stage 1:  lint → simulation (produces power traces, waveforms)
Stage 2:  ┌─ formal verification ──────────────────────┐
          │                                             │
          ├─ constant-time (uses taint analysis)        │
          ├─ side-channel  (uses power traces from sim)  │  parallel
          ├─ entropy      (uses RTL parse tree)          │
          ├─ FIPS         (uses formal + RTL)            │
          ├─ NTT          (uses sim + formal)            │
          └─ fault-inj    (uses instrumented sim)       │
Stage 3:  synthesis → timing → aggregate report

Each engine runs in its own isolated process with configurable resource limits (CPU cores, memory, timeout). Results are written to the shared PostgreSQL metadata store and MinIO object storage for waveform/trace artifacts.

Constant-Time Verifier (openforge-ct) #

The constant-time verifier ensures that cryptographic operations execute in exactly the same number of clock cycles regardless of secret input values. This is critical for preventing timing side-channel attacks, where an attacker measures execution time to extract secret keys.

How It Works

The verifier uses a three-phase approach: static taint analysis to detect potential violations, formal verification to mathematically prove constant-time properties, and simulation-based validation as a cross-check.

Phase 1: Taint Analysis — Mark signals as secret or public, then propagate taint labels through the dataflow graph. Any tainted signal reaching a control-flow decision (branch condition, FSM transition) or memory address bus is flagged as a violation.

# Python API — Constant-Time Analysis
from openforge.crypto import ConstantTimeVerifier

verifier = ConstantTimeVerifier("src/rtl/ntt_butterfly.v")

# Mark secret signals — these must not influence timing
verifier.mark_secret("key_reg")
verifier.mark_secret("seed")
verifier.mark_secret("private_key")

# Mark public outputs — safe to have data-dependent values
verifier.mark_public("ciphertext")
verifier.mark_public("public_key")

# Run analysis
report = verifier.verify()

print(f"Control-flow violations: {len(report.cf_violations)}")
print(f"Memory-access violations: {len(report.mem_violations)}")
print(f"Variable-timing violations: {len(report.timing_violations)}")
print(f"Formal proof: {'PROVEN' if report.formal_proven else 'FAILED'}")

Phase 2: Formal Verification — For designs that pass static analysis, the verifier generates SystemVerilog Assertions (SVA) and feeds them to SymbiYosys for mathematical proof. The key properties verified are:

// Auto-generated SVA properties for constant-time verification

// Control flow must not depend on secret data
property ct_no_secret_branch(clk, secret, branch_cond);
    @(posedge clk)
    $stable(secret) |-> $stable(branch_cond);
endproperty

// Memory addresses must not depend on secret data
property ct_no_secret_addr(clk, secret, addr);
    @(posedge clk)
    $stable(secret) |-> $stable(addr);
endproperty

// Execution latency must be fixed regardless of secret values
property ct_fixed_latency(clk, start, done, LATENCY);
    @(posedge clk)
    start |-> ##LATENCY done;
endproperty

Phase 3: Simulation Cross-Check — Run the design with multiple random secret values and verify that cycle counts are identical across all runs. This catches issues that static analysis might miss due to tool limitations.

Violation Types

CLI Usage

# Run constant-time analysis with default settings
$ openforge verify --crypto --constant-time

# Specify secrets via CLI (overrides openforge.yaml)
$ openforge verify --crypto --constant-time \
    --secrets "key_reg,seed,sk_bytes" \
    --public "ciphertext,pk_bytes"

# Run with formal proof (slower but mathematically rigorous)
$ openforge verify --crypto --constant-time --formal --timeout 7200

# Generate detailed HTML report
$ openforge verify --crypto --constant-time --report html \
    --output reports/ct_analysis.html

Side-Channel Simulator (openforge-sca) #

The side-channel simulator estimates power consumption during RTL simulation and runs statistical leakage detection tests. It answers the question: "If an attacker measured the power consumption of this chip, could they extract secret keys?"

Power Models

Three power estimation models are available, each trading accuracy for speed:

Leakage Detection: TVLA

Test Vector Leakage Assessment (TVLA) uses Welch's t-test to compare power traces from fixed inputs against random inputs. A t-value exceeding the threshold (default: 4.5) at any clock cycle indicates statistically significant leakage with >99.999% confidence.

# Python API — TVLA Analysis
from openforge.crypto import SideChannelSimulator

sca = SideChannelSimulator(
    design_path="src/rtl/mlkem_top.v",
    power_model="hamming_distance"
)

# Collect power traces (requires Verilator with --power-trace)
sca.simulate_with_power(
    testbench="tb/mlkem_keygen_tb.py",
    num_traces=50000
)

# Run TVLA — fixed vs. random
tvla_report = sca.run_tvla(
    fixed_input=bytes.fromhex("00" * 32),
    threshold=4.5
)

print(f"Max t-value: {tvla_report.max_t:.2f}")
print(f"Leakage points: {len(tvla_report.leakage_points)}")
print(f"Verdict: {'PASS' if tvla_report.passed else 'FAIL — LEAKAGE DETECTED'}")

Attack Simulation: CPA

Correlation Power Analysis (CPA) simulates an actual key-recovery attack against your design. For each subkey byte, it correlates hypothetical power consumption (based on a key guess) with actual simulated traces. If the correct key shows the highest correlation, the design is vulnerable.

# CPA attack simulation
cpa_report = sca.run_cpa(
    target_operation="ntt_butterfly",
    key_byte_index=0,
    num_traces=10000
)

print(f"Key recovered: {cpa_report.recovered_key is not None}")
print(f"Correlation (correct key): {cpa_report.correct_key_correlation:.4f}")
print(f"Correlation (best wrong key): {cpa_report.best_wrong_correlation:.4f}")
print(f"Minimum traces for attack: ~{cpa_report.estimated_traces_needed}")

ChipWhisperer Integration

For post-silicon validation, OpenForge can import ChipWhisperer capture files and compare predicted traces (from simulation) against measured traces (from physical hardware). This correlation validates the accuracy of the RTL power model.

# Compare simulated vs. measured traces
$ openforge verify --crypto --side-channel \
    --compare-traces chipwhisperer_captures/mlkem_traces.npy \
    --correlation-threshold 0.85

Entropy Flow Analyzer (openforge-entropy) #

The entropy flow analyzer tracks how randomness propagates through a cryptographic design — from QRNG/TRNG sources to cryptographic consumption points (key generation, nonce creation, masking). It ensures that entropy is not inadvertently reduced, corrupted, or biased before reaching security-critical operations.

Analysis Pipeline

The analyzer builds a directed flow graph using NetworkX, where nodes represent signals/registers and edges represent data dependencies. Entropy annotations propagate through the graph, with special handling for entropy-reducing operations:

# Python API — Entropy Flow Analysis
from openforge.crypto import EntropyFlowAnalyzer

analyzer = EntropyFlowAnalyzer("src/rtl/qrng_pipeline.v")

# Define entropy sources
analyzer.mark_entropy_source(
    signal="qrng_raw_out",
    bits_per_sample=0.99,    # min-entropy per output bit
    source_type="QRNG"
)

# Define entropy consumption points
analyzer.mark_entropy_sink(
    signal="keygen_seed",
    required_entropy=256,      # bits required
    purpose="key_generation"
)
analyzer.mark_entropy_sink(
    signal="nonce_value",
    required_entropy=128,
    purpose="nonce_generation"
)

# Run analysis
report = analyzer.analyze()

for violation in report.violations:
    print(f"[{violation.severity}] {violation.message}")
    print(f"  Path: {' → '.join(violation.path)}")
    print(f"  Entropy at sink: {violation.entropy_at_sink:.2f} bits")

FIPS Compliance Checker (openforge-fips) #

The FIPS compliance checker automatically verifies RTL implementations against FIPS 140-3 Level 2 requirements. It combines pattern matching (for structural requirements) with formal verification (for behavioral requirements) to produce a compliance report suitable for pre-submission review.

Automated Checks

Key Zeroization Formal Proof

The most critical FIPS check is key zeroization. The checker generates SVA properties and verifies them with SymbiYosys:

// Auto-generated zeroization properties

// Key register cleared within 100 cycles of zeroize
property key_zeroized;
    @(posedge clk)
    zeroize |-> ##[1:100] (key_reg == '0);
endproperty

// Zeroization completes in bounded time (no infinite loops)
property zeroize_completes;
    @(posedge clk)
    zeroize |-> ##[1:100] zeroize_done;
endproperty

// No key material on any output during or after zeroization
property no_key_on_output;
    @(posedge clk)
    zeroize |-> (data_out == '0) throughout (##[0:100] zeroize_done);
endproperty

# Run FIPS compliance check
$ openforge verify --crypto --fips-compliance

# Generate compliance report for certification submission
$ openforge verify --crypto --fips-compliance \
    --report pdf --output reports/fips_compliance.pdf

# Check specific rules only
$ openforge verify --crypto --fips-compliance \
    --checks key_zeroization,self_test_coverage,rng_health_tests

NTT/Polynomial Validator (openforge-ntt) #

The NTT validator verifies that Number Theoretic Transform implementations precisely match the FIPS 203 (ML-KEM) and FIPS 204 (ML-DSA) reference specifications. Even a single-bit error in a twiddle factor or butterfly operation can compromise security without producing obviously wrong outputs.

Validation Targets

Exhaustive Testing

For ML-KEM with q=3329, individual butterfly operations are small enough to test exhaustively. OpenForge tests all 3329 × 3329 × 128 input combinations (a, b, twiddle_index) for each butterfly unit — approximately 1.4 billion test vectors. This runs in parallel across available CPU cores:

# Run exhaustive NTT validation (ML-KEM)
$ openforge verify --crypto --ntt-validation \
    --standard FIPS-203 \
    --exhaustive \
    --parallel 16

# Quick mode — random vectors only (good for CI)
$ openforge verify --crypto --ntt-validation \
    --standard FIPS-203 \
    --vectors 100000

# Validate ML-DSA NTT (q=8380417, larger field)
$ openforge verify --crypto --ntt-validation \
    --standard FIPS-204 \
    --vectors 500000

Fault Injection Resilience (openforge-fi) #

The fault injection engine simulates physical fault attacks — clock glitches, voltage glitches, and electromagnetic pulses — at the RTL level. It systematically injects single-bit and multi-bit faults into registers and checks whether the design detects the fault, produces incorrect output silently, or enters an unsafe state.

Fault Models

# Run fault injection campaign
$ openforge verify --crypto --fault-injection \
    --model single-bit \
    --target-registers "ntt_stage_*,key_reg_*" \
    --campaigns 10000

# Comprehensive multi-model campaign
$ openforge verify --crypto --fault-injection \
    --model all \
    --report html --output reports/fault_campaign.html

The engine reports: (a) detected faults — the design's error detection correctly flagged the fault, (b) masked faults — the fault had no effect on outputs, (c) effective faults — the fault changed the output without detection. Effective faults indicate vulnerability to physical attacks and require countermeasure insertion (redundancy, error codes, temporal checking).

Leakage Contract Verification (openforge-leak) #

Leakage contracts formalize what information a cryptographic implementation is allowed to leak. Building on the LeaVe framework, OpenForge verifies that the actual leakage of a design conforms to a specified contract — for example, "the only information leaked through power consumption is the Hamming weight of public outputs."

# openforge.yaml — Leakage contract configuration
crypto_verification:
  leakage_contracts:
    enabled: true
    contracts:
      - module: ntt_butterfly
        allowed_leakage:
          - hamming_weight(public_output)
          - hamming_weight(address_bus)
        forbidden_leakage:
          - any_function(secret_key)
          - any_function(private_seed)

Key Management Verifier (openforge-km) #

The key management verifier analyzes the complete lifecycle of cryptographic keys within the design — generation, storage, usage, rotation, and destruction. It checks for common key management errors that compromise security even when the underlying cryptography is correct.

Lifecycle Checks

# Formal property: Key never appears on output bus
property key_isolation(clk, key_reg, output_bus);
    @(posedge clk)
    !(key_reg == output_bus) || (key_reg == '0);
endproperty

Configuration Reference #

All crypto verification settings are configured under the crypto_verification key in openforge.yaml:

crypto_verification:
  # Constant-time analysis
  constant_time:
    enabled: true
    secrets:                       # Signals containing secret data
      - "key_reg"
      - "seed"
      - "private_key"
    public:                        # Signals safe to have data-dependent values
      - "ciphertext"
      - "public_key"
    formal_proof: true              # Generate and verify formal properties
    simulation_crosscheck: true     # Run simulation-based validation

  # Side-channel simulation
  side_channel:
    enabled: true
    power_model: hamming_distance   # hamming_weight | hamming_distance | switching
    tvla_threshold: 4.5            # t-value threshold for leakage detection
    num_traces: 50000              # Number of power traces to collect
    cpa_enabled: true              # Run CPA attack simulation
    chipwhisperer_compare: null    # Path to CW capture file for comparison

  # Entropy flow analysis
  entropy_analysis:
    enabled: true
    sources:
      - signal: "qrng_out"
        min_entropy: 0.99
        rate: 8                     # bits per clock cycle
    sinks:
      - signal: "keygen_seed"
        required_entropy: 256

  # FIPS 140-3 compliance
  fips_compliance:
    enabled: true
    level: "140-3 Level 2"
    checks:
      - key_zeroization
      - self_test_coverage
      - error_output_inhibit
      - approved_algorithms
      - rng_health_tests
      - fsm_integrity

  # NTT/Polynomial validation
  ntt_validation:
    enabled: true
    standard: "FIPS-203"           # FIPS-203 (ML-KEM) | FIPS-204 (ML-DSA)
    exhaustive_test: true          # Test all input combinations (q=3329)
    twiddle_rom_check: true
    butterfly_formal: true

  # Fault injection
  fault_injection:
    enabled: false                 # Disabled by default (slow)
    models: [single-bit, instruction-skip]
    campaigns: 10000

  # Leakage contracts
  leakage_contracts:
    enabled: false
    contracts: []

  # Key management
  key_management:
    enabled: true
    key_signals:
      - "key_reg"
      - "session_key"
    checks: [isolation, zeroization, usage_separation]

Interpreting Results #

Crypto verification results are aggregated into a unified security score with per-engine breakdown:

══════════════════════════════════════════════════════════
  OPENFORGE CRYPTO VERIFICATION REPORT
══════════════════════════════════════════════════════════
  Project:   QCORE-C1 NTT Engine
  Date:      2026-01-15 14:32:07 UTC
  Duration:  47m 23s
──────────────────────────────────────────────────────────

  Engine                     Status    Findings
  ─────────────────────────  ────────  ──────────────────
  Constant-Time Verifier     ✓ PASS    0 violations, proven
  Side-Channel (TVLA)        ✓ PASS    max t=3.21 (< 4.5)
  Side-Channel (CPA)         ✓ PASS    no key recovery
  Entropy Flow               ✓ PASS    256 bits at sink
  FIPS Compliance            â–³ WARN    6/7 checks pass
  NTT Validation             ✓ PASS    1.4B vectors, 0 mismatches
  Fault Injection            ✗ FAIL    23/10000 effective faults
  Key Management             ✓ PASS    isolation proven

──────────────────────────────────────────────────────────
  Overall: 6/8 PASS, 1 WARN, 1 FAIL

  Action Items:
  1. [FIPS-006] Cryptographic boundary incomplete — debug port
     crosses boundary. Remove or gate debug access.
  2. [FI-CRIT] 23 effective single-bit faults in NTT stage 3.
     Add redundancy or error detection codes.
══════════════════════════════════════════════════════════

Integration with CI/CD #

Crypto verification results export in SARIF (Static Analysis Results Interchange Format) for integration with GitHub Advanced Security, GitLab SAST, and other CI/CD platforms:

# Generate SARIF report for GitHub Security tab
$ openforge verify --crypto --all \
    --report sarif --output security/crypto_results.sarif

# GitHub Actions workflow snippet
- name: Crypto Verification
  run: openforge verify --crypto --all --report sarif --output results.sarif

- name: Upload Security Results
  uses: github/codeql-action/upload-sarif@v3
  with:
    sarif_file: results.sarif
    category: crypto-verification

For detailed CI/CD integration patterns including merge gates, nightly builds, and webhook notifications, see the CI/CD Integration Guide.