19 citations · 21 across the 5 of their papers we have counts for
5 papers
Griotte: Verified Compartmentalisation via Capabilities
June Rousseau, Aïna Linn Georges, Jean Pichon-Pharabod +1
CHERIoT is a novel hardware-software co-design that leverages hardware capabilities to define a notion of compartment, in a minimalistic capability-based OS, CHERIoT RTOS. By defau…
Escaping the Quicksand: A Call to Arms
Peter Sewell, Jean Pichon-Pharabod
Computing has been an astonishing success - but the accumulated technical debt exposes us all to huge costs in business and societal risk. For 75 years, we've built systems to pros…
Relaxed exception semantics for Arm-A (extended version)
Ben Simner, Alasdair Armstrong, Thomas Bauereiss +4
To manage exceptions, software relies on a key architectural guarantee, precision: that exceptions appear to execute between instructions. However, this definition, dating back ove…
Relaxed virtual memory in Armv8-A (extended version)
Ben Simner, Alasdair Armstrong, Jean Pichon-Pharabod +3
Virtual memory is an essential mechanism for enforcing security boundaries, but its relaxed-memory concurrency semantics has not previously been investigated in detail. The concurr…
Repairing and Mechanising the JavaScript Relaxed Memory Model
Conrad Watt, Christopher Pulte, Anton Podkopaev +5
Modern JavaScript includes the SharedArrayBuffer feature, which provides access to true shared memory concurrency. SharedArrayBuffers are simple linear buffers of bytes, and the Ja…