VeriChat: 面向硬件安全验证的智能对话式AI助手
VeriChat: An Agentic Conversational AI Assistant for Hardware Security Verification
AI总结：
提出VeriChat，一种基于检索增强的多智能体对话助手，通过三个专业智能体协作减少幻觉，并集成开源EDA工具进行语法检查、综合、仿真和形式验证，在硬件安全验证中达到87.73%的忠实度。
摘要：
硬件安全验证是一个多阶段过程，工程师必须处理复杂的设计分析、威胁考虑和验证策略。他们通常需要以安全为中心的指导，但当前的验证环境对此类辅助提供的结构化支持很少。尽管对话式AI可以提供这种按需辅助，但直接使用像ChatGPT或Gemini这样的通用聊天机器人是有风险的，因为它们倾向于产生幻觉并依赖静态、过时的知识。我们提出了VeriChat，一个领域专用的对话助手，旨在通过提供上下文感知的安全指导来支持（而非取代）现有的验证工作流程。VeriChat采用检索增强的多智能体工作流程，其中三个专业智能体协作，在提高响应透明度和可靠性的同时最小化幻觉。除了问答功能外，VeriChat还集成了开源EDA工具，包括Icarus Verilog、Yosys和SymbiYosys，以直接对用户提供的RTL设计执行语法检查、综合分析、仿真和形式验证。通过全面的方法论评估，VeriChat的忠实度得分为87.73%，显著优于领先的专有模型。我们通过一个AES S-Box IP上的硬件木马检测案例研究来展示该框架，其中VeriChat通过多轮对话工作流程自主识别、仿真并形式证明了一个隐蔽的密钥泄露漏洞。
英文摘要：
Hardware security verification is a multi-stage process in which engineers must navigate complex design analyses, threat considerations, and verification strategies. They often need security-focused guidance, yet current verification environments provide little structured support for such assistance. Although conversational AI could offer such on-demand assistance, directly using general-purpose chatbots like ChatGPT or Gemini is risky due to their tendency to hallucinate and their reliance on static, outdated knowledge. We present VeriChat, a domain-specialized conversational assistant designed to support, rather than replace, existing verification workflows by providing context-aware security guidance. VeriChat employs a retrieval-augmented, multi-agent workflow in which three specialized agents collaboratively minimize hallucinations while improving the transparency and reliability of the response. Beyond question answering, VeriChat integrates open-source EDA tools, including Icarus Verilog, Yosys, and SymbiYosys, to perform syntax checking, synthesis analysis, simulation, and formal verification directly on user-provided RTL designs. Evaluated using a comprehensive methodology, VeriChat achieves a Faithfulness score of 87.73%, significantly outperforming the leading proprietary models. We demonstrate the framework through a hardware Trojan detection case study on an AES S-Box IP, where VeriChat autonomously identifies, simulates, and formally proves a covert key-leakage vulnerability through a multi-turn conversational workflow.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
