More Like this

1. QuickSilver: modeling and parameterized verification for distributed agreement-based systems

   https://doi.org/10.1145/3485534  

   Jaber, Nouraldin; Wagner, Christopher; Jacobs, Swen; Kulkarni, Milind; Samanta, Roopsha (October 2021, Proceedings of the ACM on Programming Languages)

   The last decade has sparked several valiant efforts in deductive verification of distributed agreement protocols such as consensus and leader election. Oddly, there have been far fewer verification efforts that go beyond the core protocols and target applications that are built on top of agreement protocols. This is unfortunate, as agreement-based distributed services such as data stores, locks, and ledgers are ubiquitous and potentially permit modular, scalable verification approaches that mimic their modular design. We address this need for verification of distributed agreement-based systems through our novel modeling and verification framework, QuickSilver, that is not only modular, but also fully automated. The key enabling feature of QuickSilver is our encoding of abstractions of verified agreement protocols that facilitates modular, decidable, and scalable automated verification. We demonstrate the potential of QuickSilver by modeling and efficiently verifying a series of tricky case studies, adapted from real-world applications, such as a data store, a lock service, a surveillance system, a pathfinding algorithm for mobile robots, and more. 

   more » « less
2. 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
3. The K2 Architecture for Trustworthy Hardware Security Modules

   https://doi.org/10.1145/3625275.3625402  

   Athalye, Anish; Kaashoek, Frans; Zeldovich, Nickolai; Tassarotti, Joseph (October 2023, ACM)

   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
4. Automated Generation of Security Assertions for RTL Models

   https://doi.org/10.1145/3565801  

   Witharana, Hasini; Jayasena, Aruna; Whigham, Andrew; Mishra, Prabhat (January 2023, ACM Journal on Emerging Technologies in Computing Systems)

   System-on-Chip (SoC) security is vital in designing trustworthy systems. Detecting and fixing a vulnerability in the early stages is easier and cost-effective. Assertion-based verification is widely used for functional validation of Register-Transfer Level (RTL) designs. Assertions can improve the controllability and observability that can lead to faster error detection and localization. Although assertions are widely used for functional validation of RTL models, there is limited effort in applying assertions to detect SoC security vulnerabilities. Specifically, a fundamental challenge in SoC security and trust validation is how to develop high-quality security assertions. In this article, we perform automated vulnerability analysis of RTL models to generate security assertions for six classes of vulnerabilities. Experimental results show that the generated security assertions can detect a wide variety of vulnerabilities. Our automated framework can drastically reduce the overall security validation effort compared to the manual development of security assertions. Automated generation of security assertions will enable assertion-based verification to be one of the most promising pre-silicon security sign-off solutions. 

   more » « less
5. Universally Composable Security

   https://doi.org/10.1145/3402457  

   Canetti, Ran (October 2020, Journal of the ACM)

   null (Ed.)

   This work presents a general framework for describing cryptographic protocols and analyzing their security. The framework allows specifying the security requirements of practically any cryptographic task in a unified and systematic way. Furthermore, in this framework the security of protocols is preserved under a general composition operation, called universal composition. The proposed framework with its security-preserving composition operation allows for modular design and analysis of complex cryptographic protocols from simpler building blocks. Moreover, within this framework, protocols are guaranteed to maintain their security in any context, even in the presence of an unbounded number of arbitrary protocol sessions that run concurrently in an adversarially controlled manner. This is a useful guarantee, which allows arguing about the security of cryptographic protocols in complex and unpredictable environments such as modern communication networks. 

   more » « less