Publications


Download a complete list of publications as BibTeX

Articles

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

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

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

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

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

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

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

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

  6. 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]
    @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}
    }
    
  7. 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]
    @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.

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

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

  10. David Chisnall. No such thing as a general-purpose processor. Communications of the ACM 57, 12 (2014), 44–48. [pdf] [doi]
    @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}
    }
    
  11. David Chisnall. Smalltalk in a C world. Science of Computer Programming 96, Part 1, 0 (2014), 4–16. [doi]
    @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.

  12. David Chisnall. There’s No Such Thing As a General-purpose Processor. Queue 12, 10 (2014), 20:20–20:25. [doi]
    @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}
    }
    
  13. 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]
    @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

  14. David Chisnall. LLVM in the FreeBSD Toolchain. Proceedings of AsiaBSDCon 2014, (2014). [pdf]
    @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}
    }
    
  15. 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]
    @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.

  16. David Chisnall. The challenge of cross-language interoperability. Communications of the ACM 56, 12 (2013), 50–56. [pdf] [doi]
    @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.

  17. David Chisnall. The Challenge of Cross-language Interoperability. Queue 11, 10 (2013), 20–28. [pdf] [doi]
    @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.

  18. David Chisnall. A new Objective-C runtime: from research to production. Communications of the ACM 55, 9 (2012), 44–47. [pdf] [doi]
    @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}
    }
    
  19. David Chisnall. Smalltalk in a C world. IWST ’12: Proceedings of the International Workshop on Smalltalk Technologies, ACM (2012), 1–12. [pdf] [doi]
    @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.

  20. David Chisnall. A New Objective-C Runtime: from Research to Production. Queue 10, 7 (2012), 20–24. [doi]
    @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}
    }
    
  21. David Chisnall. A Modern Objective-C Runtime. Journal of Object Technology 8, 1 (2009), 221–240. [pdf] [doi]
    @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.

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

  23. 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.
    @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}
    }
    
  24. 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]
    @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.

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

  26. 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.
    @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}
    }
    

Books

  1. David Chisnall. Go Programming Language Phrasebook. Addison-Wesley Professional, 2012.
    @book{gophrasebook,
      author = {Chisnall, David},
      title = {Go Programming Language Phrasebook},
      year = {2012},
      isbn = {0321817141, 9780321817143},
      publisher = {Addison-Wesley Professional}
    }
    
  2. David Chisnall. Objective-C Phrasebook. Addison-Wesley Professional, 2011.
    @book{1996266,
      author = {Chisnall, David},
      title = {Objective-C Phrasebook},
      year = {2011},
      isbn = {0321743628, 9780321743626},
      publisher = {Addison-Wesley Professional}
    }
    
  3. David Chisnall. Cocoa Programming Developer’s Handbook. Addison-Wesley Professional, 2010.
    @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.
    @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. 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]
    @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}
    }
    
  2. 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]
    @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.

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

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

  6. 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]
    @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}
    }
    
  7. 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.
    @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.

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

  9. 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]
    @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).

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

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