More Like this

1. Verifying Hardware Security Modules with Information-Preserving Refinement

   Athalye, Anish; Kaashoek, M. Frans; Zeldovich, Nickolai (July 2022, Proceedings of the 16th USENIX Symposium on Operating Systems Design and Implementation (OSDI 2022))

   Knox is a new framework that enables developers to build hardware security modules (HSMs) with high assurance through formal verification. The goal is to rule out all hardware bugs, software bugs, and timing side channels. Knox's approach is to relate an implementation's wire-level behavior to a functional specification stated in terms of method calls and return values with a new definition called information-preserving refinement (IPR). This definition captures the notion that the HSM implements its functional specification, and that it leaks no additional information through its wire-level behavior. The Knox framework provides support for writing specifications, importing HSM implementations written in Verilog and C code, and proving IPR using a combination of lightweight annotations and interactive proofs. To evaluate the IPR definition and the Knox framework, we verified three simple HSMs, including an RFC 6238-compliant TOTP token. The TOTP token is written in 2950 lines of Verilog and 360 lines of C and assembly. Its behavior is captured in a succinct specification: aside from the definition of the TOTP algorithm, the spec is only 10 lines of code. In all three case studies, verification covers entire hardware and software stacks and rules out hardware/software bugs and timing side channels. 

   more » « less
2. Survey of Approaches and Techniques for Security Verification of Computer Systems

   https://doi.org/10.1145/3564785  

   Erata, Ferhat; Deng, Shuwen; Zaghloul, Faisal; Xiong, Wenjie; Demir, Onur; Szefer, Jakub (January 2023, ACM Journal on Emerging Technologies in Computing Systems)

   This article surveys the landscape of security verification approaches and techniques for computer systems at various levels: from a software-application level all the way to the physical hardware level. Different existing projects are compared, based on the tools used and security aspects being examined. Since many systems require both hardware and software components to work together to provide the system’s promised security protections, it is not sufficient to verify just the software levels or just the hardware levels in a mutually exclusive fashion. This survey especially highlights system levels that are verified by the different existing projects and presents to the readers the state of the art in hardware and software system security verification. Few approaches come close to providing full-system verification, and there is still much room for improvement. 

   more » « less
3. Hardware and Software Co-Verification from Security Perspective

   https://doi.org/10.1109/MTV48867.2019.00018  

   Chen, Kejun; Deng, Qingxu; Hou, Yumin; Jin, Yier; Guo, Xiaolong (December 2019, 2019 20th International Workshop on Microprocessor/SoC Test, Security and Verification (MTV))

   Attacks which combine software vulnerabilities and hardware vulnerabilities are emerging security problems. Although the runtime verification or remote attestation can determine the correctness of a system, existing methods suffer from inflexible security policy setup and high performance overheads. Meanwhile, they rarely focus on addressing the threat in the RISC-V architecture, which provides an open Instruction Set Architecture (ISA) of the processsor. In this paper, we propose a comprehensive software and hardware co-verification method to protect the entire RISC-V system in the runtime. The proposed method adopts the Dynamic Information Flow Tracking (DIFT) framework to implement a new Verifier and Prover security architecture for supporting runtime software and hardware coverification. We realize a FPGA prototype on the Rocket-Chip, an RISC-V open-source processor core. The framework is implemented as a co-processor which do not change the architecture of main processor core and the new security architecture can be integrated with other RISC-V processors. 

   more » « less
4. Bridging Hardware and Software Through Causality Inference

   Liu, Zhaoxiang; Chen, Kejun; Sullivan, Dean; Arias, Orlando; Guo, Xiaolong (April 2024, New England Hardware Security Days)

   We propose Microscope, a new framework that addresses growing security issues in System-on-Chip (SoC) designs due to their complexity and involvement of third-party vendors. Traditional methods are inadequate for identifying software-exploited hardware vulnerabilities, and existing solutions for hardware-software co-verification often fall short. The framework has been proven effective through extensive testing on SoC benchmarks, and it has outperformed existing methods and commercial tools in comparative analyses. Index Terms—Causality Inference, Hardware Security, 

   more » « less
5. Practical and Scalable Security Verification of Secure Architectures

   https://doi.org/10.1145/3505253.3505256  

   Zhang, Tianwei; Szefer, Jakub; Lee, Ruby B. (October 2021, Hardware and Architectural Support for Security and Privacy)

   We present a new and practical framework for security verification of secure architectures. Specifically, we break the verification task into external verification and internal verification. External verification considers the external protocols, i.e. interactions between users, compute servers, network entities, etc. Meanwhile, internal verification considers the interactions between hardware and software components within each server. This verification framework is general-purpose and can be applied to a stand-alone server, or a large-scale distributed system. We evaluate our verification method on the CloudMonatt and HyperWall architectures as examples. 

   more » « less