所有人工,更少智能:形式验证透视下的 GenAI
FormAI 数据集利用动态零 - shot 提示技术构建,包含 11.2 万个 AI 生成的可以编译和独立运行的 C 程序,按漏洞类型进行了分类,并采用 SMT-based Bounded Model Checker 方法进行了验证,检测出漏洞并提供反例,用于评估各种静态和动态分析工具的效果以及用于训练大型语言模型和机器学习算法。
Jul, 2023
本研究探讨了使用自然语言提示生成 SystemVerilog 声明(用于硬件安全),研究了一种流行的大型语言模型的能力,并设计了一个评估框架来生成各种提示并创建基准套件,该套件由真实硬件设计和相应的黄金参考声明组成。
Jun, 2023
下一代 AI 系统需要强有力的安全保证。本报告研究了神经网络和相关内存安全性质的软件实现,包括空指针引用、越界访问、double-free 和内存泄漏。我们旨在检测这些漏洞,并借助大型语言模型自动修复它们。为此,我们首先通过程序突变的自动化过程,将现有的神经网络代码数据集 NeuroCodeBench 的规模扩大到约 81k 个程序。然后,我们使用最先进的软件验证器 ESBMC 验证突变的神经网络实现的内存安全性。每当 ESBMC 发现漏洞时,我们会调用一个大型语言模型来修复源代码。在最新的任务中,我们比较了各种最先进的提示工程技术,以及重复调用大型语言模型的迭代方法的性能。
May, 2024
现代计算框架的复杂性不断增加,导致从业人员向国家漏洞数据库(NVD)报告的网络安全漏洞激增。尽管 NVD 具有提供最新洞察的重要性,但在没有适用的技术方法的情况下,从如此大量的非结构化数据中提取有意义的趋势仍然具有挑战性。该研究提出了一种综合策略,包括解决漏洞、分数预测和从 CWE 和 CVE 数据库中提取相关洞察的知识生成系统。为了应对物联网设备的硬件攻击不断增长的问题,作者提出了基于机器学习的硬件漏洞到弱点映射(HW-V2W-Map)框架,该框架使用本体驱动叙事框架自动更新本体以识别漏洞随时间的演变趋势,并提供解决漏洞的方法。该框架还利用生成式预训练转换器(GPT)大型语言模型提供解决方案建议。
Dec, 2023
通过检查以测试为基础的验证和验证作为最实用的方法,并总结当前先进的方法学,在确保学习能力的 CPS 的形式安全方面,确定了当前测试方法的局限性,并提出了从基础概率测试过渡到更严格方法的路线图,以提供正式保证。
Nov, 2023
通过对 AI 软件系统中深度学习技术的脆弱性进行系统研究,我们提出了一个两流数据分析框架,探索各种数据库中的脆弱性模式,并进行了大规模实证研究来理解脆弱性的模式和修复中的挑战,以推进安全的深度学习系统的发展。
Jun, 2024
通过在 Verilog 数据集上微调现有的 Large Language Models(LLMs),我们探索了使用 LLMs 自动生成高质量的 Verilog 代码的能力。微调后的开源 CodeGen-16B 模型在功能正确性上优于最先进的商业 GPT-3.5-turbo 模型,并在多样化和复杂的问题集中表现出竞争性能,尤其在某些场景下显示了对生成正确 Verilog 代码的潜力,突出了内部小型 LLMs 在硬件设计自动化方面的潜力。
Jul, 2023
介绍了 LLM4SecHW,这是一个利用领域特定的大型语言模型(LLM)的硬件调试新框架。通过收集开源硬件设计缺陷和纠正步骤的版本控制数据,利用精调的中型 LLM 模型,能够准确地识别和修复硬件设计缺陷,实现自动控制硬件质量控制流程。
Jan, 2024
现代计算系统在硬件作为信任根基上依赖较重。然而,不断增加的复杂性导致了跨层攻击可以利用的安全关键弱点。我们提出了一种新颖的基于 ML 的硬件模糊测试工具 ChatFuzz,它利用类似 ChatGPT 的 LLMs 来理解处理器语言,并通过代码覆盖度度量指标引导输入生成,以此解决现有工具在实际时间范围内无法全面覆盖复杂硬件设计的问题。在测试中,与最先进的模糊测试工具相比,ChatFuzz 在仅 52 分钟内达到了 75% 的条件覆盖率,而后者需要 30 个小时的时间窗口才能达到类似的覆盖率。此外,我们的工具在 130 个小时的时间范围内,仅提供有限的 10 个模拟实例 / 许可证情况下即可达到 80% 的覆盖率。在此期间,共进行了 19.9 万个测试用例,其中 6 千个测试用例与处理器的黄金模型产生了差异。我们的分析发现了 10 多个独特的不匹配之处,包括 RocketCore 中的两个新 bug 和与 RISC-V ISA 模拟器的差异。
Apr, 2024
本文总结了当前硬件设计中人工智能和机器学习技术的应用现状以及挑战,针对电路设计存在的安全问题,提出了安全意识 CAD/EDA 的研究方向和需求。
Apr, 2022