Department of Computer Science and Technology

Publications

Download a complete list of publications as BibTeX

Contents

Articles

  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]
    BibTeX 
    @inproceedings{filardo:cornucopiareloaded,
  title = {{Cornucopia Reloaded: Load Barriers for CHERI Heap Temporal
              Safety}},
  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]
    BibTeX 
    @inproceedings{cheri-c-asplos,
  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}
}
    Abstract

    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]
    BibTeX 
    @article{10.1145/3622852,
  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}
}
    Abstract

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

  5. Hugo Lefeuvre, David Chisnall, Marios Kogias and Pierre Olivier. Towards (Really) Safe and Fast Confidential I/O. HotOS XIX, (2023). [doi]
    BibTeX 
    @inproceedings{hotosconfidential,
  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}
}
    Abstract

    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.

  6. Kapil Vaswani, Stavros Volos, Cédric Fournet, Antonio Nino Diaz, Ken Gordon, Balaji Vembu, Sam Webster, David Chisnall, Saurabh Kulkarni, Graham Cunningham, Richard Osborne and Dan Wilkinson. Confidential Computing within an AI Accelerator. 2023 USENIX Annual Technical Conference, (2023). [pdf]
    BibTeX 
    @inproceedings{vaswani2023confidential,
  author = {Vaswani, Kapil and Volos, Stavros and Fournet, Cédric and Nino Diaz, Antonio and Gordon, Ken and Vembu, Balaji and Webster, Sam and Chisnall, David and Kulkarni, Saurabh and Cunningham, Graham and Osborne, Richard and Wilkinson, Dan},
  title = {Confidential Computing within an AI Accelerator},
  booktitle = {2023 USENIX Annual Technical Conference},
  year = {2023},
  month = jul,
  url = {https://www.microsoft.com/en-us/research/uploads/prod/2023/05/confidential-ml-within-ipus-arxiv.pdf}
}
    Abstract

    We present AITX, a set of hardware extensions that enable trusted execution environments on a commodity custom AI accelerator. AITX enables the execution of AI workloads with strong confidentiality and integrity guarantees at low performance overheads. AITX isolates workloads from untrusted hosts, and ensures their data/models remain encrypted at all times except within the accelerator’s chip. AITX includes a hardware root-of-trust that provides attestation capabilities and orchestrates trusted execution, and on-chip programmable cryptographic engines for authenticated encryption of code/data at PCIe bandwidth. We also present software for AITX in the form of compiler and runtime extensions that support multi-party training without requiring a CPU-based TEE.

    We included experimental support for AITX in an AI accelerator taped out at TSMC’s 7nm node. Its evaluation on a development board using standard DNN training workloads suggests that AITX adds < 5% performance overhead, and delivers up to 17x better performance compared to CPU-based confidential computing systems based on AMD SEV-SNP.

  7. Hongyan Xia, David Zhang, Wei Liu, Istvan Haller, Bruce Sherwin and David Chisnall. A Secret-Free Hypervisor: Rethinking Isolation in the Age of Speculative Vulnerabilities. 2022 IEEE Symposium on Security and Privacy, IEEE Computer Society (2022), 1544–1544. [pdf] [doi]
    BibTeX 
    @inproceedings{xia2022a,
  author = {Xia, Hongyan and Zhang, David and Liu, Wei and Haller, Istvan and Sherwin, Bruce and Chisnall, David},
  title = {A Secret-Free Hypervisor: Rethinking Isolation in the Age of Speculative Vulnerabilities},
  booktitle = {2022 IEEE Symposium on Security and Privacy},
  year = {2022},
  month = may,
  publisher = {IEEE Computer Society},
  url = {https://www.microsoft.com/en-us/research/uploads/prod/2022/07/sf-hypervisor.pdf},
  pages = {1544-1544},
  doi = {10.1109/SP46214.2022.9833726}
}
    Abstract

    In recent years, the epidemic of speculative side channels significantly increases the difficulty in enforcing domain isolation boundaries in a virtualized cloud environment. Although mitigations exist, the approach taken by the industry is neither a long-term nor a scalable solution, as we target each vulnerability with specific mitigations that add up to substantial performance penalties. We propose a different approach to secret isolation: guaranteeing that the hypervisor is Secret-Free (SF).

    A Secret-Free design partitions memory into secrets and non-secrets and reconstructs hypervisor isolation. It enforces that all domains have a minimal and secret-free view of the address space. In contrast to state-of-the-art, a Secret-Free hypervisor does not identify secrets to be hidden, but instead identifies non-secrets that can be shared, and only grants access necessary for the current operation, an allow-list approach. SF designs function with existing hardware and do not exhibit noticeable performance penalties in production workloads versus the unmitigated baseline, and outperform state-of-the-art techniques by allowing speculative execution where secrets are invisible. We implement SF in Xen (a Type-I hypervisor) to demonstrate that the design applies well to a commercial hypervisor. Evaluation shows performance comparable to baseline and up to 37% improvement in certain hypervisor paths compared with Xen default mitigations.

    Further, we demonstrate Secret-Free is a generic kernel isolation infrastructure for a variety of systems, not limited to Type-I hypervisors. We apply the same model in Hyper-V (Type-I), bhyve (Type-II) and FreeBSD (UNIX kernel) to evaluate its applicability and effectiveness. The successful implementations on these systems prove the generality of SF, and reveal the specific adaptations and optimizations required for each type of kernel.

  8. Mark Russinovich, Manuel Costa, Cédric Fournet, David Chisnall, Antoine Delignat-Lavaud, Sylvan Clebsch, Kapil Vaswani and Vikas Bhatia. Toward Confidential Cloud Computing: Extending Hardware-Enforced Cryptographic Protection to Data While in Use. Queue 19, 1 (2021), 49–76. [doi]
    BibTeX 
    @article{10.1145/3454122.3456125,
  author = {Russinovich, Mark and Costa, Manuel and Fournet, C\'{e}dric and Chisnall, David and Delignat-Lavaud, Antoine and Clebsch, Sylvan and Vaswani, Kapil and Bhatia, Vikas},
  title = {Toward Confidential Cloud Computing: Extending Hardware-Enforced Cryptographic Protection to Data While in Use},
  year = {2021},
  issue_date = {January-February 2021},
  publisher = {Association for Computing Machinery},
  address = {New York, NY, USA},
  volume = {19},
  number = {1},
  issn = {1542-7730},
  url = {https://doi.org/10.1145/3454122.3456125},
  doi = {10.1145/3454122.3456125},
  journal = {Queue},
  month = mar,
  pages = {49–76},
  numpages = {28}
}
    Abstract

    Although largely driven by economies of scale, the development of the modern cloud also enables increased security. Large data centers provide aggregate availability, reliability, and security assurances. The operational cost of ensuring that operating systems, databases, and other services have secure configurations can be amortized among all tenants, allowing the cloud provider to employ experts who are responsible for security; this is often unfeasible for smaller businesses, where the role of systems administrator is often conflated with many others.

  9. Mark Russinovich, Manuel Costa, Cédric Fournet, David Chisnall, Antoine Delignat-Lavaud, Sylvan Clebsch, Kapil Vaswani and Vikas Bhatia. Toward Confidential Cloud Computing. Commun. ACM 64, 6 (2021), 54–61. [doi]
    BibTeX 
    @article{10.1145/3453930,
  author = {Russinovich, Mark and Costa, Manuel and Fournet, C\'{e}dric and Chisnall, David and Delignat-Lavaud, Antoine and Clebsch, Sylvan and Vaswani, Kapil and Bhatia, Vikas},
  title = {Toward Confidential Cloud Computing},
  year = {2021},
  issue_date = {June 2021},
  publisher = {Association for Computing Machinery},
  address = {New York, NY, USA},
  volume = {64},
  number = {6},
  issn = {0001-0782},
  url = {https://doi.org/10.1145/3453930},
  doi = {10.1145/3453930},
  journal = {Commun. ACM},
  month = may,
  pages = {54–61},
  numpages = {8}
}
    Abstract

    Extending hardware-enforced cryptographic protection to data while in use.

  10. 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. [pdf] [doi]
    BibTeX 
    @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
}
  11. Paul Liétar, Theodore Butler, Sylvan Clebsch, Sophia Drossopoulou, Juliana Franco, Matthew J. Parkinson, Alex Shamis, Christoph M. Wintersteiger and David Chisnall. Snmalloc: A Message Passing Allocator. Proceedings of the 2019 ACM SIGPLAN International Symposium on Memory Management, Association for Computing Machinery (2019), 122–135. [doi]
    BibTeX 
    @inproceedings{10.1145/3315573.3329980,
  author = {Li\'{e}tar, Paul and Butler, Theodore and Clebsch, Sylvan and Drossopoulou, Sophia and Franco, Juliana and Parkinson, Matthew J. and Shamis, Alex and Wintersteiger, Christoph M. and Chisnall, David},
  title = {Snmalloc: A Message Passing Allocator},
  year = {2019},
  isbn = {9781450367226},
  publisher = {Association for Computing Machinery},
  address = {New York, NY, USA},
  url = {https://doi.org/10.1145/3315573.3329980},
  doi = {10.1145/3315573.3329980},
  booktitle = {Proceedings of the 2019 ACM SIGPLAN International Symposium on Memory Management},
  pages = {122–135},
  numpages = {14},
  keywords = {Memory allocation, message passing},
  location = {Phoenix, AZ, USA},
  series = {ISMM 2019}
}
    Abstract

    snmalloc is an implementation of malloc aimed at workloads in which objects are typically deallocated by a different thread than the one that had allocated them. We use the term producer/consumer for such workloads. snmalloc uses a novel message passing scheme which returns deallocated objects to the originating allocator in batches without taking any locks. It also uses a novel bump pointer-free list data structure with which just 64-bits of meta-data are sufficient for each 64 KiB slab. On such producer/consumer benchmarks our approach performs better than existing allocators. Snmalloc is available at https://github.com/Microsoft/snmalloc.

  12. 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] [doi]
    BibTeX 
    @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},
  isbn = {9781450362405},
  publisher = {ACM},
  address = {New York, NY, USA},
  doi = {10.1145/3297858.3304042},
  pages = {379-393},
  numpages = {15},
  location = {Providence, RI, USA},
  series = {ASPLOS '19},
  year = {2019},
  month = apr,
  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},
  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.

  13. 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 68, 10 (2019), 1455–1469. [pdf] [doi]
    BibTeX 
    @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,
  volume = {68},
  number = {10},
  pages = {1455-1469},
  url = {https://www.microsoft.com/en-us/research/publication/cheri-concentrate-practical-compressed-capabilities/},
  journal = {IEEE Transactions on Computers},
  doi = {10.1109/TC.2019.2914037},
  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.

  14. 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]
    BibTeX 
    @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.

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

  16. 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]
    BibTeX 
    @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.

  17. David Chisnall, Brooks Davis, Khilan Gudka, David Brazdil, Alexandre Joannouand Jonathan Woodruff, A. Theodore Markettos, J. Edward Maste, Robert Norton, Stacey Son, Michael Roe, Simon W. Moore, Peter G. Neumann, Ben Laurie and Robert N. M. Watson. CHERI JNI: Sinking the Java security model into the C. Proceedings of the Twenty Second International Conference on Architectural Support for Programming Languages and Operating Systems, ACM (2017), 569–583. [pdf] [doi]
    BibTeX 
    @inproceedings{cherijni,
  author = {Chisnall, David and Davis, Brooks and Gudka, Khilan and Brazdil, David and Woodruff, Alexandre Joannouand Jonathan and Markettos, A. Theodore and Maste, J. Edward and Norton, Robert and Son, Stacey and Roe, Michael and Moore, Simon W. and Neumann, Peter G. and Laurie, Ben and Watson, Robert N. M.},
  title = {{CHERI JNI}: Sinking the Java security model into the {C}},
  booktitle = {Proceedings of the Twenty Second International Conference on Architectural Support for Programming Languages and Operating Systems},
  series = {ASPLOS '17},
  year = {2017},
  location = {Xi'an, China},
  publisher = {ACM},
  address = {New York, NY, USA},
  acmid = {3037725},
  pages = {569--583},
  numpages = {15},
  isbn = {978-1-4503-4465-4},
  keywords = {Java language, C language, bounds checking, capabilities, compilers, memory protection, memory safety, processor design, security},
  pdf = {http://dl.acm.org/authorize?N24950},
  url = {http://doi.acm.org/10.1145/3037697.3037725},
  doi = {10.1145/3037697.3037725}
}
    Abstract

    Java provides security and robustness by building a high-level security model atop the foundation of memory protection. Unfortunately, any native code linked into a Java program – including the million lines used to implement the standard library – is able to bypass both the memory protection and the higher-level policies. We present a hardware-assisted implementation of the Java native code interface, which extends the guarantees required for Java’s security model to native code.

    Our design supports safe direct access to buffers owned by the JVM, including hardware-enforced read-only access where appropriate. We also present Java language syntax to declaratively describe isolated compartments for native code.

    We show that it is possible to preserve the memory safety and isolation requirements of the Java security model in C code, allowing native code to run in the same process as Java code with the same impact on security as running equivalent Java code. Our approach has a negligible impact on performance, compared with the existing unsafe native code interface. We demonstrate a prototype implementation running on the CHERI microprocessor synthesized in FPGA.

  18. Robert N. M. Watson, Robert M. Norton, Jon Woodruff, Simon W. Moore, Peter G. Neumann, Jon Anderson, David Chisnall, Brooks Davis, Ben. Laurie, Michael Roe, Nirav H. Dave, Khilan Gudka, Alexandre Joannou, A. Theodore Markettos, J. Edward Maste, Steven J. Murdoch, Colin Rothwell, Stacey D. Son and Munraj Vadera. Fast Protection-Domain Crossing in the CHERI Capability-System Architecture. IEEE Micro 36, 5 (2016), 38–49. [doi]
    BibTeX 
    @article{7723791,
  author = {Watson, Robert N. M. and Norton, Robert M. and Woodruff, Jon and Moore, Simon W. and Neumann, Peter G. and Anderson, Jon and Chisnall, David and Davis, Brooks and Laurie, Ben. and Roe, Michael and Dave, Nirav H. and Gudka, Khilan and Joannou, Alexandre and Markettos, A. Theodore and Maste, J. Edward and Murdoch, Steven J. and Rothwell, Colin and Son, Stacey D. and Vadera, Munraj},
  journal = {IEEE Micro},
  title = {Fast Protection-Domain Crossing in the CHERI Capability-System Architecture},
  year = {2016},
  volume = {36},
  number = {5},
  pages = {38-49},
  keywords = {Capability engineering;Memory management;Program processors;Reduced instruction set computing;Systems modeling;CHERI;ISA;capabilities;capability;capability system;compartmentalization;hardware;instruction set architecture;memory management unit;memory protection;processor;security;software;vulnerability mitigation},
  doi = {10.1109/MM.2016.84},
  issn = {0272-1732},
  month = sep
}
    Abstract

    Capability Hardware Enhanced RISC Instructions (CHERI) supplement the conventional memory management unit (MMU) with instruction-set architecture (ISA) extensions that implement a capability system model in the address space. CHERI can also underpin a hardware-software object-capability model for scalable application compartmentalization that can mitigate broader classes of attack. This article describes ISA additions to CHERI that support fast protection-domain switching, not only in terms of low cycle count, but also efficient memory sharing with mutual distrust. The authors propose ISA support for sealed capabilities, hardware-assisted checking during protection-domain switching, a lightweight capability flow-control model, and fast register clearing, while retaining the flexibility of a software-defined protection-domain transition model. They validate this approach through a full-system experimental design, including ISA extensions, a field-programmable gate array prototype (implemented in Bluespec SystemVerilog), and a software stack including an OS (based on FreeBSD), compiler (based on LLVM), software compartmentalization model, and open-source applications.

  19. Kayvan Memarian, Justus Matthiesen, James Lingard, Kyndylan Nienhuis, David Chisnall, Robert N. M. Watson and Peter Sewell. Into the Depths of C: Elaborating the De Facto Standards. Proceedings of the 37th ACM SIGPLAN Conference on Programming Language Design and Implementation, ACM (2016), 1–15. [doi]
    BibTeX 
    @inproceedings{Memarian:2016:DCE:2908080.2908081,
  author = {Memarian, Kayvan and Matthiesen, Justus and Lingard, James and Nienhuis, Kyndylan and Chisnall, David and Watson, Robert N. M. and Sewell, Peter},
  title = {Into the Depths of C: Elaborating the De Facto Standards},
  booktitle = {Proceedings of the 37th ACM SIGPLAN Conference on Programming Language Design and Implementation},
  series = {PLDI 2016},
  year = {2016},
  isbn = {978-1-4503-4261-2},
  location = {Santa Barbara, CA, USA},
  pages = {1--15},
  numpages = {15},
  url = {http://dl.acm.org/authorize?N04455},
  doi = {10.1145/2908080.2908081},
  acmid = {2908081},
  publisher = {ACM},
  address = {New York, NY, USA},
  keywords = {C}
}
  20. Khilan Gudka, Robert N.M. Watson, Jonathan Anderson, David Chisnall, Brooks Davis, Ben Laurie, Ilias Marinos, Peter G. Neumann and Alex Richardson. Clean Application Compartmentalization with SOAAP. Proceedings of the 22nd ACM Conference on Computer and Communications Security, (2015). [pdf]
    BibTeX 
    @inproceedings{gudka2015soaap,
  title = {Clean Application Compartmentalization with SOAAP},
  author = {Gudka, Khilan and Watson, Robert N.M. and Anderson, Jonathan and Chisnall, David and Davis, Brooks and Laurie, Ben and Marinos, Ilias and Neumann, Peter G. and Richardson, Alex},
  booktitle = {Proceedings of the 22nd ACM Conference on Computer and Communications Security},
  year = {2015},
  month = oct,
  address = {Denver, CO, USA},
  pdf = {http://www.cl.cam.ac.uk/research/security/ctsrd/pdfs/2015ccs-soaap.pdf}
}
    Abstract

    Application compartmentalization, a vulnerability mitigation technique employed in programs such as OpenSSH and the Chromium web browser, decomposes software into isolated components to limit privileges leaked or otherwise available to attackers. However, compartmentalizing applications – and maintaining that compartmentalization – is hindered by ad hoc methodologies and significantly increased programming effort. In practice, programmers stumble through (rather than overtly reason about) compartmentalization spaces of possible decompositions, unknowingly trading off correctness, security, complexity, and performance. We present a new conceptual framework embodied in an LLVM-based tool: the Security-Oriented Analysis of Application Programs (SOAAP) that allows programmers to reason about compartmentalization using source-code annotations (compartmentalization hypotheses). We demonstrate considerable benefit when creating new compartmentalizations for complex applications, and analyze existing compartmentalized applications to discover design faults and maintenance issues arising from application evolution.

  21. R. N. M. Watson, J. Woodruff, P. G. Neumann, S. W. Moore, J. Anderson, D. Chisnall, N. Dave, B. Davis, K. Gudka, B. Laurie, S. J. Murdoch, R. Norton, M. Roe, S. Son and M. Vadera. CHERI: A Hybrid Capability-System Architecture for Scalable Software Compartmentalization. 2015 IEEE Symposium on Security and Privacy, (2015), 20–37. [pdf] [doi]
    BibTeX 
    @inproceedings{7163016,
  author = {Watson, R. N. M. and Woodruff, J. and Neumann, P. G. and Moore, S. W. and Anderson, J. and Chisnall, D. and Dave, N. and Davis, B. and Gudka, K. and Laurie, B. and Murdoch, S. J. and Norton, R. and Roe, M. and Son, S. and Vadera, M.},
  booktitle = {2015 IEEE Symposium on Security and Privacy},
  title = {CHERI: A Hybrid Capability-System Architecture for Scalable Software Compartmentalization},
  year = {2015},
  pages = {20-37},
  keywords = {data protection;operating systems (computers);program compilers;reduced instruction set computing;software architecture;C-language TCB;CHERI;LLVM compiler;RISC instruction-set architecture;capability-based memory protection;hardware-software object-capability model;hybrid capability-system architecture;operating system;software compartmentalization;Hardware;Kernel;Libraries;Reduced instruction set computing;Registers;Security;CHERI processor;capability system;computer architecture;memory protection;object capabilities;software compartmentalization},
  doi = {10.1109/SP.2015.9},
  issn = {1081-6011},
  month = may,
  pdf = {papers/201505-oakland2015-cheri-compartmentalization.pdf}
}
    Abstract

    CHERI is a hardware-software architecture that combines a capability-system security model with design choices from contemporary processors, Instruction-Set Architectures (ISAs), compilers, and operating systems. At the lowest level, CHERI’s fine-grained, in-address-space memory protection mitigates many widely used exploit techniques. However, CHERI’s ISA-level capability model can also act as the foundation for a software object-capability model suitable for incremental deployment in compartmentalizing C-language applications to mitigate attacks. Prototyped as an extension to the 64-bit FPGA BERI RISC soft-core processor, FreeBSD operating system, and Clang/LLVM compiler suite, we demonstrate substantial improvements to security, programmability, and scalability as compared to compartmentalization based on pure Memory-Management Unit (MMU) designs. We evaluate CHERI using several real-world UNIX libraries and applications.

  22. David Chisnall, Colin Rothwell, Brooks Davis, Robert N.M. Watson, Jonathan Woodruff, Munraj Vadera, Simon W. Moore, Peter G. Neumann and Michael Roe. Beyond the PDP-11: Architectural Support for a Memory-Safe C Abstract Machine. Proceedings of the Twentieth International Conference on Architectural Support for Programming Languages and Operating Systems, ACM (2015), 117–130. [pdf] [doi]
    BibTeX 
    @inproceedings{Chisnall:2015:BPA:2694344.2694367,
  author = {Chisnall, David and Rothwell, Colin and Davis, Brooks and Watson, Robert N.M. and Woodruff, Jonathan and Vadera, Munraj and Moore, Simon W. and Neumann, Peter G. and Roe, Michael},
  title = {Beyond the {PDP-11}: Architectural Support for a Memory-Safe C Abstract Machine},
  booktitle = {Proceedings of the Twentieth International Conference on Architectural Support for Programming Languages and Operating Systems},
  series = {ASPLOS '15},
  year = {2015},
  isbn = {978-1-4503-2835-7},
  location = {Istanbul, Turkey},
  pages = {117--130},
  numpages = {14},
  url = {http://doi.acm.org/10.1145/2694344.2694367},
  doi = {10.1145/2694344.2694367},
  acmid = {2694367},
  publisher = {ACM},
  address = {New York, NY, USA},
  keywords = {C language, bounds checking, capabilities, compilers, memory protection, memory safety, processor design, security},
  pdf = {papers/asplos15-memory-safe-c.pdf}
}
    Abstract

    We propose a new memory-safe interpretation of the C abstract machine that provides stronger protection to benefit security and debugging. Despite ambiguities in the specification intended to provide implementation flexibility, contemporary implementations of C have converged on a memory model similar to the PDP-11, the original target for C. This model lacks support for memory safety despite well documented impacts on security and reliability.

    Attempts to change this model are often hampered by assumptions embedded in a large body of existing C code, dating back to the memory model exposed by the original C compiler for the PDP-11. Our experience with attempting to implement a memory-safe variant of C on the CHERI experimental microprocessor led us to identify a number of problematic idioms. We describe these as well as their interaction with existing memory safety schemes and the assumptions that they make beyond the requirements of the C specification. Finally, we refine the CHERI ISA and abstract model for C, by combining elements of the CHERI capability model and fat pointers, and present a softcore CPU that implements a C abstract machine that can run legacy C code with strong memory protection guarantees.

  23. David Chisnall. No such thing as a general-purpose processor. Communications of the ACM 57, 12 (2014), 44–48. [pdf] [doi]
    BibTeX 
    @article{2677030,
  author = {Chisnall, David},
  title = {No such thing as a general-purpose processor},
  journal = {Communications of the ACM},
  volume = {57},
  number = {12},
  year = {2014},
  issn = {0001-0782},
  pages = {44--48},
  doi = {http://doi.acm.org/10.1145/2677030},
  publisher = {ACM},
  address = {New York, NY, USA},
  pdf = {http://dl.acm.org/authorize?N83787}
}
  24. David Chisnall. Smalltalk in a C world. Science of Computer Programming 96, Part 1, 0 (2014), 4–16. [doi]
    BibTeX 
    @article{Chisnall20144,
  title = {Smalltalk in a C world},
  journal = {Science of Computer Programming},
  volume = {96, Part 1},
  number = {0},
  pages = {4 - 16},
  year = {2014},
  mon = {dec},
  note = {Special issue on Advances in Smalltalk based Systems },
  issn = {0167-6423},
  doi = {http://dx.doi.org/10.1016/j.scico.2013.10.013},
  url = {http://www.sciencedirect.com/science/article/pii/S0167642313002852},
  author = {Chisnall, David},
  keywords = {Optimisation }
}
    Abstract

    A modern developer is presented with a continuum of choices of programming languages, ranging from assembly languages and C up to high-level domain-specific languages. It is very rare for a single language to be the best possible choice for everything, and the sweet spot with an optimal trade between ease of development and performance changes depending on the target platform.

    We present an interoperable framework for allowing code written in C (potentially with inline assembly), Objective-C, Smalltalk, and higher-level domain-specific languages to coexist with very low cognitive or performance overhead. Our implementation shares an underlying object model, in interpreted, JIT-compiled and statically compiled code among all languages, allowing a single object to have methods implemented in any of the supported languages. We also describe several techniques that we have used to improve the performance of late-bound dynamic languages.

  25. David Chisnall. There’s No Such Thing As a General-purpose Processor. Queue 12, 10 (2014), 20:20–20:25. [doi]
    BibTeX 
    @article{Chisnall:2014:TNT:2685690.2687011,
  author = {Chisnall, David},
  title = {There's No Such Thing As a General-purpose Processor},
  journal = {Queue},
  issue_date = {October 2014},
  volume = {12},
  number = {10},
  month = oct,
  year = {2014},
  issn = {1542-7730},
  pages = {20:20--20:25},
  articleno = {20},
  numpages = {6},
  url = {http://doi.acm.org/10.1145/2685690.2687011},
  doi = {10.1145/2685690.2687011},
  acmid = {2687011},
  publisher = {ACM},
  address = {New York, NY, USA}
}
  26. Jonathan Woodruff, Robert N.M. Watson, David Chisnall, Simon W. Moore, Jonathan Anderson, Brooks Davis, Ben Laurie, Peter G. Neumann, Robert Norton and Michael Roe. The CHERI capability model: revisiting RISC in an age of risk. ISCA ’14: Proceeding of the 41st annual international symposium on Computer architecture, IEEE Press (2014), 457–468. [pdf] [doi]
    BibTeX 
    @inproceedings{2665740,
  author = {Woodruff, Jonathan and Watson, Robert N.M. and Chisnall, David and Moore, Simon W. and Anderson, Jonathan and Davis, Brooks and Laurie, Ben and Neumann, Peter G. and Norton, Robert and Roe, Michael},
  title = {The CHERI capability model: revisiting RISC in an age of risk},
  booktitle = {ISCA '14: Proceeding of the 41st annual international symposium on Computer architecture},
  year = {2014},
  isbn = {978-1-4799-4394-4},
  doi = {http://dx.doi.org/10.1145/2678373.2665740},
  pages = {457--468},
  location = {Minneapolis, Minnesota, USA},
  publisher = {IEEE Press},
  address = {Piscataway, NJ, USA},
  pdf = {http://dl.acm.org/ft_gateway.cfm?id=2665740&type=pdf}
}
    Abstract

    Motivated by contemporary security challenges, we reevaluate and refine capability-based addressing for the RISC era. We present CHERI, a hybrid capability model that extends the 64-bit MIPS ISA with byte-granularity memory protection. We demonstrate that CHERI enables language memory model enforcement and fault isolation in hardware rather than software, and that the CHERI mechanisms are easily adopted by existing programs for efficient in-program memory safety. In contrast to past capability models, CHERI complements, rather than replaces, the ubiquitous page-based protection mechanism, providing a migration path towards deconflating data-structure protection and OS memory management. Furthermore, CHERI adheres to a strict RISC philosophy: it maintains a load-store architecture and requires only singlecycle instructions, and supplies protection primitives to the compiler, language runtime, and operating system. We demonstrate a mature FPGA implementation that runs the FreeBSD operating system with a full range of software and an open-source application suite compiled with an extended LLVM to use CHERI memory protection. A limit study compares published memory safety mechanisms in terms of instruction count and memory overheads. The study illustrates that CHERI is performance-competitive even while providing assurance and greater flexibility with simpler hardware

  27. David Chisnall. LLVM in the FreeBSD Toolchain. Proceedings of AsiaBSDCon 2014, (2014). [pdf]
    BibTeX 
    @inproceedings{llvmfreebsd2014,
  author = {Chisnall, David},
  title = {LLVM in the FreeBSD Toolchain},
  booktitle = {Proceedings of AsiaBSDCon 2014},
  address = {Tokyo, Japan},
  month = mar,
  days = {13–16},
  year = {2014},
  pdf = {http://www.cl.cam.ac.uk/research/security/ctsrd/pdfs/201403-asiabsdcon2014-llvmbsd.pdf}
}
  28. Jonathan Anderson, Robert N. M. Watson, David Chisnall, Khilan Gudka, Ilias Marinos and Brooks Davis. TESLA: temporally enhanced system logic assertions. EuroSys ’14: Proceedings of the Ninth European Conference on Computer Systems, ACM (2014), 1–14. [pdf] [doi]
    BibTeX 
    @inproceedings{2592801,
  author = {Anderson, Jonathan and Watson, Robert N. M. and Chisnall, David and Gudka, Khilan and Marinos, Ilias and Davis, Brooks},
  title = {TESLA: temporally enhanced system logic assertions},
  booktitle = {EuroSys '14: Proceedings of the Ninth European Conference on Computer Systems},
  year = {2014},
  isbn = {978-1-4503-2704-6},
  pages = {1--14},
  location = {Amsterdam, The Netherlands},
  doi = {http://doi.acm.org/10.1145/2592798.2592801},
  publisher = {ACM},
  address = {New York, NY, USA},
  pdf = {http://www.cl.cam.ac.uk/research/security/ctsrd/pdfs/201406-isca2014-cheri.pdf}
}
    Abstract

    Large, complex, rapidly evolving pieces of software such as operating systems are notoriously difficult to prove correct. Developers instead describe expected behaviour through assertions and check actual behaviour through testing. However, many dynamic safety properties cannot be validated this way as they are temporal: they depend on events in the past or future and are not easily expressed in assertions.

    TESLA is a description, analysis, and validation tool that allows systems programmers to describe expected temporal behaviour in low-level languages such as C. Temporal assertions can span the interfaces between libraries and even languages. TESLA exposes run-time behaviour using program instrumentation, illuminating coverage of complex state machines and detecting violations of specifications.

    We apply TESLA to complex software, including an OpenSSL security API, the FreeBSD Mandatory Access Control framework, and GNUstep’s rendering engine. With performance allowing "always-on" availability, we demonstrate that existing systems can benefit from richer dynamic analysis without being re-written for amenability to a complete formal analysis.

  29. David Chisnall. The challenge of cross-language interoperability. Communications of the ACM 56, 12 (2013), 50–56. [pdf] [doi]
    BibTeX 
    @article{2534719,
  author = {Chisnall, David},
  title = {The challenge of cross-language interoperability},
  journal = {Communications of the ACM},
  volume = {56},
  number = {12},
  year = {2013},
  issn = {0001-0782},
  pages = {50--56},
  doi = {http://doi.acm.org/10.1145/2534706.2534719},
  publisher = {ACM},
  address = {New York, NY, USA},
  pdf = {http://dl.acm.org/authorize?N87790}
}
    Abstract

    Interoperability between languages has been a problem since the second programming language was invented. Various solutions have been proposed, ranging from language-independent object models like COM and CORBA to VMs designed to integrate languages like the JVM and CLR. With software becoming ever more complex and hardware less homogeneous, the likelihood of a single language being the correct tool for the job for all of a program is lower than ever. As modern compilers become more modular, there is potential for a new generation of interesting solutions.

  30. David Chisnall. The Challenge of Cross-language Interoperability. Queue 11, 10 (2013), 20–28. [pdf] [doi]
    BibTeX 
    @article{2543971,
  author = {Chisnall, David},
  title = {The Challenge of Cross-language Interoperability},
  journal = {Queue},
  volume = {11},
  number = {10},
  year = {2013},
  issn = {1542-7730},
  pages = {20--28},
  doi = {http://doi.acm.org/10.1145/2542661.2543971},
  publisher = {ACM},
  address = {New York, NY, USA},
  pdf = {http://dl.acm.org/ft_gateway.cfm?id=2543971&type=pdf}
}
    Abstract

    Interoperability between languages has been a problem since the second programming language was invented. Various solutions have been proposed, ranging from language-independent object models like COM and CORBA to VMs designed to integrate languages like the JVM and CLR. With software becoming ever more complex and hardware less homogeneous, the likelihood of a single language being the correct tool for the job for all of a program is lower than ever. As modern compilers become more modular, there is potential for a new generation of interesting solutions.

  31. David Chisnall. A new Objective-C runtime: from research to production. Communications of the ACM 55, 9 (2012), 44–47. [pdf] [doi]
    BibTeX 
    @article{2330682,
  author = {Chisnall, David},
  title = {A new Objective-C runtime: from research to production},
  journal = {Communications of the ACM},
  volume = {55},
  number = {9},
  year = {2012},
  issn = {0001-0782},
  pages = {44--47},
  doi = {http://doi.acm.org/10.1145/2330667.2330682},
  publisher = {ACM},
  address = {New York, NY, USA},
  pdf = {http://dl.acm.org/authorize?N83788}
}
  32. David Chisnall. Smalltalk in a C world. IWST ’12: Proceedings of the International Workshop on Smalltalk Technologies, ACM (2012), 1–12. [pdf] [doi]
    BibTeX 
    @inproceedings{2448967,
  author = {Chisnall, David},
  title = {Smalltalk in a C world},
  booktitle = {IWST '12: Proceedings of the International Workshop on Smalltalk Technologies},
  year = {2012},
  isbn = {978-1-4503-1897-6},
  pages = {1--12},
  location = {Ghent, Belgium},
  doi = {http://doi.acm.org/10.1145/2448963.2448967},
  publisher = {ACM},
  address = {New York, NY, USA},
  pdf = {http://dl.acm.org/authorize?N83789}
}
    Abstract

    Smalltalk, in spite of myriad advantages in terms of ease of development, has been largely eclipsed by lower-level languages like C, which has become the lingua franca on modern systems. This paper introduces the Pragmatic Smalltalk compiler, which provides a dialect of Smalltalk that is designed from the ground up for close interoperability with C libraries. We describe how high-level Smalltalk language features are lowered to allow execution without a virtual machine, allowing Smalltalk and C code to be mixed in the same program without hard boundaries between the two. This allows incremental deployment of Smalltalk code in programs and libraries along with heavily optimised low-level C and assembly routines for performance critical segments.

  33. David Chisnall. A New Objective-C Runtime: from Research to Production. Queue 10, 7 (2012), 20–24. [doi]
    BibTeX 
    @article{2331170,
  author = {Chisnall, David},
  title = {A New Objective-C Runtime: from Research to Production},
  journal = {Queue},
  volume = {10},
  number = {7},
  year = {2012},
  issn = {1542-7730},
  pages = {20--24},
  doi = {http://doi.acm.org/10.1145/2330087.2331170},
  publisher = {ACM},
  address = {New York, NY, USA}
}
  34. David Chisnall, Min Chen and Charles Hansen. Ray-driven dynamic working set rendering: For complex volume scene graphs involving large point clouds. Vis. Comput. 23, 3 (2007), 167–179. [doi]
    BibTeX 
    @article{1229162,
  author = {Chisnall, David and Chen, Min and Hansen, Charles},
  title = {Ray-driven dynamic working set rendering: For complex volume scene graphs involving large point clouds},
  journal = {Vis. Comput.},
  volume = {23},
  number = {3},
  year = {2007},
  issn = {0178-2789},
  pages = {167--179},
  doi = {http://dx.doi.org/10.1007/s00371-006-0091-6},
  publisher = {Springer-Verlag New York, Inc.},
  address = {Secaucus, NJ, USA}
}
    Abstract

    Ray tracing a volume scene graph composed of multiple point-based volume objects (PBVO) can produce high quality images with effects such as shadows and constructive operations. A naive approach, however, would demand an overwhelming amount of memory to accommodate all point datasets and their associated control structures such as octrees. This paper describes an out-of-core approach for rendering such a scene graph in a scalable manner. In order to address the difficulty in pre-determining the order of data caching, we introduce a technique based on a dynamic, in-core working set. We present a ray-driven algorithm for predicting the working set automatically. This allows both the data and the control structures required for ray tracing to be dynamically pre-fetched according to access patterns determined based on captured knowledge of ray-data intersection. We have conducted a series of experiments on the scalability of the technique using working sets and datasets of different sizes. With the aid of both qualitative and quantitative analysis, we demonstrate that this approach allows the rendering of multiple large PBVOs in a volume scene graph to be performed on desktop computers.

  35. David Chisnall and Min Chen. The Making of SimEAC. ICAC ’06: Proceedings of the 2006 IEEE International Conference on Autonomic Computing, IEEE Computer Society (2006), 301–302. [doi]
    BibTeX 
    @inproceedings{1471676,
  author = {Chisnall, David and Min Chen},
  title = {The Making of SimEAC},
  booktitle = {ICAC '06: Proceedings of the 2006 IEEE International Conference on Autonomic Computing},
  year = {2006},
  isbn = {1-4244-0175-5},
  pages = {301--302},
  doi = {http://dx.doi.org/10.1109/ICAC.2006.1662417},
  publisher = {IEEE Computer Society},
  address = {Washington, DC, USA}
}
    Abstract

    In this short paper, we give a brief overview a simulation environment, SimEAC, which was designed for testing algorithms with strong autonomic features. SimEAC enables a user to configure a system infrastructure to be simulated by specifying a collection of hardware attributes and it provides a fine degree of control over operating system and task simulation, hence allowing a variety of autonomic algorithms to be prototyped on a virtual system infrastructure.

  36. David Chisnall, Min Chen and Charles Hansen. Knowledge-based out-of-core algorithms for data management in visualization. EUROVIS’06: Proceedings of the Eighth Joint Eurographics / IEEE VGTC conference on Visualization, Eurographics Association (2006), 107–114. [doi]
    BibTeX 
    @inproceedings{2384813,
  author = {Chisnall, David and Chen, Min and Hansen, Charles},
  title = {Knowledge-based out-of-core algorithms for data management in visualization},
  booktitle = {EUROVIS'06: Proceedings of the Eighth Joint Eurographics / IEEE VGTC conference on Visualization},
  year = {2006},
  isbn = {3-905673-31-2},
  pages = {107--114},
  location = {Lisbon, Portugal},
  doi = {http://dx.doi.org/10.2312/VisSym/EuroVis06/107-114},
  publisher = {Eurographics Association},
  address = {Aire-la-Ville, Switzerland, Switzerland}
}
    Abstract

    Data management is the very first issue in handling very large datasets. Many existing out-of-core algorithms used in visualization are closely coupled with application-specific logic. This paper presents two knowledgebased out-of-core prefetching algorithms that do not use hard-coded rendering-related logic. They acquire the knowledge of the access history and patterns dynamically, and adapt their prefetching strategies accordingly. We have compared the algorithms with a demand-based algorithm, as well as a more domain-specific out-of-core algorithm. We carried out our evaluation in conjunction with an example application where rendering multiple point sets in a volume scene graph put a great strain on the rendering algorithm in terms of memory management. Our results have shown that the knowledge-based approach offers a better cache-hit to disk-access trade-off. This work demonstrates that it is possible to build an out-of-core prefetching algorithm without depending on rendering-related application-specific logic. The knowledge based approach has the advantage of being generic, efficient, flexible and self-adaptive.

  37. Ken Brodlie, John Brooke, Min Chen, David Chisnall, Ade Fewings, Chris Hughes, Nigel W. John, Mark W. Jones, Mark Riding and Nicolas Roard. Visual Supercomputing - Technologies, Applications and Challenges. Computer Graphics Forum, 2 (2005), 217–245.
    BibTeX 
    @article{brodlie05eviz,
  author = {Brodlie, Ken and Brooke, John and Chen, Min and Chisnall, David and Fewings, Ade and Hughes, Chris and John, Nigel W. and Jones, Mark W. and Riding, Mark and Roard, Nicolas},
  title = {Visual Supercomputing - Technologies, Applications and Challenges},
  booktitle = {Computer Graphics Forum},
  year = {2005},
  issue = {2},
  number = {24},
  pages = {217--245}
}
  38. K. W. Brodlie, J. Brooke, M. Chen, D. Chisnall, C. J. Hughes, Nigel W. John, M. W. Jones, M. Riding, N. Roard, M. Turner and J. D. Wood. Adaptive Infrastructure for Visual Computing. Theory and Practice of Computer Graphics, (2007), 147–156.
    BibTeX 
    @inproceedings{brodlie:2007,
  author = {Brodlie, K. W. and Brooke, J. and Chen, M. and Chisnall, D. and Hughes, C. J. and John, Nigel W. and Jones, M. W. and Riding, M. and Roard, N. and Turner, M. and Wood, J. D.},
  title = {Adaptive Infrastructure for Visual Computing},
  booktitle = {Theory and Practice of Computer Graphics},
  year = {2007},
  pages = {147--156}
}
  39. David Chisnall. A Modern Objective-C Runtime. Journal of Object Technology 8, 1 (2009), 221–240. [pdf] [doi]
    BibTeX 
    @article{Chisnall:09:libobjc,
  author = {Chisnall, David},
  title = {A Modern Objective-C Runtime},
  journal = {Journal of Object Technology},
  volume = {8},
  number = {1},
  month = jan,
  year = {2009},
  pages = {221--240},
  pdf = {http://www.jot.fm/issues/issue_2009_01/article4.pdf},
  doi = {http://dx.doi.org/10.5381/jot.2009.8.1.a4}
}
    Abstract

    In light of the recent modifications to the de facto standard implementation Objective-C language by Apple Inc., the GNU Objective-C runtime lacks a number of features that are desirable for a modern implementation.

    This paper presents a metaobject protocol flexible enough to implement Objective-C and other languages of interest. It also presents an implementation of this model in the form of a new Objective-C runtime library which supports all of the new features of Objective-C 2.0 as well as safe inline caching, mixins, prototype-based object orientation, transparent support for other languages—including those with a prototype-based object model—and a small, maintainable code base.

Books

  1. David Chisnall. Objective-C Phrasebook. Addison-Wesley Professional, 2011.
    BibTeX 
    @book{1996266,
  author = {Chisnall, David},
  title = {Objective-C Phrasebook},
  year = {2011},
  isbn = {0321743628, 9780321743626},
  publisher = {Addison-Wesley Professional}
}
  2. David Chisnall. Go Programming Language Phrasebook. Addison-Wesley Professional, 2012.
    BibTeX 
    @book{gophrasebook,
  author = {Chisnall, David},
  title = {Go Programming Language Phrasebook},
  year = {2012},
  isbn = {0321817141, 9780321817143},
  publisher = {Addison-Wesley Professional}
}
  3. David Chisnall. Cocoa Programming Developer’s Handbook. Addison-Wesley Professional, 2010.
    BibTeX 
    @book{1875306,
  author = {Chisnall, David},
  title = {Cocoa Programming Developer's Handbook},
  year = {2010},
  isbn = {0321695003, 9780321695000, 0321639634, 9780321639639},
  publisher = {Addison-Wesley Professional}
}
  4. David Chisnall. The Definitive Guide to the Xen Hypervisor (Prentice Hall Open Source Software Development Series). Prentice Hall PTR, Upper Saddle River, NJ, USA, 2007.
    BibTeX 
    @book{1324849,
  author = {Chisnall, David},
  title = {The Definitive Guide to the Xen Hypervisor (Prentice Hall Open Source Software Development Series)},
  year = {2007},
  isbn = {013234971X},
  publisher = {Prentice Hall PTR},
  address = {Upper Saddle River, NJ, USA}
}

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.

  2. Tony Chen and David Chisnall. Pointer Tagging for Memory Safety. Microsoft, 2019. [pdf]
    BibTeX 
    @techreport{chen2019pointer,
  author = {Chen, Tony and Chisnall, David},
  title = {Pointer Tagging for Memory Safety},
  institution = {Microsoft},
  year = {2019},
  month = jul,
  url = {https://www.microsoft.com/en-us/research/publication/pointer-tagging-for-memory-safety/},
  pdf = {https://www.microsoft.com/en-us/research/uploads/prod/2019/07/Pointer-Tagging-for-Memory-Safety.pdf},
  number = {MSR-TR-2019-17}
}
    Abstract

    Memory safety attacks continue to be prevalent on computer systems in use today, as large amounts of unsafe C/C++ code continues to provide attackers with a large supply of buffer overrun, use after free and type confusion bugs. This paper proposes a fundamental instruction set architecture change to combat memory safety problems. The ISA change is mostly transparent to application code and typically only requires a recompilation of the application to gain the security benefits. The change involves having the CPU hold two extra tag bits to the side of each piece of 64-bit data to denote whether the data holds a code/data pointer or not. By doing this, we can prevent attackers from using ‘data’ to corrupt ‘pointers’ and cause undesired damage. We believe the proposed architecture change enables stronger control flow protection than shadow stack (Intel CET) plus Control Flow Guard (CFG) with less performance overhead. Thus, this ISA change not only enhances security, but does so while improving performance.

  3. Robert N. M. Watson, Peter G. Neumann, Jonathan Woodruff, Michael Roe, Jonathan Anderson, John Baldwin, David Chisnall, Brooks Davis, Alexandre Joannou, Ben Laurie, Simon W. Moore, Steven J. Murdoch, Robert Norton, Stacey Son and Hongyan Xia. Capability Hardware Enhanced RISC Instructions: CHERI Instruction-Set Architecture (Version 6). University of Cambridge, Computer Laboratory, 2017. [pdf]
    BibTeX 
    @techreport{UCAM-CL-TR-907,
  author = {Watson, Robert N. M. and Neumann, Peter G. and Woodruff, Jonathan and Roe, Michael and Anderson, Jonathan and Baldwin, John and Chisnall, David and Davis, Brooks and Joannou, Alexandre and Laurie, Ben and Moore, Simon W. and Murdoch, Steven J. and Norton, Robert and Son, Stacey and Xia, Hongyan},
  title = {{Capability Hardware Enhanced RISC Instructions: CHERI
           	   Instruction-Set Architecture (Version 6)}},
  year = {2017},
  month = apr,
  url = {http://www.cl.cam.ac.uk/techreports/UCAM-CL-TR-907.pdf},
  institution = {University of Cambridge, Computer Laboratory},
  number = {UCAM-CL-TR-907}
}
  4. Robert N. M. Watson, Peter G. Neumann, Jonathan Woodruff, Michael Roe, Jonathan Anderson, David Chisnall, Brooks Davis, Alexandre Joannou, Ben Laurie, Simon W. Moore, Steven J. Murdoch, Robert Norton, Stacey Son and Hongyan Xia. Capability Hardware Enhanced RISC Instructions: CHERI Instruction-Set Architecture (Version 5). University of Cambridge, Computer Laboratory, 2016. [pdf]
    BibTeX 
    @techreport{UCAM-CL-TR-891,
  author = {Watson, Robert N. M. and Neumann, Peter G. and Woodruff, Jonathan and Roe, Michael and Anderson, Jonathan and Chisnall, David and Davis, Brooks and Joannou, Alexandre and Laurie, Ben and Moore, Simon W. and Murdoch, Steven J. and Norton, Robert and Son, Stacey and Xia, Hongyan},
  title = {{Capability Hardware Enhanced RISC Instructions: CHERI
           	   Instruction-Set Architecture (Version 5)}},
  year = {2016},
  month = jun,
  url = {http://www.cl.cam.ac.uk/techreports/UCAM-CL-TR-891.pdf},
  institution = {University of Cambridge, Computer Laboratory},
  number = {UCAM-CL-TR-891}
}
    Abstract

    This technical report describes CHERI ISAv5, the fifth version of the Capability Hardware Enhanced RISC Instructions (CHERI) Instruction-Set Architecture (ISA) being developed by SRI International and the University of Cambridge. This design captures six years of research, development, refinement, formal analysis, and testing, and is a substantial enhancement to the ISA versions described in earlier technical reports. This version introduces the CHERI-128 “compressed” capability format, adds further capability instructions to improve code generation, and rationalizes a number of ISA design choices (such as system permissions) as we have come to better understand mappings from C programming-language and MMU-based operating-system models into CHERI. It also contains improvements to descriptions, explanations, and rationale.

    The CHERI instruction set is based on a hybrid capability-system architecture that adds new capability-system primitives to a commodity 64-bit RISC ISA enabling software to efficiently implement fine-grained memory protection and a hardware-software object-capability security model. These extensions support incrementally adoptable, high-performance, formally based, programmer-friendly underpinnings for fine-grained software decomposition and compartmentalization, motivated by and capable of enforcing the principle of least privilege. Fine-grained memory protection also provides direct mitigation of many widely deployed exploit techniques.

    The CHERI system architecture purposefully addresses known performance and robustness gaps in commodity ISAs that hinder the adoption of more secure programming models centered around the principle of least privilege. To this end, CHERI blends traditional paged virtual memory with a per-address-space capability model that includes capability registers, capability instructions, and tagged memory that have been added to the 64-bit MIPS ISA. CHERI learns from the C-language fat-pointer literature: its capabilities describe fine-grained regions of memory and can be substituted for data or code pointers in generated code, protecting data and also providing Control-Flow Integrity (CFI). Strong monotonicity properties allow the CHERI capability model to express a variety of protection properties, from valid C-language pointer provenance and C-language bounds checking to implementing the isolation and controlled communication structures required for compartmentalization.

    CHERI’s hybrid system approach, inspired by the Capsicum security model, allows incremental adoption of capability-oriented software design: software implementations that are more robust and resilient can be deployed where they are most needed, while leaving less critical software largely unmodified, but nevertheless suitably constrained to be incapable of having adverse effects. For example, we are focusing conversion efforts on low-level TCB components of the system: separation kernels, hypervisors, operating-system kernels, language runtimes, and userspace TCBs such as web browsers. Likewise, we see early-use scenarios (such as data compression, protocol parsing, image processing, and video processing) that relate to particularly high-risk software libraries, which are concentrations of both complex and historically vulnerability-prone code combined with untrustworthy data sources, while leaving containing applications unchanged.

  5. Robert N. M. Watson, Peter G. Neumann, Jonathan Woodruff, Michael Roe, Jonathan Anderson, David Chisnall, Brooks Davis, Alexandre Joannou, Ben Laurie, Simon W. Moore, Steven J. Murdoch, Robert Norton and Stacey Son. Capability Hardware Enhanced RISC Instructions: CHERI Instruction-Set Architecture. University of Cambridge, Computer Laboratory, 2015. [pdf]
    BibTeX 
    @techreport{UCAM-CL-TR-876,
  author = {Watson, Robert N. M. and Neumann, Peter G. and Woodruff, Jonathan and Roe, Michael and Anderson, Jonathan and Chisnall, David and Davis, Brooks and Joannou, Alexandre and Laurie, Ben and Moore, Simon W. and Murdoch, Steven J. and Norton, Robert and Son, Stacey},
  title = {{Capability Hardware Enhanced RISC Instructions: CHERI
           	   Instruction-Set Architecture}},
  year = {2015},
  month = sep,
  url = {http://www.cl.cam.ac.uk/techreports/UCAM-CL-TR-876.pdf},
  institution = {University of Cambridge, Computer Laboratory},
  number = {UCAM-CL-TR-876}
}
  6. Robert N. M. Watson, David Chisnall, Brooks Davis, Wojciech Koszek, Simon W. Moore, Steven J. Murdoch, Peter G. Neumann and Jonathan Woodruff. Capability Hardware Enhanced RISC Instructions: CHERI Programmer’s Guide. University of Cambridge, Computer Laboratory, 2015. [pdf]
    BibTeX 
    @techreport{UCAM-CL-TR-877,
  author = {Watson, Robert N. M. and Chisnall, David and Davis, Brooks and Koszek, Wojciech and Moore, Simon W. and Murdoch, Steven J. and Neumann, Peter G. and Woodruff, Jonathan},
  title = {{Capability Hardware Enhanced RISC Instructions: CHERI
           	   Programmer's Guide}},
  year = {2015},
  month = sep,
  url = {http://www.cl.cam.ac.uk/techreports/UCAM-CL-TR-877.pdf},
  institution = {University of Cambridge, Computer Laboratory},
  number = {UCAM-CL-TR-877}
}
    Abstract

    This work presents CHERI, a practical extension of the 64-bit MIPS instruction set to support capabilities for fine-grained memory protection.

    Traditional paged memory protection has proved inadequate in the face of escalating security threats and proposed solutions include fine-grained protection tables (Mondrian Memory Protection) and hardware fat-pointer protection (Hardbound). These have emphasised transparent protection for C executables but have lacked flexibility and practicality. Intel’s recent memory protection extensions (iMPX) attempt to adopt some of these ideas and are flexible and optional but lack the strict correctness of these proposals.

    Capability addressing has been the classical solution to efficient and strong memory protection but it has been thought to be incompatible with common instruction sets and also with modern program structure which uses a flat memory space with global pointers.

    CHERI is a fusion of capabilities with a paged flat memory producing a program-managed fat pointer capability model. This protection mechanism scales from application sandboxing to efficient byte-level memory safety with per-pointer permissions. I present an extension to the 64-bit MIPS architecture on FPGA that runs standard FreeBSD and supports self-segmenting applications in user space.

    Unlike other recent proposals, the CHERI implementation is open-source and of sufficient quality to support software development as well as community extension of this work. I compare with published memory safety mechanisms and demonstrate competitive performance while providing assurance and greater flexibility with simpler hardware requirements.

  7. Robert N. M. Watson, David Chisnall, Brooks Davis, Wojciech Koszek, Simon W. Moore, Steven J. Murdoch, Peter G. Neumann and Jonathan Woodruff. Bluespec Extensible RISC Implementation: BERI Software reference. University of Cambridge, Computer Laboratory, 2015. [pdf]
    BibTeX 
    @techreport{UCAM-CL-TR-869,
  author = {Watson, Robert N. M. and Chisnall, David and Davis, Brooks and Koszek, Wojciech and Moore, Simon W. and Murdoch, Steven J. and Neumann, Peter G. and Woodruff, Jonathan},
  title = {{Bluespec Extensible RISC Implementation: BERI Software
           	   reference}},
  year = {2015},
  month = apr,
  url = {http://www.cl.cam.ac.uk/techreports/UCAM-CL-TR-869.pdf},
  institution = {University of Cambridge, Computer Laboratory},
  number = {UCAM-CL-TR-869}
}
    Abstract

    The BERI Software Reference documents how to build and use the FreeBSD operating system on the Bluespec Extensible RISC Implementation (BERI) developed by SRI International and the University of Cambridge. The reference is targeted at hardware and software programmers who will work with BERI or BERI-derived systems.

  8. Robert N. M. Watson, Jonathan Woodruff, David Chisnall, Brooks Davis, Wojciech Koszek, A. Theodore Markettos, Simon W. Moore, Steven J. Murdoch, Peter G. Neumann, Robert Norton and Michael Roe. Bluespec Extensible RISC Implementation: BERI Hardware reference. University of Cambridge, Computer Laboratory, 2015. [pdf]
    BibTeX 
    @techreport{UCAM-CL-TR-868,
  author = {Watson, Robert N. M. and Woodruff, Jonathan and Chisnall, David and Davis, Brooks and Koszek, Wojciech and Markettos, A. Theodore and Moore, Simon W. and Murdoch, Steven J. and Neumann, Peter G. and Norton, Robert and Roe, Michael},
  title = {{Bluespec Extensible RISC Implementation: BERI Hardware
           	   reference}},
  year = {2015},
  month = apr,
  url = {http://www.cl.cam.ac.uk/techreports/UCAM-CL-TR-868.pdf},
  institution = {University of Cambridge, Computer Laboratory},
  number = {UCAM-CL-TR-868}
}
  9. Robert N. M. Watson, Peter G. Neumann, Jonathan Woodruff, Jonathan Anderson, David Chisnall, Brooks Davis, Ben Laurie, Simon W. Moore, Steven J. Murdoch and Michael Roe. Capability Hardware Enhanced RISC Instructions: CHERI Instruction-set architecture. University of Cambridge, Computer Laboratory, 15 JJ Thomson Avenue, Cambridge CB3 0FD, United Kingdom, phone +44 1223 763500, 2014.
    BibTeX 
    @techreport{UCAM-CL-TR-864,
  author = {Watson, Robert N. M. and Neumann, Peter G. and Woodruff, Jonathan and Anderson, Jonathan and Chisnall, David and Davis, Brooks and Laurie, Ben and Moore, Simon W. and Murdoch, Steven J. and Roe, Michael},
  title = {{Capability Hardware Enhanced RISC Instructions: CHERI
           	   Instruction-set architecture}},
  year = {2014},
  month = dec,
  institution = {University of Cambridge, Computer Laboratory},
  address = {15 JJ Thomson Avenue, Cambridge CB3 0FD, United Kingdom,
            	  phone +44 1223 763500},
  number = {UCAM-CL-TR-864}
}
    Abstract

    This technical report describes CHERI ISAv3, the third version of the Capability Hardware Enhanced RISC Instructions (CHERI) Instruction-Set Architecture (ISA). CHERI is being developed by SRI International and the University of Cambridge. This design captures four years of development, refinement, formal analysis, and testing, and is a substantial enhancement to their ISA version described in UCAM-CL-TR-850. Key improvements lie in tighter C-language integration, and more mature support for software object-capability models; these changes result from experience gained in adapting software to run on prototype hardware.

    The CHERI instruction set is based on a hybrid capability-system architecture that adds new capability-system primitives to a commodity 64-bit RISC ISA enabling software to efficiently implement fine-grained memory protection and a hardware-software object-capability security model. These extensions support incrementally adoptable, high-performance, formally based, programmer-friendly underpinnings for fine-grained software decomposition and compartmentalization, motivated by and capable of enforcing the principle of least privilege. The CHERI system architecture purposefully addresses known performance and robustness gaps in commodity ISAs that hinder the adoption of more secure programming models centered around the principle of least privilege. To this end, CHERI blends traditional paged virtual memory with a per-address-space capability model that includes capability registers, capability instructions, and tagged memory that have been added to the 64-bit MIPS ISA via a new capability coprocessor. CHERI also learns from the C-language fat-pointer literature; CHERI capabilities can describe not only regions of memory, but can also capture C pointer semantics allowing substitution for pointers in generated code.

    CHERI’s hybrid system approach, inspired by the Capsicum security model, allows incremental adoption of capability-oriented software design: software implementations that are more robust and resilient can be deployed where they are most needed, while leaving less critical software largely unmodified, but nevertheless suitably constrained to be incapable of having adverse effects. For example, we are focusing conversion efforts on low-level TCB components of the system: separation kernels, hypervisors, operating system kernels, language runtimes, and userspace TCBs such as web browsers. Likewise, we see early-use scenarios (such as data compression, protocol parsing, image processing, and video processing) that relate to particularly high-risk software libraries, which are concentrations of both complex and historically vulnerability-prone code combined with untrustworthy data sources, while leaving containing applications unchanged.

    This report describes the CHERI Instruction-Set Architecture (ISA) and design, and provides reference documentation and potential memory models, along with their requirements. It also briefly addresses the CHERI system hardware-software architecture, documenting our current thinking on integrating programming languages and operating systems with the CHERI hardware.

  10. Robert N.M. Watson, David Chisnall, Brooks Davis, Wojciech Koszek, Simon W. Moore, Steven J. Murdoch, Peter G. Neumann and Jonathan Woodruff. Bluespec Extensible RISC Implementation: BERI Software reference. University of Cambridge, Computer Laboratory, 2014. [pdf]
    BibTeX 
    @techreport{UCAM-CL-TR-853,
  author = {Watson, Robert N.M. and Chisnall, David and Davis, Brooks and Koszek, Wojciech and Moore, Simon W. and Murdoch, Steven J. and Neumann, Peter G. and Woodruff, Jonathan},
  title = {{Bluespec Extensible RISC Implementation: BERI Software reference}},
  year = {2014},
  month = apr,
  url = {http://www.cl.cam.ac.uk/techreports/UCAM-CL-TR-853.pdf},
  institution = {University of Cambridge, Computer Laboratory},
  number = {UCAM-CL-TR-853}
}
    Abstract

    The BERI Software Reference documents how to build and use FreeBSD on the Bluespec Extensible RISC Implementation (BERI) developed by SRI International and the University of Cambridge. The reference is targeted at hardware and software programmers who will work with BERI or BERI-derived systems.

  11. Robert N.M. Watson, Jonathan Woodruff, David Chisnall, Brooks Davis, Wojciech Koszek, A. Theodore Markettos, Simon W. Moore, Steven J. Murdoch, Peter G. Neumann, Robert Norton and Michael Roe. Bluespec Extensible RISC Implementation: BERI Hardware reference. University of Cambridge, Computer Laboratory, 2014. [pdf]
    BibTeX 
    @techreport{UCAM-CL-TR-852,
  author = {Watson, Robert N.M. and Woodruff, Jonathan and Chisnall, David and Davis, Brooks and Koszek, Wojciech and Markettos, A. Theodore and Moore, Simon W. and Murdoch, Steven J. and Neumann, Peter G. and Norton, Robert and Roe, Michael},
  title = {{Bluespec Extensible RISC Implementation: BERI Hardware reference}},
  year = {2014},
  month = apr,
  url = {http://www.cl.cam.ac.uk/techreports/UCAM-CL-TR-852.pdf},
  institution = {University of Cambridge, Computer Laboratory},
  number = {UCAM-CL-TR-852}
}
    Abstract

    The BERI Hardware Reference documents the Bluespec Extensible RISC Implementation (BERI) developed by SRI International and the University of Cambridge. The reference is targeted at hardware and software developers working with the BERI1 and BERI2 processor prototypes in simulation and synthesized to FPGA targets. We describe how to use the BERI1 and BERI2 processors in simulation, the BERI1 debug unit, the BERI unit-test suite, how to use BERI with Altera FPGAs and Terasic DE4 boards, the 64-bit MIPS and CHERI ISAs implemented by the prototypes, the BERI1 and BERI2 processor implementations themselves, and the BERI Programmable Interrupt Controller (PIC).

  12. Robert N.M. Watson, David Chisnall, Brooks Davis, Wojciech Koszek, Simon W. Moore, Steven J. Murdoch, Peter G. Neumann and Jonathan Woodruff. Capability Hardware Enhanced RISC Instructions: CHERI User’s guide. University of Cambridge, Computer Laboratory, 2014. [pdf]
    BibTeX 
    @techreport{UCAM-CL-TR-851,
  author = {Watson, Robert N.M. and Chisnall, David and Davis, Brooks and Koszek, Wojciech and Moore, Simon W. and Murdoch, Steven J. and Neumann, Peter G. and Woodruff, Jonathan},
  title = {{Capability Hardware Enhanced RISC Instructions: CHERI
           	   User's guide}},
  year = {2014},
  month = apr,
  url = {http://www.cl.cam.ac.uk/techreports/UCAM-CL-TR-851.pdf},
  institution = {University of Cambridge, Computer Laboratory},
  number = {UCAM-CL-TR-851}
}
    Abstract

    The CHERI User’s Guide documents the software environment for the Capability Hardware Enhanced RISC Instructions (CHERI) prototype developed by SRI International and the University of Cambridge. The User’s Guide is targeted at hardware and software developers working with capability-enhanced software. It describes the CheriBSD operating system, a version of the FreeBSD operating system that has been adapted to support userspace capability systems via the CHERI ISA, and the CHERI Clang/LLVM compiler suite. It also describes the earlier Deimos demonstration microkernel.

  13. Robert N.M. Watson, Peter G. Neumann, Jonathan Woodruff, Jonathan Anderson, David Chisnall, Brooks Davis, Ben Laurie, Simon W. Moore, Steven J. Murdoch and Michael Roe. Capability Hardware Enhanced RISC Instructions: CHERI Instruction-set architecture. University of Cambridge, Computer Laboratory, 2014. [pdf]
    BibTeX 
    @techreport{UCAM-CL-TR-850,
  author = {Watson, Robert N.M. and Neumann, Peter G. and Woodruff, Jonathan and Anderson, Jonathan and Chisnall, David and Davis, Brooks and Laurie, Ben and Moore, Simon W. and Murdoch, Steven J. and Roe, Michael},
  title = {{Capability Hardware Enhanced RISC Instructions: CHERI
           	   Instruction-set architecture}},
  year = {2014},
  month = apr,
  url = {http://www.cl.cam.ac.uk/techreports/UCAM-CL-TR-850.pdf},
  institution = {University of Cambridge, Computer Laboratory},
  number = {UCAM-CL-TR-850}
}
    Abstract

    This document describes the rapidly maturing design for the Capability Hardware Enhanced RISC Instructions (CHERI) Instruction-Set Architecture (ISA), which is being developed by SRI International and the University of Cambridge. The document is intended to capture our evolving architecture, as it is being refined, tested, and formally analyzed. We have now reached 70% of the time for our research and development cycle.

    CHERI is a hybrid capability-system architecture that combines new processor primitives with the commodity 64-bit RISC ISA enabling software to efficiently implement fine-grained memory protection and a hardware-software object-capability security model. These extensions support incrementally adoptable, high-performance, formally based, programmer-friendly underpinnings for fine-grained software decomposition and compartmentalization, motivated by and capable of enforcing the principle of least privilege. The CHERI system architecture purposefully addresses known performance and robustness gaps in commodity ISAs that hinder the adoption of more secure programming models centered around the principle of least privilege. To this end, CHERI blends traditional paged virtual memory with a per-address-space capability model that includes capability registers, capability instructions, and tagged memory that have been added to the 64-bit MIPS ISA via a new capability coprocessor.

    CHERI’s hybrid approach, inspired by the Capsicum security model, allows incremental adoption of capability-oriented software design: software implementations that are more robust and resilient can be deployed where they are most needed, while leaving less critical software largely unmodified, but nevertheless suitably constrained to be incapable of having adverse effects. For example, we are focusing conversion efforts on low-level TCB components of the system: separation kernels, hypervisors, operating system kernels, language runtimes, and userspace TCBs such as web browsers. Likewise, we see early-use scenarios (such as data compression, image processing, and video processing) that relate to particularly high-risk software libraries, which are concentrations of both complex and historically vulnerability-prone code combined with untrustworthy data sources, while leaving containing applications unchanged.

    This report describes the CHERI architecture and design, and provides reference documentation for the CHERI instruction-set architecture (ISA) and potential memory models, along with their requirements. It also documents our current thinking on integration of programming languages and operating systems. Our ongoing research includes two prototype processors employing the CHERI ISA, each implemented as an FPGA soft core specified in the Bluespec hardware description language (HDL), for which we have integrated the application of formal methods to the Bluespec specifications and the hardware-software implementation.