Task 2 Papers
[1] |
Kyndylan Nienhuis, Alexandre Joannou, Thomas Bauereiss, Anthony Fox, Michael
Roe, Brian Campbell, Matthew Naylor, Robert M. Norton, Simon W. Moore,
Peter G. Neumann, Ian Stark, Robert N. M. Watson, and Peter Sewell.
Rigorous engineering for hardware security: Formal modelling and
proof in the CHERI design and implementation process.
In Security and Privacy 2020: Proceedings of the 41st
IEEE Symposium on Security and Privacy (SP), May 2020.
[ bib |
.pdf ]
The root causes of many security vulnerabilities include a pernicious combination of two problems, often regarded as inescapable aspects of computing. First, the protection mechanisms provided by the mainstream processor architecture and C/C++ language abstractions, dating back to the 1970s and before, provide only coarse-grain virtual-memory-based protection. Second, mainstream system engineering relies almost exclusively on test-and-debug methods, with (at best) prose specifications. These methods have historically sufficed commercially for much of the computer industry, but they fail to prevent large numbers of exploitable bugs, and the security problems that this causes are becoming ever more acute. |
[2] |
Ben Simner, Shaked Flur, Christopher Pulte, Alasdair Armstrong, Jean
Pichon-Pharabod, Luc Maranget, and Peter Sewell.
ARMv8-A system semantics: instruction fetch in relaxed
architectures (extended version).
In ESOP 2020: Proceedings of the 29th European
Symposium on Programming, April 2020.
This is an extended version of the ESOP 2020 paper, with appendices
giving additional details.
[ bib |
.pdf ]
Computing relies on architecture specifications to decouple hardware and software development. Historically these have been prose documents, with all the problems that entails, but research over the last ten years has developed rigorous and executable-as-test-oracle specifications of mainstream architecture instruction sets and “user-mode” concurrency, clarifying architectures and bringing them into the scope of programming-language semantics and verification. However, the system semantics, of instruction-fetch and cache maintenance, exceptions and interrupts, and address translation, remains obscure, leaving us without a solid foundation for verification of security-critical systems software. |
[3] |
J. Woodruff, A. Joannou, H. Xia, A. Fox, R. M. Norton, D. Chisnall,
B. Davis, K. Gudka, N. W. Filardo, A. T. Markettos, M. Roe, P. G.
Neumann, R. N. M. Watson, and S. W. Moore.
Cheri concentrate: Practical compressed capabilities.
IEEE Transactions on Computers, 68(10):1455--1469, October
2019.
[ bib |
DOI |
.pdf ]
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 to enforce 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 elsewhere that do not support legacy instruction sets, ignore features critical to the existing software base, and also introduce 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 present the first quantitative analysis of compiled capability code, which we use to guide the design of the encoding format. 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 to 75 percent 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. Keywords: data compression;decoding;encoding;field programmable gate arrays;microprocessor chips;pipeline processing;program compilers;reduced instruction set computing;storage management;theorem proving;tree data structures;practical compressed capabilities;fat-pointer compression scheme;developed capability-pointer system;capability fat pointers;nonbypassable security properties;future computer systems;increased pointer size;capability compression;legacy instruction sets;existing software base;design inefficiencies;RISC-style processor pipelines;state-of-the-art region-encoding efficiency;compressed encoding;legacy software stack;compiled capability code;encoding format;open-source CHERI prototype processor design;pointer arithmetic;decode;pointer-modify operations;commodity operating system;CHERI concentrate;pipeline problems;efficiency 75.0 percent;Encoding;Pipelines;Delays;Safety;Software;Semantics;Registers;Capabilities;fat pointers;compression;memory safety;computer architecture |
[4] |
Robert N. M. Watson, Simon W. Moore, Peter Sewell, and Peter Neumann.
An introduction to CHERI.
Technical Report UCAM-CL-TR-941, University of Cambridge, Computer
Laboratory, September 2019.
[ bib |
.pdf ]
|
[5] |
Kyndylan Nienhuis, Alexandre Joannou, Anthony Fox, Michael Roe, Thomas
Bauereiss, Brian Campbell, Matthew Naylor, Robert M. Norton, Simon W. Moore,
Peter G. Neumann, Ian Stark, Robert N. M. Watson, and Peter Sewell.
Rigorous engineering for hardware security: Formal modelling and
proof in the CHERI design and implementation process.
Technical Report UCAM-CL-TR-940, University of Cambridge, Computer
Laboratory, September 2019.
[ bib |
.pdf ]
The root causes of many security vulnerabilities include a pernicious combination of two problems, often regarded as inescapable aspects of computing. First, the protection mechanisms provided by the mainstream processor architecture and C/C++ language abstractions, dating back to the 1970s and before, provide only coarse-grain virtual-memory-based protection. Second, mainstream system engineering relies almost exclusively on test-and-debug methods, with (at best) prose specifications. These methods have historically sufficed commercially for much of the computer industry, but they fail to prevent large numbers of exploitable bugs, and the security problems that this causes are becoming ever more acute. |
[6] |
Robert N. M. Watson, Peter G. Neumann, Jonathan Woodruff, Michael Roe, Hesham
Almatary, Jonathan Anderson, John Baldwin, David Chisnall, Brooks Davis,
Nathaniel Wesley Filardo, Alexandre Joannou, Ben Laurie, A. Theodore
Markettos, Simon W. Moore, Steven J. Murdoch, Kyndylan Nienhuis, Robert
Norton, Alex Richardson, Peter Rugg, Peter Sewell, Stacey Son, and Hongyan
Xia.
Capability Hardware Enhanced RISC Instructions: CHERI
Instruction-Set Architecture (Version 7).
Technical Report UCAM-CL-TR-927, University of Cambridge, Computer
Laboratory, June 2019.
[ bib |
.pdf ]
This technical report describes CHERI ISAv7, the seventh 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 nine years of research, development, experimentation, refinement, formal analysis, and validation through hardware and software implementation. CHERI ISAv7 is a substantial enhancement to prior ISA versions. We differentiate an architecture-neutral protection model vs. architecture-specific instantiations in 64-bit MIPS, 64-bit RISC-V, and x86-64. We have defined a new CHERI Concentrate compression model. CHERI-RISC-V is more substantially elaborated. A new compartment-ID register assists in resisting microarchitectural side-channel attacks. Experimental features include linear capabilities, capability coloring, temporal memory safety, and 64-bit capabilities for 32-bit architectures. |
[7] |
Christopher Pulte, Jean Pichon-Pharabod, Jeehoon Kang, Sung-Hwan Lee, and
Chung-Kil Hur.
Promising-ARM/RISC-V: A simpler and faster operational concurrency
model.
In PLDI 2019: Proceedings of the 40th ACM SIGPLAN
Conference on Programming Language Design and Implementation, June 2019.
[ bib |
DOI |
.pdf ]
For ARMv8 and RISC-V, there are concurrency models in two styles, extensionally equivalent: axiomatic models, expressing the concurrency semantics in terms of global properties of complete executions; and operational models, that compute incrementally. The latter are in an abstract microarchitectural style: they execute each instruction in multiple steps, out-of-order and with explicit branch speculation. This similarity to hardware implementations has been important in developing the models and in establishing confidence, but involves complexity that, for programming and model-checking, one would prefer to avoid. |
[8] |
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.
Technical Report UCAM-CL-TR-932, University of Cambridge, Computer
Laboratory, January 2019.
[ bib |
.pdf ]
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. |
[9] |
Alasdair Armstrong, Thomas Bauereiss, Brian Campbell, Alastair Reid, Kathryn E.
Gray, Robert M. Norton, Prashanth Mundkur, Mark Wassell, Jon French,
Christopher Pulte, Shaked Flur, Ian Stark, Neel Krishnaswami, and Peter
Sewell.
ISA semantics for ARMv8-A, RISC-V, and CHERI-MIPS.
In POPL 2019: Proc. 46th ACM SIGPLAN Symposium on
Principles of Programming Languages, January 2019.
Proc. ACM Program. Lang. 3, POPL, Article 71.
[ bib |
DOI |
.pdf ]
Architecture specifications notionally define the fundamental interface between hardware and software: the envelope of allowed behaviour for processor implementations, and the basic assumptions for software development and verification. But in practice, they are typically prose and pseudocode documents, not rigorous or executable artifacts, leaving software and verification on shaky ground. |
[10] | Andrew Waterman and Krste Asanović, editors. The RISC-V Instruction Set Manual Volume I: Unprivileged ISA. December 2018. Document Version 20181221-Public-Review-draft. Contributors: Arvind, Krste Asanović, Rimas Avižienis, Jacob Bachmeyer, Christopher F. Batten, Allen J. Baum, Alex Bradbury, Scott Beamer, Preston Briggs, Christopher Celio, Chuanhua Chang, David Chisnall, Paul Clayton, Palmer Dabbelt, Roger Espasa, Shaked Flur, Stefan Freudenberger, Jan Gray, Michael Hamburg, John Hauser, David Horner, Bruce Hoult, Alexandre Joannou, Olof Johansson, Ben Keller, Yunsup Lee, Paul Loewenstein, Daniel Lustig, Yatin Manerkar, Luc Maranget, Margaret Martonosi, Joseph Myers, Vijayanand Nagarajan, Rishiyur Nikhil, Jonas Oberhauser, Stefan O'Rear, Albert Ou, John Ousterhout, David Patterson, Christopher Pulte, Jose Renau, Colin Schmidt, Peter Sewell, Susmit Sarkar, Michael Taylor, Wesley Terpstra, Matt Thomas, Tommy Thorn, Caroline Trippel, Ray VanDeWalker, Muralidaran Vijayaraghavan, Megan Wachs, Andrew Waterman, Robert Watson, Derek Williams, Andrew Wright, Reinoud Zandijk, and Sizhuo Zhang. [ bib | .pdf ] |
[11] |
Christopher Pulte, Shaked Flur, Will Deacon, Jon French, Susmit Sarkar, and
Peter Sewell.
Simplifying ARM Concurrency: Multicopy-atomic Axiomatic and
Operational Models for ARMv8.
In POPL 2018, pages 19:1--19:29, January 2018.
[ bib |
DOI |
http |
.pdf ]
ARM has a relaxed memory model, previously specified in informal prose for ARMv7 and ARMv8. Over time, and partly due to work building formal semantics for ARM concurrency, it has become clear that some of the complexity of the model is not justified by the potential benefits. In particular, the model was originally non-multicopy-atomic: writes could become visible to some other threads before becoming visible to all --- but this has not been exploited in production implementations, the corresponding potential hardware optimisations are thought to have insufficient benefits in the ARM context, and it gives rise to subtle complications when combined with other ARMv8 features. The ARMv8 architecture has therefore been revised: it now has a multicopy-atomic model. It has also been simplified in other respects, including more straightforward notions of dependency, and the architecture now includes a formal concurrency model. |
[12] |
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.
In ICCD 2017: IEEE 35th International Conference on
Computer Design, November 2017.
[ bib |
DOI |
www: |
.pdf ]
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 power- ful 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. |
[13] |
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).
Technical Report UCAM-CL-TR-907, University of Cambridge, Computer
Laboratory, April 2017.
[ bib |
.pdf ]
This technical report describes CHERI ISAv6, the sixth 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 seven years of research, development, experimentation, refinement, formal analysis, and validation through hardware and software implementation. CHERI ISAv6 is a substantial enhancement to prior ISA versions: it introduces support for kernel-mode compartmentalization, jump-based rather than exception-based domain transition, architecture-abstracted and efficient tag restoration, and more efficient generated code. A new chapter addresses potential applications of the CHERI model to the RISC-V and x86-64 ISAs, previously described relative only to the 64-bit MIPS ISA. CHERI ISAv6 better explains our design rationale and research methodology. |
[14] |
Shaked Flur, Susmit Sarkar, Christopher Pulte, Kyndylan Nienhuis, Luc Maranget,
Kathryn E. Gray, Ali Sezgin, Mark Batty, and Peter Sewell.
Mixed-size concurrency: ARM, POWER, C/C++11, and SC.
In POPL 2017: The 44st Annual ACM SIGPLAN-SIGACT
Symposium on Principles of Programming Languages, Paris, France, pages
429--442, January 2017.
[ bib |
DOI |
http |
.pdf ]
Previous work on the semantics of relaxed shared-memory concurrency has only considered the case in which each load reads the data of exactly one store. In practice, however, multiprocessors support mixed-size accesses, and these are used by systems software and (to some degree) exposed at the C/C++ language level. A semantic foundation for software, therefore, has to address them. |
[15] |
Brian Campbell and Ian Stark.
Extracting behaviour from an executable instruction set model.
In Ruzica Piskac and Muralidhar Talupur, editors, FMCAD
2016: Formal Methods in Computer-Aided Design, pages 33--40, October 2016.
Full proceedings
http://www.cs.utexas.edu/users/hunt/FMCAD/FMCAD16/proceedings/fmcad-2016-proceedings.pdf.
[ bib |
.pdf ]
Presenting large formal instruction set models as executable functions makes them accessible to engineers and useful for less formal purposes such as simulation. However, it is more difficult to extract information about the behaviour of individual instructions for reasoning. We present a method which combines symbolic evaluation and symbolic execution techniques to provide a rule-based view of instruction behaviour, with particular application to automatic test generation for large MIPS-like models. |
[16] |
Robert N.M. Watson, Robert M. Norton, Jonathan Woodruff, Simon W. Moore,
Peter G. Neumann, Jonathan Anderson, David Chisnall, Brooks Davis, Ben
Laurie, Michael Roe, Nirav H. Dave, Khilan Gudka, Alexandre Joannou,
A. Theodore Markettos, Ed 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):38--49, September 2016.
[ bib |
DOI |
http ]
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. |
[17] |
M. Naylor, S. W. Moore, and A. Mujumdar.
A consistency checker for memory subsystem traces.
In FMCAD 2016: Formal Methods in Computer-Aided
Design, September 2016.
[ bib |
DOI |
.pdf ]
Verifying the memory subsystem in a modern shared-memory multiprocessor is a big challenge. Optimized implementations are highly sophisticated, yet must provide subtle consistency and liveness guarantees for the correct execution of concurrent programs. We present a tool that supports efficient specification-based testing of the memory subsystem against a range of formally specified consistency models. Our tool operates directly on the memory subsystem interface, promoting a compositional approach to system-on-chip verification, and can be used to search for simple failure cases – assisting rapid debug. It has recently been incorporated into the development flows of two open-source implementations -- Berkeley’s Rocket Chip (RISCV) and Cambridge’s BERI (MIPS) -- where it has uncovered a number of serious bugs. |
[18] |
Brian Campbell and Ian Stark.
Randomised testing of a microprocessor model using SMT-solver state
generation.
Sci. Comput. Program., 118:60--76, March 2016.
[ bib |
DOI |
.pdf ]
We validate a HOL4 model of the ARM Cortex-M0 microcontroller core by testing the model’s behaviour on randomly chosen instructions against real chips from several manufacturers. The model and our intended application involve precise timing information about instruction execution, but the implementations are pipelined, so checking the behaviour of single instructions would not give us sufficient confidence in the model. Thus we test the model using sequences of randomly chosen instructions. The main challenge is to meet the constraints on the initial and intermediate execution states: we must ensure that memory accesses are in range and that we respect restrictions on the instructions. By careful transformation of these constraints an off-the-shelf SMT solver can be used to find suitable states for executing test sequences. We also use additional constraints to test our hypotheses about the timing anomalies encountered. |
[19] |
Shaked Flur, Kathryn E. Gray, Christopher Pulte, Susmit Sarkar, Ali Sezgin, Luc
Maranget, Will Deacon, and Peter Sewell.
Modelling the ARMv8 architecture, operationally: concurrency and
ISA.
In POPL 2016: Proceedings of the 43rd Annual ACM
SIGPLAN-SIGACT Symposium on Principles of Programming Languages, St.
Petersburg, FL, USA, pages 608--621, January 2016.
[ bib |
DOI |
http |
.pdf ]
In this paper we develop semantics for key aspects of the ARMv8 multiprocessor architecture: the concurrency model and much of the 64-bit application-level instruction set (ISA). Our goal is to clarify what the range of architecturally allowable behaviour is, and thereby to support future work on formal verification, analysis, and testing of concurrent ARM software and hardware. |
[20] |
Kathryn E. Gray, Gabriel Kerneis, Dominic P. Mulligan, Christopher Pulte,
Susmit Sarkar, and Peter Sewell.
An integrated concurrency and core-ISA architectural envelope
definition, and test oracle, for IBM POWER multiprocessors.
In MICRO 2015: Proceedings of the 48th International
Symposium on Microarchitecture, , Waikiki, HI, USA, pages 635--646, December
2015.
[ bib |
DOI |
http |
.pdf ]
Weakly consistent multiprocessors such as ARM and IBM POWER have been with us for decades, but their subtle programmer-visible concurrency behaviour remains challenging, both to implement and to use; the traditional architecture documentation, with its mix of prose and pseudocode, leaves much unclear. |
[21] |
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.
Technical Report UCAM-CL-TR-877, University of Cambridge, Computer
Laboratory, September 2015.
[ bib |
.pdf ]
The CHERI Programmer'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 Guide is targeted at hardware and software developers working with capability-enhanced software. It describes how to use the CHERI Clang/LLVM compiler suite and CheriBSD operating system -- versions of the off-the-shelf LLVM suite and FreeBSD operating system adapted to use CHERI’s protection features -- as well as implementation details of both. |
[22] |
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.
Technical Report UCAM-CL-TR-876, University of Cambridge, Computer
Laboratory, September 2015.
[ bib |
.pdf ]
This technical report describes CHERI ISAv4, the fourth 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 research, development, refinement, formal analysis, and testing, and is a substantial enhancement to the 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 substantial software stacks to run on prototype hardware. |
[23] |
Matthew Naylor and Simon W. Moore.
A generic synthesisable test bench.
In MEMOCODE 2015: ACM/IEEE International Conference
on Formal Methods and Models for Codesign, Austin, TX, USA, pages 128--137,
September 2015.
[ bib |
DOI |
http |
.pdf ]
Writing test benches is one of the most frequently-performed tasks in the hardware development process. The ability to reuse common test bench features is therefore key to productivity. In this paper, we present a generic test bench, parameterised by a specification of correctness, which can be used to test any design. Our test bench provides several important features, including automatic test-sequence generation and shrinking of counter-examples, and is fully synthesisable, allowing rigorous testing on FPGA as well as in simulation. The approach is easy to use, cheap to implement, and encourages the formal specification of hardware components through the reward of automatic testing and simple failure cases. |
[24] |
Robert N. M. Watson, Jonathan Woodruff, Peter G. Neumann, Simon W. Moore,
Jonathan Anderson, David Chisnall, Nirav Dave, Brooks Davis, Khilan Gudka,
Ben Laurie, Steven J. Murdoch, Robert Norton, Michael Roe, Stacey Son, and
Munraj Vadera.
CHERI: A hybrid capability-system architecture for scalable
software compartmentalization.
In Security and Privacy 2015: Proceedings of the 36th
IEEE Symposium on Security and Privacy (“Oakland”), May 2015.
[ bib |
DOI |
.pdf ]
CHERI extends a conventional RISC Instruction-Set Architecture, compiler, and operating system to support fine-grained, capability-based memory protection to mitigate memory-related vulnerabilities in C-language TCBs. We describe how CHERI capabilities can also underpin a hardware-software object-capability model for application compartmentalization that can mitigate broader classes of attack. Prototyped as an extension to the open-source 64-bit BERI RISC FPGA softcore processor, FreeBSD operating system, and LLVM compiler, we demonstrate multiple orders-of-magnitude improvement in scalability, simplified programmability, and resulting tangible security benefits as compared to compartmentalization based on pure Memory-Management Unit (MMU) designs. We evaluate incrementally deployable CHERI-based compartmentalization using several real-world UNIX libraries and applications. |
[25] |
S. Flur, K. Gray, G. Kerneis, D. Mulligan, C. Pulte, S. Sarkar, and P. Sewell.
Rigorous architectural modelling for production multiprocessors, May
2015.
Presentation at HCSS 2015: the Fifteenth Annual High Confidence
Software and Systems Conference.
[ bib ]
Processor architectures are critical interfaces in computing, but they are typically defined only by prose and pseudocode documentation. This is especially problematic for the subtle concurrency behaviour of weakly consistent multiprocessors such as ARM and IBM POWER: the traditional documentation does not define precisely what programmer-observable behaviour is (and is not) allowed for concurrent code; it is not executable as a test oracle for pre-Silicon or post-Silicon hardware testing; it is not executable as an emulator for software testing; and it is not mathematically rigorous enough to serve as a foundation for software verification. |
[26] |
Jade Alglave, Mark Batty, Alastair F. Donaldson, Ganesh Gopalakrishnan, Jeroen
Ketema, Daniel Poetzl, Tyler Sorensen, and John Wickerson.
GPU concurrency: Weak behaviours and programming assumptions.
In ASPLOS 2015: Proceedings of the Twentieth
International Conference on Architectural Support for Programming Languages
and Operating Systems, Istanbul, Turkey, pages 577--591, March 2015.
[ bib |
DOI |
http ]
Concurrency is pervasive and perplexing, particularly on graphics processing units (GPUs). Current specifications of languages and hardware are inconclusive; thus programmers often rely on folklore assumptions when writing software. |
[27] |
Brian Campbell and Ian Stark.
Randomised testing of a microprocessor model using SMT-solver state
generation.
In Frédéric Lang and Francesco Flammini, editors,
FMICS 2014: Formal Methods for Industrial Critical Systems, volume
8718 of Lecture Notes in Computer Science, pages 185--199. Springer,
September 2014.
[ bib |
DOI |
.pdf ]
We validate a HOL4 model of the ARM Cortex-M0 microcontroller core by testing the model's behaviour on randomly chosen instructions against a real chip. The model and our intended application involve precise timing information about instruction execution, but the implementations are pipelined, so checking the behaviour of single instructions would not give us sufficient confidence in the model. Thus we test the model using sequences of randomly chosen instructions. The main challenge is to meet the constraints on the initial and intermediate execution states: we must ensure that memory accesses are in range and that we respect restrictions on the instructions. By careful transformation of these constraints an off-the-shelf SMT solver can be used to find suitable states for executing test sequences. |
This file was generated by bibtex2html 1.99.