@inproceedings{fa218e83748e4f0d8ea48ef21b377f89,
title = "The K2 Architecture for Trustworthy Hardware Security Modules",
abstract = "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.",
keywords = "security, verification",
author = "Anish Athalye and Frans Kaashoek and Nickolai Zeldovich and Joseph Tassarotti",
note = "Publisher Copyright: {\textcopyright} 2023 Owner/Author(s).; 1st Workshop on Kernel Isolation, Safety and Verification, KISV 2023 ; Conference date: 23-10-2023",
year = "2023",
month = oct,
day = "23",
doi = "10.1145/3625275.3625402",
language = "English (US)",
series = "KISV 2023 - Proceedings of the1st Workshop on Kernel Isolation, Safety and Verification",
publisher = "Association for Computing Machinery, Inc",
pages = "26--32",
booktitle = "KISV 2023 - Proceedings of the1st Workshop on Kernel Isolation, Safety and Verification",
}