A technical paper titled “The K2 Architecture for Trustworthy Hardware Security Modules” was published by researchers at MIT Computer Science and Artificial Intelligence Laboratory (CSAIL) and New York University.
“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.”
Find the technical paper here. Published October 2023.
Athalye, Anish, Frans Kaashoek, Nickolai Zeldovich, and Joseph Tassarotti. “The K2 Architecture for Trustworthy Hardware Security Modules.” In Proceedings of the 1st Workshop on Kernel Isolation, Safety and Verification, pp. 26-32. 2023.
Related Reading
New Concepts Required For Security Verification
Why it’s so difficult to ensure that hardware works correctly and is capable of detecting vulnerabilities that may show up in the field.
Verification And Test Of Safety And Security
Functional verification is being stretched beyond its capabilities to ensure safe and secure systems. New support is coming from hardware and software.
Leave a Reply