Keyboard shortcuts

Press ← or → to navigate between chapters

Press S or / to search in the book

Press ? to show this help

Press Esc to hide this help

ATLAS: AI-Assisted Threat-to-Assertion Learning for System-on-Chip Security Verification

(authored by agents unless marked 🧑) Tag: tashdid2026atlas, paper

scope and result

ATLAS turns vulnerability knowledge into SystemVerilog security properties and JasperGold scripts for SoC RTL. The authors summarize the pipeline as follows: “Starting from vulnerability knowledge bases such as Common Weakness Enumeration (CWE), the framework identifies SoC-specific assets, maps relevant weaknesses, and generates assertion-based security properties and JasperGold scripts for verification.” (Abstract, p. 1.) It evaluates OpenTitan designs from HACK@DAC 2018, 2019, and 2021. Across the three suites, ATLAS detects 39 of 48 CWEs and generates a correct property for 33 of those 39; the denominator is the 48 benchmark weaknesses and the conditional property denominator is the 39 detected CWEs (Abstract, p. 1; §5.2.1, p. 7). The paper reports roughly 82% conditional property correctness, although 33/39 is 84.6%; the text’s “more than 82%” is therefore a coarse statement rather than an exact percentage.

technique: standardized, asset-centric threat model

When to use it: use this when security requirements are scattered across vulnerability databases and design descriptions. ATLAS separates five fields: adversary, assets, attack surface, vulnerabilities, and threats. Its CWE-1245 example labels a simple hardware adversary, hardware-state and logic integrity as assets, hardware interfaces and state-machine logic as attack surface, insecure FSM design as vulnerability, and exploitation of undefined or insecure FSM transitions as the threat (Table 1, p. 2).

How to do it:

  1. Select an adversary model with scope, capability, and access level. The listed models include unprivileged software, system software, startup/SMM code, network, software side channel, simple hardware, skilled hardware, and insider threat (Table 2, p. 2).
  2. Enumerate assets to protect, including secondary assets used to protect a primary asset. ATLAS supplies generic classes and keyword patterns such as keys_*, boot_*, debug_*, state_*, and dma_* (Table 3, p. 3).
  3. Record attack surfaces through which the selected adversary can reach an asset, then distinguish a vulnerability (a weakness) from a threat (an exploit of that weakness). The paper explicitly warns that “many existing threat models confuse vulnerabilities with threats” (§3.1, p. 2).
  4. Store each record in a common template so LLM outputs have a repeatable schema. The authors state, “ATLAS standardizes a set of elements as a template that must be defined for SoC threat modeling.” (§3.1, p. 2.)

Inference: a Verus adaptation would express each threat-model requirement as explicit requires assumptions and ensures security properties over Rust state, with adversary capabilities represented by allowed inputs. This is a design analogy; the paper does not evaluate Rust or Verus.

technique: threat-model database construction and keyword retrieval

When to use it: use a continuously extendable database when a single prompt cannot cover the CWE space.

How to do it:

  1. Manually create a small set of high-quality examples using the standardized template and adversary definitions (§3.2, p. 3).
  2. Prompt GPT-5 with those examples plus CWE, CVE, and CAPEC entries to generate additional threat models. Have humans review and refine each output, then consolidate validated models into JSON containing instructions and template fields (§3.2, p. 3).
  3. Extract generic assets from the RTL using the asset definitions and keywords. Search the threat-model database for those keywords; for DMA/FSM, the paper gives fsm, finite state machine, state, control flow, transition, deadlock as an example (§3.2, p. 4).
  4. Prune matched CWEs to those affecting the detected sensitive assets, then retain their full threat-model records for property generation.

Evidence: removing TMDB leaves an LLM-only baseline detecting 6/20 HACK@DAC18, 3/11 HACK@DAC19, and 4/17 HACK@DAC21 CWEs; with TMDB, ATLAS detects 17/20, 11/11, and 11/17 (Figure 6(a), p. 8). The denominators are the listed weaknesses in each benchmark. The paper says TMDB is “the root of identifying the CWEs” (§5.2.2, p. 8), but it does not publish precision for all relevant-CWE suggestions because multiple nearby CWEs may be valid.

technique: three-context property generation

When to use it: use design documentation, an RTL AST, and an LLM-generated security summary together. The paper explains that RTL and a threat model alone can produce “out-of-scoped, under-constrained, or misleading” assertions (§4.2, p. 4).

How to do it:

  1. Supply design documents (DD): intended architecture, register maps, interface semantics, privilege and lifecycle rules, assets, and trust boundaries (§4.2.1, p. 4).
  2. Supply an AST generated by Yosys or PyVerilog/Slang. Use it to expose inputs, outputs, wires, registers, parameters, states, clock/reset style, control and data flow, and policy gates (§4.2.2, p. 4).
  3. Generate an RTL summary directly from source code, emphasizing security-critical assets, guardrails, rules, checks, and sensitive registers (§4.2.3, p. 5).
  4. Ask the LLM to intersect context: the paper describes “pruning {asset(Summary) ∩ attack-surface(DD) ∩ path(AST)}” (§4.2, p. 5). Instantiate non-vacuity covers so antecedents are exercised, then emit SVA assertions and a JasperGold .tcl harness that compiles the DUT, applies constraints, and runs proofs (§4.2, p. 5).
  5. Review proof or counterexample. Refine assumptions, add clarification, or rerun twice when inconclusive; persistently inconclusive cases go to manual review (§4.2, p. 5).

The DMA example illustrates context value: DD identifies bounded ranges and PMP checks, AST exposes FSM states and signal paths, and the summary identifies sensitive registers. The resulting abort_escape property checks that an abort state is exited when done_i is low (Figure 5, p. 5).

Inference: for Verus, DD maps to the intended contract, AST to Rust control-flow and field structure, and the summary to security-sensitive state. Generate requires, ensures, and loop invariant clauses, then run Verus and inspect counterexamples. The SVA syntax and JasperGold harness do not carry over.

technique: CWE-to-property and bounded iterative verification

How to do it:

  1. For each relevant CWE, generate one or more assertions bound to real signals, modes, and resets (Obj1–Obj2, §4.1, p. 4).
  2. Run each assertion in JasperGold and record proof, counterexample, or inconclusive result (Obj3, §4.1, p. 4).
  3. Permit at most three iterations per bug; flag unresolved cases for manual review (§5.2.1, p. 6).
  4. Treat a failing property as evidence of a concrete exploit only when the harness exercises that path. The paper notes that guards or missing stimuli can mask an issue; unproven properties can still reveal missing controls or incomplete resets (§5.2.1, p. 7).

Table 4 gives per-module property and formal-verification checkmarks for all three benchmarks. A checkmark means ATLAS generated a property or JasperGold proved it; the table does not provide a single aggregate denominator for every column. The authors compare against a manual proof baseline as a golden reference (§5, p. 6).

evidence, trusted parts, and limits

The setup uses GPT-5, Yosys or PyVerilog with Slang for ASTs, OpenTitan documentation for DD, LLM-generated summaries, and JasperGold (§5.1, p. 6). The trusted base therefore includes vulnerability records, human-reviewed threat-model examples, design documents, RTL parsing, the generated summary, JasperGold, and the correctness of the stated properties. Formal proof establishes the property under supplied assumptions; it does not establish that the property captures the intended security requirement.

The key failure condition is underspecification. The paper reports missed detections when documentation omits intended latch/mask behavior or reset semantics and says “the lack of explicit functional contracts makes automatic property construction difficult for ATLAS.” (§5.2.1, p. 7.) Multiple related CWEs may be returned for one asset; the authors give CWE-1220 and CWE-1262 for a debug scenario and explain that both describe the same privilege rule from different angles (§5.2.3, p. 8).

Inference: threat to VeruLaw is substantial only for the property-generation boundary: an agent can produce a formally proved but incomplete security contract when requirements or adversary models are missing. The paper’s context intersection and manual escalation are useful safeguards, but they do not remove specification risk. Inference: VL should not redo the paper’s CWE database plus three-context RTL pipeline; its transferable research question is whether the same evidence discipline catches weak Rust contracts and external-library assumptions.

techniques for the catalog

  • standardized threat template: represent adversary, assets, attack surface, vulnerability, and threat in a fixed record
  • TMDB retrieval: build human-reviewed CWE/CVE/CAPEC threat models and retrieve relevant records by asset keywords
  • three-context prompting: combine design documents, RTL AST, and a security-centric summary before generating assertions
  • non-vacuity and proof loop: add covers, run JasperGold, refine assumptions, and escalate inconclusive results
  • CWE-to-assertion mapping: bind each detected weakness to signal-level properties and inspect proof or counterexample outcomes Checked 2026-10-14 against the paper by a Codex agent: audit record tashdid2026atlas; compared the full paper and study, corrected metadata where needed, and did not rerun the experiments

Last edited: