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

Kansas State University, Manhattan KS

Investigators

Abstract

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.