David Chisnall

---

---

Recent Publications

A full list is available on the publications page.

1. Nathaniel Wesley Filardo, Brett F. Gutstein, Jonathan Woodruff, Sam Ainsworth, Lucian Paul-Trifu, Brooks Davis, Hongyan Xia, Edward Tomasz Napierala, Alexander Richardson, John Baldwin, David Chisnall, Jessica Clarke, Khilan Gudka, Alexandre Joannou, A. Theodore Markettos, Alfredo Mazzinghi, Robert M. Norton, Michael Roe, Peter Sewell, Stacey Son, Timothy M. Jones, Simon W. Moore, Peter G. Neumann and Robert N. M. Watson. Cornucopia: Temporal Safety for CHERI Heaps. 2020 IEEE Symposium on Security and Privacy (SP), IEEE Computer Society (2020), 1507–1524. [BibTeX] [pdf] [doi]

   @inproceedings{filardo:cornucopia,
     author = {Filardo, Nathaniel Wesley and Gutstein, Brett~F. and Woodruff, Jonathan and Ainsworth, Sam and Paul-Trifu, Lucian and Davis, Brooks and Xia, Hongyan and Napierala, Edward Tomasz and Richardson, Alexander and Baldwin, John and Chisnall, David and Clarke, Jessica and Gudka, Khilan and Joannou, Alexandre and Markettos, A.~Theodore and Mazzinghi, Alfredo and Norton, Robert~M. and Roe, Michael and Sewell, Peter and Son, Stacey and Jones, Timothy~M. and Moore, Simon~W. and Neumann, Peter~G. and Watson, Robert~N.~M.},
     booktitle = {2020 IEEE Symposium on Security and Privacy (SP)},
     title = {Cornucopia: Temporal Safety for {CHERI} Heaps},
     year = {2020},
     volume = {},
     issn = {2375-1207},
     pages = {1507-1524},
     doi = {10.1109/SP40000.2020.00098},
     url = {https://www.cl.cam.ac.uk/research/security/ctsrd/pdfs/2020oakland-cornucopia.pdf},
     publisher = {IEEE Computer Society},
     address = {Los Alamitos, CA, USA},
     month = may
   }
   

2. 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. [BibTeX] [abstract] [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.

3. 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). [BibTeX] [abstract] [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.

4. 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. [BibTeX] [abstract] [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.

5. David Chisnall. C is Not a Low-level Language. Commun. ACM 61, 7 (2018), 44–48. [BibTeX] [abstract] [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.