David Chisnall

Photo by Will Harwood

Address University of Cambridge
William Gates Building
15 JJ Thomson Avenue
Cambridge CB3 1FD
United Kingdom
Office: GE10, William Gates Building
Telephone: +44 (0)1223 763 776
Fax: +44 (0)1223 334 678
E-mail: David.Chisnall AT cl.cam.ac.uk

I am a Visiting Researcher in the Computer Lab.

Research Interests

  • Cross-language interoperability
  • Hardware / language co-design
  • Safety in unsafe languages

Former teaching responsibilities

Open source

Recent Publications

A full list is available on the publications page.

  1. Nathaniel Wesley Filardo, Brett F. Gutstein, Jonathan Woodruff, Jessica Clarke, Peter Rugg, Brooks Davis, Mark Johnston, Robert Norton, David Chisnall, Simon W. Moore, Peter G. Neumann and Robert N. M. Watson. Cornucopia Reloaded: Load Barriers for CHERI Heap Temporal Safety. Proceedings of the 29th ACM International Conference on Architectural Support for Programming Languages and Operating Systems (ASPLOS’24), (2024). [pdf] [doi]
      title = {{Cornucopia Reloaded: Load Barriers for CHERI Heap Temporal
      author = {Filardo, Nathaniel Wesley and Gutstein, Brett F. and Woodruff, Jonathan and Clarke, Jessica and Rugg, Peter and Davis, Brooks and Johnston, Mark and Norton, Robert and Chisnall, David and Moore, Simon W. and Neumann, Peter G. and Watson, Robert N. M.},
      doi = {10.1145/3620665.3640416},
      booktitle = {Proceedings of the 29th ACM International Conference on
                  Architectural Support for Programming Languages and Operating
                  Systems (ASPLOS’24)},
      year = {2024},
      month = aug,
      pdf = {https://www.ietfng.org/nwf/_downloads/5827e22fd2720e88960bdec554bfad39/2024-cornucopia-reloaded.pdf}
  2. Vadim Zaliva, Kayvan Memarian, Ricardo Almeida, Jessica Clarke, Brooks Davis, Alex Richardson, David Chisnall, Brian Campbell, Ian Stark, Robert N. M. Watson and Peter Sewell. Formal Mechanised Semantics of CHERI C: Capabilities, Provenance, and Undefined Behaviour. (2024). [pdf]
      author = {Zaliva, Vadim and Memarian, Kayvan and Almeida, Ricardo and Clarke, Jessica and Davis, Brooks and Richardson, Alex and Chisnall, David and Campbell, Brian and Stark, Ian and Watson, Robert N. M. and Sewell, Peter},
      title = {Formal Mechanised Semantics of {CHERI C}: Capabilities, Provenance, and Undefined Behaviour},
      conf = {ASPLOS 2024},
      year = {2024},
      pdf = {http://www.cl.cam.ac.uk/users/pes20/asplos24spring-paper110.pdf}

    Memory safety issues are a persistent source of security vulnerabilities, with conventional architectures and the C codebase chronically prone to exploitable errors. The CHERI research project has shown how one can provide radically improved security for that existing codebase with minimal modification, using unforgeable hardware capabilities in place of machine-word pointers in CHERI dialects of C, implemented as adaptions of Clang/LLVM and GCC. CHERI was first prototyped as extensions of MIPS and RISC-V; it is currently being evaluated by Arm and others with the Arm Morello experimental architecture, processor, and platform, to explore its potential for mass-market adoption, and by Microsoft in their CHERIoT design for embedded cores.

    There is thus considerable practical experience with CHERI C implementation and use, but exactly what CHERI C’s semantics is (or should be) remains an open question. In this paper, we present the first attempt to rigorously and comprehensively define CHERI C semantics, discuss key semantics design questions relating to capabilities, provenance, and undefined behaviour, and clarify them with semantics in multiple complementary forms: in prose, as an executable semantics adapting the Cerberus C semantics, and mechanised in Coq.

    This establishes a solid foundation for CHERI C, for those porting code to it, for compiler implementers, and for future semantics and verification.

  3. Luke Cheeseman, Matthew J. Parkinson, Sylvan Clebsch, Marios Kogias, Sophia Drossopoulou, David Chisnall, Tobias Wrigstad and Paul Liétar. When Concurrency Matters: Behaviour-Oriented Concurrency. Proc. ACM Program. Lang. 7, OOPSLA2 (2023). [doi]
      author = {Cheeseman, Luke and Parkinson, Matthew J. and Clebsch, Sylvan and Kogias, Marios and Drossopoulou, Sophia and Chisnall, David and Wrigstad, Tobias and Li\'{e}tar, Paul},
      title = {When Concurrency Matters: Behaviour-Oriented Concurrency},
      year = {2023},
      issue_date = {October 2023},
      publisher = {Association for Computing Machinery},
      address = {New York, NY, USA},
      volume = {7},
      number = {OOPSLA2},
      url = {https://doi.org/10.1145/3622852},
      doi = {10.1145/3622852},
      journal = {Proc. ACM Program. Lang.},
      month = oct,
      articleno = {276},
      numpages = {30},
      keywords = {actors}

    Expressing parallelism and coordination is central for modern concurrent programming. Many mechanisms exist for expressing both parallelism and coordination. However, the design decisions for these two mechanisms are tightly intertwined. We believe that the interdependence of these two mechanisms should be recognised and achieved through a single, powerful primitive. We are not the first to realise this: the prime example is actor model programming, where parallelism arises through fine-grained decomposition of a program’s state into actors that are able to execute independently in parallel. However, actor model programming has a serious pain point: updating multiple actors as a single atomic operation is a challenging task. We address this pain point by introducing a new concurrency paradigm: Behaviour-Oriented Concurrency (BoC). In BoC, we are revisiting the fundamental concept of a behaviour to provide a more transactional concurrency model. BoC enables asynchronously creating atomic and ordered units of work with exclusive access to a collection of independent resources. In this paper, we describe BoC informally in terms of examples, which demonstrate the advantages of exclusive access to several independent resources, as well as the need for ordering. We define it through a formal model. We demonstrate its practicality by implementing a C++ runtime. We argue its applicability through the Savina benchmark suite: benchmarks in this suite can be more compactly represented using BoC in place of Actors, and we observe comparable, if not better, performance.

  4. 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]
      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}

    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.

  5. Hugo Lefeuvre, David Chisnall, Marios Kogias and Pierre Olivier. Towards (Really) Safe and Fast Confidential I/O. HotOS XIX, (2023). [doi]
      title = {Towards (Really) Safe and Fast Confidential I/O},
      author = {Lefeuvre, Hugo and Chisnall, David and Kogias, Marios and Olivier, Pierre},
      booktitle = {HotOS XIX},
      year = {2023},
      month = jun,
      doi = {10.1145/3593856.3595913}

    Confidential cloud computing enables cloud tenants to distrust their service provider. Achieving confidential computing solutions that provide concrete security guarantees requires not only strong mechanisms, but also carefully designed interfaces. In this paper, we make the observation that confidential I/O interfaces, caught in the tug-of-war between performance and security, fail to address both at a time when confronted to interface vulnerabilities and observability. We expose the problem of safe I/O interfaces in confidential computing, its implications and challenges, and devise research paths to achieve confidential I/O interfaces that are both safe and fast.