Agentic SoC Security Validation

Instructor 

Dr. Farimah Farahmandi is the Wally Rhines Endowed Professor in Hardware Security in the Department of Electrical and Computer Engineering (ECE) at the University of Florida

Learning Objectives

The Agentic SoC Security Validation micro-certificate prepares participants to use large language models (LLMs) within structured workflows for hardware security testing, RTL debugging, and countermeasure development. Participants learn to turn hardware weakness descriptions and design specifications into testable hypotheses, trace observed failures to their RTL causes, and evaluate proposed repairs using simulation and formal verification.

The course emphasizes evidence at every stage. Generated hypotheses must refer to real design signals, security tests must exercise meaningful attack and control conditions, and repairs must satisfy independent verification checks. Participants learn why functional sign-off does not establish security, why a plausible explanation does not validate an edit, and why an accepted countermeasure still requires engineering review.

The micro-certificate is organized into the following three units:

• Unit 1 Security validation through test generation: Participants investigate a functionally signed-off debug-unlock controller, secure_unlock_fsm, using a hardware weakness class rather than an existing bug report. They translate CWE-1245, Improper Finite State Machines in Hardware Logic, into structured hypotheses that identify triggering inputs, relevant signals, and observable violations. Mechanical signal checks and critic refinement help remove ungrounded or redundant hypotheses before test generation.The workflow converts each hypothesis into a cycle-specific scenario with an attack arm, a control arm, and a predefined region of interest. Generated SystemVerilog testbenches are compiled and simulated. A golden monitor is derived from the specification without access to the observed design behavior or RTL, and is compared with simulation results. Participants apply the two-arm rule: a finding is confirmed only when the monitors disagree on the attack arm and agree on the control arm. They also identify ineffective attack stimulus and incorrect expectations, and explain why a passing generated test cannot establish the absence of a weakness.
• Unit 2 Automated RTL debugging and root causing: Participants use a synchronous stack, FILO_RTL, to distinguish a reported symptom from the line that causes it. An LLM produces a causal defect graph anchored in RTL signals and source lines before proposing a repair. The graph makes the reasoning available for review, while its confidence estimates remain model judgments rather than proof of causality.The unit combines example-based functional tests with adversarial invariant tests for stack order, depth, and quiet behavior. Candidate patches are eligible only when the functional suite passes and every required invariant holds in the executed tests. Participants compare candidates using defect closure, functional preservation, patch minimality, and synthesis area when Yosys is available. They interpret Pareto selection and an observed-regret stopping rule, keeping a held-out oracle outside the repair loop. The exercise demonstrates why a small change that leaves the bug intact and an unnecessarily broad rewrite are poor engineering choices.
• Unit 3 Automated RTL countermeasure development: Participants harden crypto_wrapper, an AES accelerator register wrapper, against debug-mode key exposure, key-register readback, and incomplete plaintext clearing. Security requirements are expressed as assertions. JasperGold, or the supplied Yosys and SymbiYosys flow, produces proof results or counterexamples that guide an LLM toward a root cause and minimal RTL edits. The agent may change the RTL but may not weaken the assertions.Acceptance requires the violated assertion to be proven, its precondition to remain reachable, required function covers to remain reachable, and previously proven assertions to remain proven. Failed checks guide a bounded retry. Participants then examine an accepted plaintext-clearing change that also drops unrelated register writes in the same cycle. An additional review assertion exposes this side effect, demonstrating that the strength of formal evidence depends on the properties and model being checked.

Learning Outcomes:

1. Upon successful completion, participants will be able to use LLM agents to investigate RTL security weaknesses, locate defects, and develop countermeasures while evaluating each result against independent simulation or formal evidence.
2. Translate a hardware CWE and design specification into refutable security hypotheses grounded in actual RTL signals and states.
3. Construct and evaluate cycle-specific security scenarios with distinct attack and control arms and a predefined region of interest.
4. Validate generated testbenches using simulation monitors and specification-derived expectations, distinguishing confirmed findings from false positives and ineffective tests.
5. Build and review a causal defect graph that traces observed symptoms to candidate RTL causes without treating model confidence as proof.
6. Evaluate repair candidates using functional tests and invariant checks before comparing minimality, defect closure, functional preservation, and available area measurements.
7. Interpret Pareto-based patch selection and observed-regret stopping without claiming exhaustive correctness from sampled tests.
8. Interpret security assertions and formal counterexamples to propose minimal RTL countermeasures without changing the security requirements.
9. Apply the four formal acceptance checks for proof, nonvacuity, required behavior reachability, and preservation of previously proven assertions.
10. Review accepted edits for unintended behavior and formulate an additional assertion when existing checks miss a corner case.
11. Document baseline and final results, preserve held-out evaluation independence, and explain the limits of simulation, coverage, formal models, and machine-generated explanations.

Prerequisites:

• Basic knowledge of digital logic, finite-state machines, and RTL design using Verilog or SystemVerilog.
• Familiarity with simulation, testbenches, clock and reset behavior, and waveform interpretation.
• Basic Python and command-line skills for running scripts and reviewing generated reports.
• Introductory hardware-security and CWE knowledge is recommended. Familiarity with LLM prompting and SystemVerilog assertions is helpful; the modules introduce their use in the workflows.

Target Audience

Designed for U.S. citizens working in the Department of War, Government, or Government-affiliated employees, industry, as well as college students and faculty. Must register with your organizational email, and will be notified of acceptance within one week of the course start date.

Biography

Dr. Farimah Farahmandi is the Wally Rhines Endowed Professor in Hardware Security in the Department of Electrical and Computer Engineering (ECE) at the University of Florida. She also serves as the Associate Director of the Florida Institute for Cybersecurity (FICS) at the University of Florida. Her research focuses on hardware security verification, formal methods, fault-injection attack analysis, and post-silicon validation and debug, resulting in 7 books and over 140 publications in these fields. Dr. Farahmandi’s research has been sponsored by a variety of leading companies and government agencies. For her contributions, she is a recipient of 7 best paper and nomination awards, and was recognized with the ACM/IEEE DAC Under 40 Innovators Award (2024), the Best Assistant Professor Award at the University of Florida (2024), the Excellence in Service Award (2023), and the Excellence in Research Award (2022) from the ECE department at UF. She also received the prestigious Young Faculty Award from SRC (2022) and the NSF CAREER Award.