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 Principal Researcher in the Confidential Computing Group at Microsoft Research Cambridge, where I work at the intersection of computer architecture, operating systems, programming language design, and security. I am also a Visiting Researcher in the Computer Lab.

Research Interests

  • Cross-language interoperability
  • Hardware / language co-design
  • High-performance garbage collection
  • Safety in unsafe languages

Former teaching responsibilities

Open source work


Recent Publications

A full list is available on the publications page.

  1. Brooks Davis, Robert N. M. Watson, Alexander Richardson, Peter G. Neumann, Simon W. Moore, John Baldwin, David Chisnall, James Clarke, Nathaniel Wesley Filardo, Khilan Gudka, Alexandre Joannou, Ben Laurie, A. Theodore Markettos, J. Edward Maste, Alfredo Mazzinghi, Edward Tomasz Napierala, Robert M. Norton, Michael Roe, Peter Sewell, Stacey Son and Jonathan Woodruff. CheriABI: Enforcing Valid Pointer Provenance and Minimizing Pointer Privilege in the POSIX C Run-time Environment. Proceedings of the Twenty-Fourth International Conference on Architectural Support for Programming Languages and Operating Systems, ACM (2019), 379–393. [pdf]
    @inproceedings{davis2019cheriabi,
      author = {Davis, Brooks and Watson, Robert N. M. and Richardson, Alexander and Neumann, Peter G. and Moore, Simon W. and Baldwin, John and Chisnall, David and Clarke, James and Filardo, Nathaniel Wesley and Gudka, Khilan and Joannou, Alexandre and Laurie, Ben and Markettos, A. Theodore and Maste, J. Edward and Mazzinghi, Alfredo and Napierala, Edward Tomasz and Norton, Robert M. and Roe, Michael and Sewell, Peter and Son, Stacey and Woodruff, Jonathan},
      title = {{CheriABI: Enforcing Valid Pointer Provenance and Minimizing Pointer Privilege in the POSIX C Run-time Environment}},
      booktitle = {Proceedings of the Twenty-Fourth International Conference on Architectural Support for Programming Languages and Operating Systems},
      year = {2019},
      month = apr,
      publisher = {ACM},
      url = {https://www.microsoft.com/en-us/research/publication/cheriabi-enforcing-valid-pointer-provenance-and-minimizing-pointer-privilege-in-the-posix-c-run-time-environment/},
      pdf = {https://www.cl.cam.ac.uk/research/security/ctsrd/pdfs/201904-asplos-cheriabi.pdf},
      pages = {379-393},
      note = {Best paper award winner}
    }
    

    Abstract: The CHERI architecture allows pointers to be implemented as capabilities (rather than integer virtual addresses) in a manner that is compatible with, and strengthens, the semantics of the C language. In addition to the spatial protections offered by conventional fat pointers, CHERI capabilities offer strong integrity, enforced provenance validity, and access monotonicity. The stronger guarantees of these architectural capabilities must be reconciled with the real-world behavior of operating systems, run-time environments, and applications. When the process model, user-kernel interactions, dynamic linking, and memory management are all considered, we observe that simple derivation of architectural capabilities is insufficient to describe appropriate access to memory. We bridge this conceptual gap with a notional abstract capability that describes the accesses that should be allowed at a given point in execution, whether in the kernel or userspace. To investigate this notion at scale, we describe the first adaptation of a full C-language operating system (FreeBSD) with an enterprise database (PostgreSQL) for complete spatial and referential memory safety. We show that awareness of abstract capabilities, coupled with CHERI architectural capabilities, can provide more complete protection, strong compatibility, and acceptable performance overhead compared with the pre-CHERI baseline and software-only approaches. Our observations also have potentially significant implications for other mitigation techniques.

  2. Jonathan Woodruff, Alexandre Joannou, Hongyan Xia, Anthony Fox, Robert Norton, Thomas Bauereiss, David Chisnall, Brooks Davis, Khilan Gudka, Nathaniel W. Filardo, A. Theodore Markettos, Michael Roe, Peter G. Neumann, Robert N. M. Watson and Simon W. Moore. CHERI Concentrate: Practical Compressed Capabilities. IEEE Transactions on Computers, (2019). [pdf]
    @article{woodruff2019cheri,
      author = {Woodruff, Jonathan and Joannou, Alexandre and Xia, Hongyan and Fox, Anthony and Norton, Robert and Bauereiss, Thomas and Chisnall, David and Davis, Brooks and Gudka, Khilan and Filardo, Nathaniel W. and Markettos, A. Theodore and Roe, Michael and Neumann, Peter G. and Watson, Robert N. M. and Moore, Simon W.},
      title = {CHERI Concentrate: Practical Compressed Capabilities},
      year = {2019},
      month = apr,
      url = {https://www.microsoft.com/en-us/research/publication/cheri-concentrate-practical-compressed-capabilities/},
      journal = {IEEE Transactions on Computers},
      pdf = {https://www.cl.cam.ac.uk/research/security/ctsrd/pdfs/2019tc-cheri-concentrate.pdf}
    }
    

    Abstract: We present CHERI Concentrate, a new fat-pointer compression scheme applied to CHERI, the most developed capability-pointer system at present. Capability fat-pointers are a primary candidate for enforcing fine-grained and non-bypassable security properties in future computer systems, although increased pointer size can severely affect performance. Thus, several proposals for capability compression have been suggested but these did not support legacy instruction sets, ignored features critical to the existing software base, and also introduced design inefficiencies to RISC-style processor pipelines. CHERI Concentrate improves on the state-of-the-art region-encoding efficiency, solves important pipeline problems, and eases semantic restrictions of compressed encoding, allowing it to protect a full legacy software stack. We analyze and extend logic from the open-source CHERI prototype processor design on FPGA to demonstrate encoding efficiency, minimize delay of pointer arithmetic, and eliminate additional load-to-use delay. To verify correctness of our proposed high-performance logic, we present a HOL4 machine-checked proof of the decode and pointer-modify operations. Finally, we measure a 50%-75% reduction in L2 misses for many compiled C-language benchmarks running under a commodity operating system using compressed 128-bit and 64-bit formats, demonstrating both compatibility with and increased performance over the uncompressed, 256-bit format.

  3. L. Simon, D. Chisnall and R. Anderson. What You Get is What You C: Controlling Side Effects in Mainstream C Compilers. 2018 IEEE European Symposium on Security and Privacy (EuroS&P), (2018), 1–15. [doi]
    @inproceedings{8406587,
      author = {Simon, L. and Chisnall, D. and Anderson, R.},
      booktitle = {2018 IEEE European Symposium on Security and Privacy ({EuroS\&P})},
      title = {What You Get is What You {C}: Controlling Side Effects in Mainstream {C} Compilers},
      year = {2018},
      pages = {1-15},
      keywords = {C++ language;cryptographic protocols;optimisation;program compilers;program verification;security properties;compiler commands;cryptographic protocol security;compiler performance;language security;mainstream C compilers;security engineers;careful programmer;cryptographic algorithm;compiler writers;compiler upgrade;timing channel;secure code;compiler optimization;implicit properties;crypto code;side effects;CPUs;Cryptography;Program processors;Standards;Libraries;Timing;Optimization;compilers;LLVM;Clang;compiler optimizations;side channels;cryptography;side effects;C;C abstract machine;constant-time;zeroing;erasing;stack},
      doi = {10.1109/EuroSP.2018.00009},
      month = apr
    }
    

    Abstract: Security engineers have been fighting with C compilers for years. A careful programmer would test for null pointer dereferencing or division by zero; but the compiler would fail to understand, and optimize the test away. Modern compilers now have dedicated options to mitigate this. But when a programmer tries to control side effects of code, such as to make a cryptographic algorithm execute in constant time, the problem remains. Programmers devise complex tricks to obscure their intentions, but compiler writers find ever smarter ways to optimize code. A compiler upgrade can suddenly and without warning open a timing channel in previously secure code. This arms race is pointless and has to stop. We argue that we must stop fighting the compiler, and instead make it our ally. As a starting point, we analyze the ways in which compiler optimization breaks implicit properties of crypto code; and add guarantees for two of these properties in Clang/LLVM. Our work explores what is actually involved in controlling side effects on modern CPUs with a standard toolchain. Similar techniques can and should be applied to other security properties; achieving intentions by compiler commands or annotations makes them explicit, so we can reason about them. It is already understood that explicitness is essential for cryptographic protocol security and for compiler performance; it is essential for language security too. We therefore argue that this should be only the first step in a sustained engineering effort.

  4. David Chisnall. C is Not a Low-level Language. Commun. ACM 61, 7 (2018), 44–48. [doi]
    @article{Chisnall:2018:CLL:3234519.3209212,
      author = {Chisnall, David},
      title = {C is Not a Low-level Language},
      journal = {Commun. ACM},
      issue_date = {July 2018},
      volume = {61},
      number = {7},
      month = jun,
      year = {2018},
      issn = {0001-0782},
      pages = {44--48},
      numpages = {5},
      url = {https://queue.acm.org/detail.cfm?id=3212479},
      doi = {10.1145/3209212},
      acmid = {3209212},
      publisher = {ACM},
      address = {New York, NY, USA}
    }
    

    Abstract: Your computer is not a fast PDP-11.

  5. Alexandre Joannou, Jonathan Woodruff, Robert Kovacsics, Simon. W. Moore, Alex Bradbury, Hongyan Xia, Robert N. M. Watson, David Chisnall, Michael Roe, Brooks Davis, Edward Napierala, John Baldwin, Khilan Gudka, Peter G. Neumann, Alfredo Mazzinghi, Alex Richardson, Stacey Son and A. Theodore Markettos. Efficient Tagged Memory. 2017 IEEE International Conference on Computer Design (ICCD), (2017), 641–648. [pdf] [doi]
    @inproceedings{efficienttags,
      author = {Joannou, Alexandre and Woodruff, Jonathan and Kovacsics, Robert and Moore, Simon. W. and Bradbury, Alex and Xia, Hongyan and Watson, Robert N. M. and Chisnall, David and Roe, Michael and Davis, Brooks and Napierala, Edward and Baldwin, John and Gudka, Khilan and Neumann, Peter G. and Mazzinghi, Alfredo and Richardson, Alex and Son, Stacey and Markettos, A. Theodore},
      booktitle = {2017 IEEE International Conference on Computer Design (ICCD)},
      title = {Efficient Tagged Memory},
      year = {2017},
      pages = {641-648},
      keywords = {Computer architecture;Error correction codes;Hardware;Metadata;Pipelines;Random access memory;Security;Caches;Memory;Processor;Safety;Security},
      doi = {10.1109/ICCD.2017.112},
      pdf = {http://www.cl.cam.ac.uk/research/security/ctsrd/pdfs/201711-iccd2017-efficient-tags.pdf},
      issn = {1063-6404},
      month = nov
    }
    

    Abstract: We characterize the cache behavior of an in-memory tag table and demonstrate that an optimized implementation can typically achieve a near-zero memory traffic overhead. Both industry and academia have repeatedly demonstrated tagged memory as a key mechanism to enable enforcement of powerful security invariants, including capabilities, pointer integrity, watchpoints, and information-flow tracking. A single-bit tag shadowspace is the most commonly proposed requirement, as one bit is the minimum metadata needed to distinguish between an untyped data word and any number of new hardware enforced types. We survey various tag shadowspace approaches and identify their common requirements and positive features of their implementations. To avoid non-standard memory widths, we identify the most practical implementation for tag storage to be an in-memory table managed next to the DRAM controller. We characterize the caching performance of such a tag table and demonstrate a DRAM traffic overhead below 5% for the vast majority of applications. We identify spatial locality on a page scale as the primary factor that enables surprisingly high table cache-ability. We then demonstrate tag-table compression for a set of common applications. A hierarchical structure with elegantly simple optimizations reduces DRAM traffic overhead to below 1% for most applications. These insights and optimizations pave the way for commercial applications making use of single-bit tags stored in commodity memory.