An official website of the United States government
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
Modular Verification of Secure and Leakage-Free Systems: From Application Specification to Circuit-Level Implementation
Parfait is a framework for proving that an implementation of a hardware security module (HSM) leaks nothing more than what is mandated by an application specification. Parfait proofs cover the software and the hardware of an HSM, which catches bugs above the cycle-level digital circuit abstraction, including timing side channels. Parfait's contribution is a scalable approach to proving security and non-leakage by using intermediate levels of abstraction and relating them with transitive information-preserving refinement. This enables Parfait to use different techniques to verify the implementation at different levels of abstraction, reuse existing verified components such as CompCert, and automate parts of the proof, while still providing end-to-end guarantees. We use Parfait to verify four HSMs, including an ECDSA certificate-signing HSM and a password-hashing HSM, on top of the OpenTitan Ibex and PicoRV32 processors. Parfait provides strong guarantees for these HSMs: for instance, it proves that the ECDSA-on-Ibex HSM implementation---2,300 lines of code and 13,500 lines of Verilog---leaks nothing more than what is allowed by a 40-line specification of its behavior.
more »
« less
- Award ID(s):
- 2225441
- PAR ID:
- 10609813
- Publisher / Repository:
- ACM
- Date Published:
- ISBN:
- 9798400712517
- Page Range / eLocation ID:
- 655 to 672
- Format(s):
- Medium: X
- Location:
- Austin TX USA
- Sponsoring Org:
- National Science Foundation
More Like this
-
-
K2 is a new architecture and verification approach for hardware security modules (HSMs). The K2 architecture's rigid separation between I/O, storage, and computation over secret state enables modular proofs and allows for software development and verification independent of hardware development and verification while still providing correctness and security guarantees about the composed system. For a key step of verification, K2 introduces a new tool called Chroniton that automatically proves timing properties of software running on a particular hardware implementation, ensuring the lack of timing side channels at a cycle-accurate level.more » « less
-
Hypervisors are widely deployed by cloud computing providers to support virtual machines, but their growing complexity poses a security risk, as large codebases contain many vulnerabilities. We present SeKVM, a layered Linux KVM hypervisor architecture that has been formally verified on multiprocessor hardware. Using layers, we isolate KVM's trusted computing base into a small core such that only the core needs to be verified to ensure KVM's security guarantees. Using layers, we model hardware features at different levels of abstraction tailored to each layer of software. Lower hypervisor layers that configure and control hardware are verified using a novel machine model that includes multiprocessor memory management hardware such as multi-level shared page tables, tagged TLBs, and a coherent cache hierarchy with cache bypass support. Higher hypervisor layers that build on the lower layers are then verified using a more abstract and simplified model, taking advantage of layer encapsulation to reduce proof burden. Furthermore, layers provide modularity to reduce verification effort across multiple implementation versions. We have retrofitted and verified multiple versions of KVM on Arm multiprocessor hardware, proving the correctness of the implementations and that they contain no vulnerabilities that can affect KVM's security guarantees. Our work is the first machine-checked proof for a commodity hypervisor using multiprocessor memory management hardware. SeKVM requires only modest KVM modifications and incurs only modest performance overhead versus unmodified KVM on real application workloads.more » « less
-
Concurrent systems software is widely-used, complex, and error-prone, posing a significant security risk. We introduce VRM, a new framework that makes it possible for the first time to verify concurrent systems software, such as operating systems and hypervisors, on Arm relaxed memory hardware. VRM defines a set of synchronization and memory access conditions such that a program that satisfies these conditions can be mostly verified on a sequentially consistent hardware model and the proofs will automatically hold on relaxed memory hardware. VRM can be used to verify concurrent kernel code that is not data race free, including code responsible for managing shared page tables in the presence of relaxed MMU hardware. Using VRM, we verify the security guarantees of a retrofitted implementation of the Linux KVM hypervisor on Arm. For multiple versions of KVM, we prove KVM's security properties on a sequentially consistent model, then prove that KVM satisfies VRM's required program conditions such that its security proofs hold on Arm relaxed memory hardware. Our experimental results show that the retrofit and VRM conditions do not adversely affect the scalability of verified KVM, as it performs similar to unmodified KVM when concurrently running many multiprocessor virtual machines with real application workloads on Arm multiprocessor server hardware. Our work is the first machine-checked proof for concurrent systems software on Arm relaxed memory hardware.more » « less
-
null (Ed.)High sulfur-content materials (HSMs) have been investigated for a plethora of applications owing to a combination of desirable properties and the low cost of waste sulfur as a starting monomer. Whereas extended sulfur catenates are unstable with respect to orthorhombic sulfur (S 8 rings) at STP, oligomeric/polymeric sulfur chains can be stabilized when they are confined in a supporting matrix. The vast majority of reported HSMs have been made by inverse vulcanization of sulfur and olefins. In the current case, a radical aryl halide–sulfur polymerization (RASP) route was employed to form an HSM ( XS81 ) by copolymerizing elemental sulfur with the xylenol derivative 2,4-dimethyl-3,5-dichlorophenol (DDP). XS81 is a composite of which 81 wt% is sulfur, wherein the sulfur is distributed between cross-linking chains averaging four sulfur atoms in length and trapped sulfur that is not covalently attached to the network. XS81 (flexural strength = 2.0 MPa) exhibits mechanical properties on par with other HSMs prepared by inverse vulcanization. Notably, XS81 retains mechanical integrity over many heat-recast cycles, making it a candidate for facile recyclability. This is the first report of an HSM comprising stabilized polymeric sulfur that has been successfully prepared from a small molecular comonomer by RASP. Preparation of XS81 thus demonstrates a new route to access HSMs using small molecular aryl halides, a notable expansion beyond the olefins required for the well-studied inverse vulcanization route to HSMs from small molecular comonomers.more » « less
- Free Publicly Accessible Full Text
-
Accepted Manuscript1.0
- Conference Paper:
- https://doi.org/10.1145/3694715.3695956
