权益分类	功能权益	普通用户	{{item.name}}会员
{{category.name}}	{{benefitItem.name}}

Collaborative Research: FMitF: Track I: Property-specific Hardware-oriented Formal Verification Modules for Embedded Systems

合作研究：FMitF：第一轨：嵌入式系统的面向属性的硬件形式验证模块

基本信息

批准号：
2019310
负责人：
Xiaolong Guo
金额：
$ 25万
依托单位：
Kansas State University
依托单位国家：
美国
项目类别：
Standard Grant
财政年份：
2020
资助国家：
美国
起止时间：
2020-10-01 至 2024-09-30
项目状态：
已结题

来源：
https://www.nsf.gov/awardsearch/showAward?AWD_ID=2019310&HistoricalAwards=false
关键词：
Collaborative Research FMitF Track Property

项目摘要

With the Internet of Things and Cyber-Physical Systems being used in a broad range of applications such as smart homes, smart infrastructure, and smart health, a rigorous analysis of both hardware and software became critical in ensuring safety and security of these systems. Recently discovered micro-architectural side channels in Intel processors has demonstrated the need for a deep understanding of the interaction between software and hardware. However, hardware/software co-verification is challenging due to the complexity of both hardware and software. The project novelties include a property-directed co-model extraction and a property-specific run-time validation methodology to achieve scalability and precision in detecting bugs due to hardware/software interactions. If successful, the developed methodologies and automation tools will empower embedded-system vendors with tools that can detect security and safety vulnerabilities early in design. The project’s impacts on workforce training and broadening participation in formal methods and embedded-system security will be achieved through the investigators’ courses on formal verification and embedded-system development and security, outreach events, and collaborations with industry. The project will result in a set of system-level benchmarks to demonstrate various cases of hardware software interactions leading to security and safety violations. To achieve these goals, the project will be built on three research thrusts. 1) Property-driven Hardware/Software Co-Model Extraction: A failure property is decomposed into hardware- and software-relevant parts to drive localization of the software and hardware features relevant to the property. State exploration on the combined state space of the hardware and software will be performed only when required directly by the property. The result of this incremental and property-directed search is the extraction of failure conditions that describe the software contexts in which certain hardware and software properties should be monitored. 2) Low Overhead Property-Specific Hardware Monitors: An off-chip dynamic information-flow tracking module will be implemented leveraging an open-source RISC V processor core. The collected run-time data will be used for enforcing user policies as well as for detecting user-specified failure properties. 3) Reconfigurable Hardware Decision Modules: A configurable interface will be developed for the data exchange between the off-chip dynamic information-flow tracking module and the main processor. The failure conditions generated by the co-model extraction tool will inform the configuration of this interface. The instruction-set architecture will be extended to define new instructions for guiding and configuring the run-time checker.This award reflects NSF's statutory mission and has been deemed worthy of support through evaluation using the Foundation's intellectual merit and broader impacts review criteria.

随着物联网和网络物理系统被广泛应用于智能家居、智能基础设施和智能健康等领域，对硬件和软件的严格分析对于确保这些系统的安全至关重要。最近在英特尔处理器中发现的微架构侧通道表明，需要深入了解软件和硬件之间的交互。然而，由于硬件和软件的复杂性，硬件/软件协同验证是具有挑战性的。该项目的新颖之处包括属性导向的协同模型提取和属性特定的运行时验证方法，以实现可扩展性和精度检测由于硬件/软件交互的错误。如果成功，开发的方法和自动化工具将使嵌入式系统供应商能够在设计早期检测安全和安全漏洞。该项目对劳动力培训和扩大正式方法和嵌入式系统安全参与的影响将通过调查人员关于正式核查和嵌入式系统开发和安全的课程、外联活动以及与业界的合作来实现。该项目将产生一套系统一级的基准，以展示导致违反安保和安全规定的各种软硬件互动情况。为了实现这些目标，该项目将建立在三个研究重点之上。1)属性驱动的硬件/软件协同模型提取：故障属性被分解为硬件和软件相关部分，以驱动与该属性相关的软件和硬件功能的本地化。仅当属性直接要求时，才执行硬件和软件组合状态空间上的状态探索。这种增量和属性导向搜索的结果是提取故障条件，这些故障条件描述了应监控某些硬件和软件属性的软件上下文。2)低开销的特定于属性的硬件支持：一个片外动态信息流跟踪模块将利用开源RISC V处理器核心来实现。收集的运行时数据将用于强制执行用户策略以及检测用户指定的故障属性。3)可重构硬件决策模块：将开发一个可配置的接口，用于片外动态信息流跟踪模块和主处理器之间的数据交换。由协同模型提取工具生成的故障条件将通知此接口的配置。该奖项反映了NSF的法定使命，并已被认为是值得的支持，通过评估使用基金会的智力价值和更广泛的影响审查标准。

项目成果

期刊论文数量（9）

专著数量（0）

科研奖励数量（0）

会议论文数量（0）

专利数量（0）

Graph Neural Network based Hardware Trojan Detection at Intermediate Representative for SoC Platforms

DOI：
10.1145/3526241.3530827
发表时间：
2022-06
期刊：
Proceedings of the Great Lakes Symposium on VLSI 2022
影响因子：
0
作者：
Weimin Fu;H. Yu;Orlando Arias;Kaichen Yang;Yier Jin;Tuba Yavuz;Xiaolong Guo
通讯作者：
Weimin Fu;H. Yu;Orlando Arias;Kaichen Yang;Yier Jin;Tuba Yavuz;Xiaolong Guo

Microscope: Causality Inference Crossing the Hardware and Software Boundary from Hardware Perspective

显微镜：从硬件角度跨越软硬件界限的因果推理

DOI：
发表时间：
2024
期刊：
Proceedings of the ASPDAC Asia and South Pacific Design Automation Conference
影响因子：
0
作者：
Liu, Zhaoxiang;Chen, Kejun;Sullivan, Dean;Arias, Orlando;Dutta, Raj Gautam;Jin, Yier;Guo, Xiaolong
通讯作者：
Guo, Xiaolong

LLM4SecHW: Leavering Domain-Specific Large Language Model for Hardware Debugging

LLM4SecHW：用于硬件调试的特定领域大型语言模型