Demonstration venue · read-only. Every page can be browsed; the buttons that would change it are switched off. Create an account to run TaxoReview on your own data. A simulation from public publication records: the people listed were not invited and did not agree to review.
? Tutorial for this page

Alex Richardson 0001

dblp:75/10952-1 · also Alexander Richardson 0001 · DBLP profile ↗
← Back
11ranked-venue papers
0as first author
2since 2021 · last 2024
0000-0002-6372-217XORCID · verified

Domains — the database's venue-derived domains; a paper can count in several

Systems, architecture and hardware · 7 · 2 since 2021Software engineering, systems software and programming languages · 4 · 1 since 2021Security and privacy · 2

Expertise — from the expertise taxonomy: the topics of the expert's papers under the CCF categories. A weight counts papers with recency: 1 for a paper about the topic, 0.3 when the topic is its context, halved every five years.

Network and information security
7 papers
Systems and software security · 100%
Software engineering, system software, and programming languages
5 papers
Programming languages and type systems · 66% Operating systems · 20% Concurrent programming · 13%
Computer architecture, parallel and distributed computing, and storage systems
1 paper
Memory systems · 87% Storage systems · 13%

Topics — the 12 heaviest of 14, each with the papers that count most for it

TopicWeightPapersLastEvidence papers
Systems and software security
memory safety
1.642024
Formal Mechanised Semantics of CHERI C: Capabilities, Undefined Behaviour, and Provenance · ASPLOS (1) 2024
CHERIvoke: Characterising Pointer Revocation using CHERI Capabilities for Temporal Memory Safety · MICRO 2019
CheriABI: Enforcing Valid Pointer Provenance and Minimizing Pointer Privilege in the POSIX C Run-time Environment · ASPLOS 2019
Systems and software security › memory safety
temporal memory safety
0.822020
Cornucopia: Temporal Safety for CHERI Heaps · SP 2020
CHERIvoke: Characterising Pointer Revocation using CHERI Capabilities for Temporal Memory Safety · MICRO 2019
Systems and software security › memory safety › memory corruption defense
use-after-free prevention
0.822020
Cornucopia: Temporal Safety for CHERI Heaps · SP 2020
CHERIvoke: Characterising Pointer Revocation using CHERI Capabilities for Temporal Memory Safety · MICRO 2019
Programming languages and type systems › language semantics
formal semantics
0.812024
Formal Mechanised Semantics of CHERI C: Capabilities, Undefined Behaviour, and Provenance · ASPLOS (1) 2024
Programming languages and type systems › language semantics › formal semantics
mechanized semantics
0.812024
Formal Mechanised Semantics of CHERI C: Capabilities, Undefined Behaviour, and Provenance · ASPLOS (1) 2024
Programming languages and type systems › language semantics
c semantics
0.412019
Exploring C semantics and pointer provenance · Proc. ACM Program. Lang. 2019
Concurrent programming
memory models
0.412019
Exploring C semantics and pointer provenance · Proc. ACM Program. Lang. 2019
Operating systems › resource management › memory management
memory protection
0.412019
CheriABI: Enforcing Valid Pointer Provenance and Minimizing Pointer Privilege in the POSIX C Run-time Environment · ASPLOS 2019
Memory systems
non-volatile memory
0.412019
Memory-Side Protection With a Capability Enforcement Co-Processor · ACM Trans. Archit. Code Optim. 2019
Memory systems › non-volatile memory › persistent memory
secure persistent memory
0.412019
Memory-Side Protection With a Capability Enforcement Co-Processor · ACM Trans. Archit. Code Optim. 2019
Operating systems › resource management › memory management
virtual memory
0.112020
Cornucopia: Temporal Safety for CHERI Heaps · SP 2020
Storage systems
storage reliability
0.112019
Memory-Side Protection With a Capability Enforcement Co-Processor · ACM Trans. Archit. Code Optim. 2019

Methods — techniques the papers use, named apart from their topics

CHERI capabilities · 1.9formal mechanisation · 1.5concurrent kernel-resident revocation · 0.9capability revocation · 0.9runtime instrumentation · 0.8memory controller design · 0.8dynamic linking · 0.8cerberus semantics · 0.8capability model · 0.8capability architecture · 0.8test oracle · 0.4LLVM · 0.2
YearPublicationVenuePosition
2024 Formal Mechanised Semantics of CHERI C: Capabilities, Undefined Behaviour, and Provenance
abstract
Memory safety issues are a persistent source of security vulnerabilities, with conventional architectures and the C codebase chronically prone to exploitable errors. The CHERI research project has shown how one can provide radically improved security for that existing codebase with minimal modification, using unforgeable hardware capabilities in place of machine-word pointers in CHERI dialects of C, implemented as adaptions of Clang/LLVM and GCC. CHERI was first prototyped as extensions of MIPS and RISC-V; it is currently being evaluated by Arm and others with the Arm Morello experimental architecture, processor, and platform, to explore its potential for mass-market adoption, and by Microsoft in their CHERIoT design for embedded cores.
Vadim Zaliva, Kayvan Memarian, Ricardo Almeida 0003, Jessica Clarke 0001, Brooks Davis, Alex Richardson 0001, David Chisnall, Brian Campbell 0001, Ian Stark, Robert N. M. Watson, Peter Sewell
ASPLOS (1)6
2023 Architectural Contracts for Safe Speculation
abstract
We propose architectural contracts that specify the allowable limits of speculative execution to enable both software safety guarantees and hardware verification. Transient-execution attacks have presented a major threat in recent years, driving deployment of software mitigations and research into hardware solutions. Recent work on hardware/software contracts for secure speculation recognizes the need for cooperation between hardware guarantees and software analysis, and demonstrates that speculative execution models can enable formal analysis of programs with respect to transient-execution vulnerabilities. Therefore, we have extended these limited models into comprehensive architecture-level contracts that can be verified at a microarchitecture level. We define a set of speculation contracts for translation (TSC) and branching (BSC), and for memory ordering (MOSC). We also develop a set of directed-random test routines that reproduce all known contract violations in a prototype out-of-order processor, most of which represent known transient-execution vulnerabilities. We also extend the RiscyOO processor to enforce each contract and evaluate performance, demonstrating the practicality of the chosen contracts with an overhead between -1.2% and +1.8% for this prototype. These general-purpose contracts set the stage for specification of speculative execution for complete instruction-set architectures, and particularly for new security-focused ISA extensions.
Franz A. Fuchs, Jonathan Woodruff, Peter Rugg, Marno van der Maas, Alexandre Joannou, Alex Richardson 0001, Jessica Clarke 0001, Nathaniel Wesley Filardo, Brooks Davis, John Baldwin, Peter G. Neumann, Simon W. Moore, Robert N. M. Watson
ICCD6
2020 Cornucopia: Temporal Safety for CHERI Heaps
abstract
Use-after-free violations of temporal memory safety continue to plague software systems, underpinning many high-impact exploits. The CHERI capability system shows great promise in achieving C and C++ language spatial memory safety, preventing out-of-bounds accesses. Enforcing language-level temporal safety on CHERI requires capability revocation, traditionally achieved either via table lookups (avoided for performance in the CHERI design) or by identifying capabilities in memory to revoke them (similar to a garbage-collector sweep). CHERIvoke, a prior feasibility study, suggested that CHERI's tagged capabilities could make this latter strategy viable, but modeled only architectural limits and did not consider the full implementation or evaluation of the approach.Cornucopia is a lightweight capability revocation system for CHERI that implements non-probabilistic C/C++ temporal memory safety for standard heap allocations. It extends the CheriBSD virtual-memory subsystem to track capability flow through memory and provides a concurrent kernel-resident revocation service that is amenable to multi-processor and hardware acceleration. We demonstrate an average overhead of less than 2% and a worst-case of 8.9% for concurrent revocation on compatible SPEC CPU2006 benchmarks on a multi-core CHERI CPU on FPGA, and we validate Cornucopia against the Juliet test suite's corpus of temporally unsafe programs. We test its compatibility with a large corpus of C programs by using a revoking allocator as the system allocator while booting multi-user CheriBSD. Cornucopia is a viable strategy for always-on temporal heap memory safety, suitable for production environments.
Nathaniel Wesley Filardo, Brett F. Gutstein, Jonathan Woodruff, Sam Ainsworth 0001, Lucian Paul-Trifu, Brooks Davis, Hongyan Xia, Edward Napierala, Alex Richardson 0001, John Baldwin, David Chisnall, Jessica Clarke 0001, Khilan Gudka, Alexandre Joannou, A. Theodore Markettos, Alfredo Mazzinghi, Robert M. Norton, Michael Roe, Peter Sewell, Stacey D. Son, Timothy M. Jones 0001, Simon W. Moore, Peter G. Neumann, Robert N. M. Watson
SP9
2019 CheriABI: Enforcing Valid Pointer Provenance and Minimizing Pointer Privilege in the POSIX C Run-time Environment
abstract
The CHERI architecture allows pointers to be implemented as capabilities (rather than integer virtual addresses) in a manner that is compatible with, and strengthens, the semantics of the C language. In addition to the spatial protections offered by conventional fat pointers, CHERI capabilities offer strong integrity, enforced provenance validity, and access monotonicity. The stronger guarantees of these architectural capabilities must be reconciled with the real-world behavior of operating systems, run-time environments, and applications. When the process model, user-kernel interactions, dynamic linking, and memory management are all considered, we observe that simple derivation of architectural capabilities is insufficient to describe appropriate access to memory. We bridge this conceptual gap with a notional abstract capability that describes the accesses that should be allowed at a given point in execution, whether in the kernel or userspace. To investigate this notion at scale, we describe the first adaptation of a full C-language operating system (FreeBSD) with an enterprise database (PostgreSQL) for complete spatial and referential memory safety. We show that awareness of abstract capabilities, coupled with CHERI architectural capabilities, can provide more complete protection, strong compatibility, and acceptable performance overhead compared with the pre-CHERI baseline and software-only approaches. Our observations also have potentially significant implications for other mitigation techniques.
Brooks Davis, Robert N. M. Watson, Alex Richardson 0001, Peter G. Neumann, Simon W. Moore, John Baldwin, David Chisnall, Jessica Clarke 0001, Nathaniel Wesley Filardo, Khilan Gudka, Alexandre Joannou, Ben Laurie, A. Theodore Markettos, Ed Maste, Alfredo Mazzinghi, Edward Napierala, Robert M. Norton, Michael Roe, Peter Sewell, Stacey D. Son, Jonathan Woodruff
ASPLOS3
2019 CHERIvoke: Characterising Pointer Revocation using CHERI Capabilities for Temporal Memory Safety
abstract
A lack of temporal safety in low-level languages has led to an epidemic of use-after-free exploits. These have surpassed in number and severity even the infamous buffer-overflow exploits violating spatial safety. Capability addressing can directly enforce spatial safety for the C language by enforcing bounds on pointers and by rendering pointers unforgeable. Nevertheless, an efficient solution for strong temporal memory safety remains elusive.
Hongyan Xia, Jonathan Woodruff, Sam Ainsworth 0001, Nathaniel Wesley Filardo, Michael Roe, Alex Richardson 0001, Peter Rugg, Peter G. Neumann, Simon W. Moore, Robert N. M. Watson, Timothy M. Jones 0001
MICRO6
2019 Exploring C semantics and pointer provenance
abstract
The semantics of pointers and memory objects in C has been a vexed question for many years. C values cannot be treated as either purely abstract or purely concrete entities: the language exposes their representations, but compiler optimisations rely on analyses that reason about provenance and initialisation status, not just runtime representations. The ISO WG14 standard leaves much of this unclear, and in some respects differs with de facto standard usage --- which itself is difficult to investigate. In this paper we explore the possible source-language semantics for memory objects and pointers, in ISO C and in C as it is used and implemented in practice, focussing especially on pointer provenance. We aim to, as far as possible, reconcile the ISO C standard, mainstream compiler behaviour, and the semantics relied on by the corpus of existing C code. We present two coherent proposals, tracking provenance via integers and not; both address many design questions. We highlight some pros and cons and open questions, and illustrate the discussion with a library of test cases. We make our semantics executable as a test oracle, integrating it with the Cerberus semantics for much of the rest of C, which we have made substantially more complete and robust, and equipped with a web-interface GUI. This allows us to experimentally assess our proposals on those test cases. To assess their viability with respect to larger bodies of C code, we analyse the changes required and the resulting behaviour for a port of FreeBSD to CHERI, a research architecture supporting hardware capabilities, which (roughly speaking) traps on the memory safety violations which our proposals deem undefined behaviour. We also develop a new runtime instrumentation tool to detect possible provenance violations in normal C code, and apply it to some of the SPEC benchmarks. We compare our proposal with a source-language variant of the twin-allocation LLVM semantics proposal of Lee et al. Finally, we describe ongoing interactions with WG14, exploring how our proposals could be incorporated into the ISO standard.
Kayvan Memarian, Victor B. F. Gomes, Brooks Davis, Stephen Kell, Alex Richardson 0001, Robert N. M. Watson, Peter Sewell
Proc. ACM Program. Lang.5
2019 Memory-Side Protection With a Capability Enforcement Co-Processor
abstract
Byte-addressable nonvolatile memory (NVM) blends the concepts of storage and memory and can radically improve data-centric applications, from in-memory databases to graph processing. By enabling large-capacity devices to be shared across multiple computing elements, fabric-attached NVM changes the nature of rack-scale systems and enables short-latency direct memory access while retaining data persistence properties and simplifying the software stack. An adequate protection scheme is paramount when addressing shared and persistent memory, but mechanisms that rely on virtual memory paging suffer from the tension between performance (pushing toward large pages) and protection granularity (pushing toward small pages). To address this tension, capabilities are worth revisiting as a more powerful protection mechanism, but the long time needed to introduce new CPU features hampers the adoption of schemes that rely on instruction-set architecture support. This article proposes the Capability Enforcement Co-Processor (CEP), a programmable memory controller that implements fine-grain protection through the capability model without requiring instruction-set support in the application CPU. CEP decouples capabilities from the application CPU instruction-set architecture, shortens time to adoption, and can rapidly evolve to embrace new persistent memory technologies, from NVDIMMs to native NVM devices, either locally connected or fabric attached in rack-scale configurations. CEP exposes an application interface based on memory handles that get internally converted to extended-pointer capabilities. This article presents a proof of concept implementation of a distributed object store (Redis) with CEP. It also demonstrates a capability-enhanced file system (FUSE) implementation using CEP. Our proof of concept shows that CEP provides fine-grain protection while enabling direct memory access from application clients to the NVM, and that by doing so opens up important performance optimization opportunities (up to 4× reduction in latency in comparison to software-based security enforcement) without compromising security. Finally, we also sketch how a future hybrid model could improve the initial implementation by delegating some CEP functionality to a CHERI-enabled processor.
Leonid Azriel, Lukas Humbel, Reto Achermann, Alex Richardson 0001, Moritz Hoffmann 0001, Avi Mendelson, Timothy Roscoe, Robert N. M. Watson, Paolo Faraboschi, Dejan S. Milojicic
ACM Trans. Archit. Code Optim.4
2018 CheriRTOS: A Capability Model for Embedded Devices
abstract
Embedded systems are deployed ubiquitously among various sectors including automotive, medical, robotics and avionics. As these devices become increasingly connected, the attack surface also increases tremendously; new mechanisms must be deployed to defend against more sophisticated attacks while not violating resource constraints. In this paper we present CheriRTOS on CHERI-64, a hardware-software platform atop Capability Hardware Enhanced RISC Instructions (CHERI) for embedded systems. Our system provides efficient and scalable task isolation, fast and secure inter-task communication, fine-grained memory safety, and real-time guarantees, using hardware capabilities as the sole protection mechanism. We summarize state-of-the-art security and memory safety for embedded systems for comparison with our platform, illustrating the superior substrate provided by CHERI's capabilities. Finally, our evaluations show that a capability system can be implemented within the constraints of embedded systems.
Hongyan Xia, Jonathan Woodruff, Hadrien Barral, Lawrence Esswood, Alexandre Joannou, Robert Kovacsics, David Chisnall, Michael Roe, Brooks Davis, Edward Napierala, John Baldwin, Khilan Gudka, Peter G. Neumann, Alex Richardson 0001, Simon W. Moore, Robert N. M. Watson
ICCD14
2017 Separating Translation from Protection in Address Spaces with Dynamic Remapping
abstract
It is time to reconsider memory protection. The emergence of large non-volatile main memories, scalable interconnects, and rack-scale computers running large numbers of small "micro services" creates significant challenges for memory protection based solely on MMU mechanisms. Central to this is a tension between protection and translation: optimizing for translation performance often comes with a cost in protection flexibility.
Reto Achermann, Chris I. Dalton, Paolo Faraboschi, Moritz Hoffmann 0001, Dejan S. Milojicic, Geoffrey Ndu, Alex Richardson 0001, Timothy Roscoe, Adrian L. Shaw, Robert N. M. Watson
HotOS7
2017 Efficient Tagged Memory
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.
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 0001, Stacey D. Son, A. Theodore Markettos
ICCD16
2015 Clean Application Compartmentalization with SOAAP
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.
Khilan Gudka, Robert N. M. Watson, Jonathan Anderson, David Chisnall, Brooks Davis, Ben Laurie, Ilias Marinos, Peter G. Neumann, Alex Richardson 0001
CCS9