LASHED: LLMs And Static Hardware Analysis for Early Detection of RTL Bugs

TL;DR

LASHED tackles the challenge of detecting hardware RTL security bugs early by blending Large Language Models (LLMs) with static analysis. The framework uses LLMs for assets identification, pruning false positives, and explaining violations, while static analysis (linting or formal verification) provides verification and structure, guided by MITRE hardware CWEs. Through four open-source SoCs and five CWEs, LASHED demonstrates that prompting strategies with in-context learning and thinking-again prompts can achieve high precision, up to around 0.88 in certain configurations, with an overall notable improvement over baselines. The work suggests that integrating LLM reasoning with formal and lint-based checks can offer scalable, actionable pre-silicon security diagnostics for complex RTL designs, with practical implications for hardware verification workflows.

Abstract

While static analysis is useful in detecting early-stage hardware security bugs, its efficacy is limited because it requires information to form checks and is often unable to explain the security impact of a detected vulnerability. Large Language Models can be useful in filling these gaps by identifying relevant assets, removing false violations flagged by static analysis tools, and explaining the reported violations. LASHED combines the two approaches (LLMs and Static Analysis) to overcome each other's limitations for hardware security bug detection. We investigate our approach on four open-source SoCs for five Common Weakness Enumerations (CWEs) and present strategies for improvement with better prompt engineering. We find that 87.5% of instances flagged by our recommended scheme are plausible CWEs. In-context learning and asking the model to 'think again' improves LASHED's precision.

Figures (5)

• Figure 1: LASHED framework. 1) Assets Identification (AssetID): LLM identifies assets relevant to a CWE in the RTL. 2) Static Analysis: Depending on CWE, a linting or assertion-based strategy is used. A linter or formal property verification tool checks for the lint tags identified or assertions formed. 3) Contextualization: LLM reasons and prunes linting violations or falsified properties. LLM gives an explanation if there is a security issue.
• Figure 2: Motivating example for CWE 1191 to illustrate LASHED flow for linter-based strategy.
• Figure 3: Motivating example for CWE 1233 to illustrate LASHED flow for assertion based strategy.
• Figure 4: Classification of instances flagged by LASHED. Stacked bar shows the number of instances identified by LASHED that pose security issues as true positives (tp) and those that do not as false positives (fp). The numbers are summed up for all CWEs.
• Figure 5: Intermediary outputs during LASHED's operation. # assets identified is number of security relevant signals identified during Assets Identification, # assertions formed is the number of assertions formed during Static Analysis. # violations removed in contextualization is the number of violations that the LLM reasoned as not posing a security threat. The numbers are summed up for all CWEs.