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

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

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.