Download a complete list of publications as BibTeX

Contents

Articles

  1. Anna Lena Duque Antón, Johannes Müller, Philipp Schmitz, Tobias Jauch, Alex Wezel, Lucas Deutschmann, Mohammad Rahmani Fadiheh, Dominik Stoffel and Wolfgang Kunz. VeriCHERI: Exhaustive Formal Security Verification of CHERI at the RTL. Accepted for publication at the 43rd International Conference on Computer-Aided Design (ICCAD ‘24), Association for Computing Machinery (2024). [doi]
    BibTeX 
    @inproceedings{vericheri2024,
  author = {Duque Ant{\'o}n, Anna Lena and M{\"u}ller, Johannes and Schmitz, Philipp and Jauch, Tobias and Wezel, Alex and Deutschmann, Lucas and Fadiheh, Mohammad Rahmani and Stoffel, Dominik and Kunz, Wolfgang},
  title = {VeriCHERI: Exhaustive Formal Security Verification of CHERI at the RTL},
  doi = {https://doi.org/10.1145/3676536.3676841},
  year = {2024},
  month = oct,
  location = {New York, USA},
  publisher = {Association for Computing Machinery},
  booktitle = {Accepted for publication at the 43rd International Conference on Computer-Aided Design (ICCAD `24)}
}
    Abstract

    Protecting data in memory from attackers continues to be a concern in computing systems. CHERI is a promising approach to achieve such protection, by providing and enforcing fine-grained memory protection directly in the hardware. Creating trust for the entire system stack, however, requires a gap-free verification of CHERI’s hardware-based protection mechanisms. Existing verification methods for CHERI target the abstract ISA model rather than the underlying hardware implementation. Fully ensuring the CHERI security guarantees for a concrete RTL implementation is a challenge in previous flows and demands high manual efforts. This paper presents VeriCHERI, a novel approach to security verification. It is conceptionally different from previous works in that it does not require any ISA specification. Instead of checking compliance with a golden ISA model, we check against well-established global security objectives of confidentiality and integrity. Fully covering these objectives, VeriCHERI uses as few as four unbounded properties to exhaustively prove or disprove any vulnerability. We demonstrate the effectiveness and scalability of VeriCHERI on a RISC-V based processor implementing a CHERI variant.

  2. Saar Amar, David Chisnall, Tony Chen, Nathaniel Filardo Wesley, Ben Laurie, Kunyan Liu, Robert Norton, Simon W. Moore, Yucong Tao, Robert N. M. Watson and Hongyan Xia. CHERIoT: Complete Memory Safety for Embedded Devices. proceedings of the 56th IEEE/ACM International Symposium on Microarchitecture, Association for Computing Machinery (2023). [pdf] [poster] [doi]
    BibTeX 
    @inproceedings{cheriotmicro2023,
  author = {Amar, Saar and Chisnall, David and Chen, Tony and Wesley, Nathaniel Filardo and Laurie, Ben and Liu, Kunyan and Norton, Robert and Moore, Simon W. and Tao, Yucong and Watson, Robert N. M. and Xia, Hongyan},
  title = {{CHERIoT}: Complete Memory Safety for Embedded Devices},
  doi = {https://doi.org/10.1145/3613424.3614266},
  year = {2023},
  month = oct,
  location = {Toronto, Canada},
  publisher = {Association for Computing Machinery},
  booktitle = {proceedings of the 56th IEEE/ACM International Symposium on Microarchitecture},
  pdf = {https://cheriot.org/papers/2023-micro-cheriot-uarch.pdf},
  poster = {https://cheriot.org/papers/2023-11-31-MIRCRO-CHERIoT-Poster.pdf}
}
    Abstract

    The ubiquity of embedded devices is apparent. The desire for increased functionality and connectivity drives ever larger software stacks, with components from multiple vendors and entities. These stacks should be replete with isolation and memory safety technologies, but existing solutions impinge upon development, unit cost, power, scalability, and/or real-time constraints, limiting their adoption and production-grade deployments. As memory safety vulnerabilities mount, the situation is clearly not tenable and a new approach is needed.

    To slake this need, we present a novel adaptation of the CHERI capability architecture, co-designed with a green-field, security-centric RTOS. It is scaled for embedded systems, is capable of fine-grained software compartmentalization, and provides affordances for full inter-compartment memory safety. We highlight central design decisions and offloads and summarize how our prototype RTOS uses these to enable memory-safe, compartmentalized applications. Unlike many state-of-the-art schemes, our solution deterministically (not probabilistically) eliminates memory safety vulnerabilities while maintaining source-level compatibility. We characterize the power, performance, and area microarchitectural impacts, run microbenchmarks of key facilities, and exhibit the practicality of an end-to-end IoT application. The implementation shows that full memory safety for compartmentalized embedded systems is achievable without violating resource constraints or real-time guarantees, and that hardware assists need not be expensive, intrusive, or power-hungry.

Tech Reports

  1. Saar Amar, Tony Chen, David Chisnall, Felix Domke, Nathaniel Filardo, Kunyan Liu, Robert Norton-Wright, Yucong Tao, Robert N. M. Watson and Hongyan Xia. CHERIoT: Rethinking security for low-cost embedded systems. Microsoft, 2023. [pdf]
    BibTeX 
    @techreport{amar2023cheriot,
  author = {Amar, Saar and Chen, Tony and Chisnall, David and Domke, Felix and Filardo, Nathaniel and Liu, Kunyan and Norton-Wright, Robert and Tao, Yucong and N. M. Watson, Robert and Xia, Hongyan},
  title = {CHERIoT: Rethinking security for low-cost embedded systems},
  institution = {Microsoft},
  year = {2023},
  month = feb,
  url = {https://www.microsoft.com/en-us/research/uploads/prod/2023/02/cheriot-63e11a4f1e629.pdf},
  number = {MSR-TR-2023-6}
}
    Abstract

    Small embedded cores have little area to spare for security features and yet must often run code written in unsafe languages and, increasingly, are exposed to the hostile Internet. CHERIoT  (Capability Hardware Extension to RISC-V for Internet of Things) builds on top of CHERI and RISC-V to provide an ISA and software model that lets software depend on object-granularity spatial memory safety, deterministic use-after-free protection, and lightweight compartmentalization exposed directly to the C/C++ language model. This can run existing embedded software components on a clean-slate RTOS that scales up to large numbers of isolated (yet securely communicating) compartments, even on systems with under 256 KiB of SRAM.

Presentations

  1. Kunyan Liu. Introduction to CHERIoT. 2023. [pdf]
    BibTeX 
    @unpublished{riscvsummit2023cheriot,
  title = {Introduction to CHERIoT},
  author = {Liu, Kunyan},
  year = {2023},
  note = {RISC-V Summit},
  pdf = {papers/CHERIoT_riscv_summit2023_final.pdf}
}
  2. David Chisnall and Ben Laurie. Compartmentalisation Workshop. 2023. [pdf] [slides]
    BibTeX 
    @unpublished{dsbd2023compartmentalisationworkshop,
  title = {Compartmentalisation Workshop},
  author = {Chisnall, David and Laurie, Ben},
  year = {2023},
  note = {Digital Security by Design All Hands},
  slides = {https://cheriot.org/papers/2023-11-08-Compartmentalisation-Workshop.pptx},
  pdf = {https://cheriot.org/papers/2023-11-08-Compartmentalisation-Workshop.pdf}
}