POCL 2024
who it's for
compiler engineers, formal methods engineers, security researchers, systems software engineers, toolchain maintainers, operating system developers, hardware architects
topics
Morello ISA proofs; capability machine calling conventions; capability compression mitigation; CHERI C semantics in Coq; capability-aware LLVM toolchain; CHERI static analysis; ESBMC CHERI verification; capability-tracking memory allocators; compartmentalization runtime trampolines; indirect sentries and seals; Rust on Morello; heap temporal safety
| title | author | length |
|---|---|---|
| The state of Morello and CHERI | Robert N. M. Watson | 42m |
CHERI is now portable across MIPS, RISC‑V and ARM-derived Morello platforms, with vendor efforts from Microsoft Chariot to a commercial CIP IP and about 600… | ||
| The state of Morello software and projects | Konrad Witaszczyk | 14m |
Project scaffolding delivers four package repos (hybrid, CH, Benchmark, CH-debug) and a build run that finishes in up to 102 hours using two builders (ARM64 80… | ||
| The Morello ISA semantics, proof, and test generation | Thomas Bauereiss, Brian Campbell | 16m |
Formal work translates the ~62,000-line ASL Morello spec into a theorem‑prover model, generates Isabelle proofs that check a monotonicity theorem (software… | ||
| Morello Cerise: proving secure encapsulation (work in progress) | Angus Hammond, Ricardo Almeida | 11m |
Formal encapsulation for Morello is approached by combining T-Cherry properties (Isabelle-proven whole-architecture bounds on capability behavior) with the Lis… | ||
| Compartmentalisation models | Dapeng Gao | 23m |
Proposes enforcing least privilege by treating each dynamic library as a compartment and modifying the runtime linker to insert a trampoline for every… | ||
| Proving capability safety in the presence of indirect sentries | Bastien Rousseau, Aina Linn Georges, Dominique Devriese, Jean Pichon-Pharabod, Lars Birkedal | 17m |
Extends a CHERI-style miniature machine (SeRiES) with indirect sentries, adapts an Iris-like program logic plus a new logical relation, and produces… | ||
| Sealed with a Library Call: Memory Allocators Should Track Capability Seal Opera... | Jeremy Singer | 17m |
Claim: memory allocators must track capability seal operations or they break when user code seals pointers. Evidence: ports of the Boehm GC and MicroPython to… | ||
| Secure Calling Conventions for CHERI Capability Machines in Practice (Work in Pr... | Elias Storme, Sander Huyghebaert, Steven Keuchel, Thomas Van Strydonck, Dominique Devriese | 24m |
Implements CHERI calling conventions in LLVM and shows a concrete fix for CHERI’s lossy capability compression: split the stack into an active/reserve stack so… | ||
| Morello software and compilers | Jessica Clarke | 29m |
LLVM based toolchain using Clang LLD and GDB targets Morello with three ABIs pure capability ABI for full CHERI pointers, hybrid ABI for opt‑in compatibility… | ||
| CHERI C semantics | Vadim Zaliva | 19m |
Project produces a mechanized CHERI C semantics implemented in Coq executable semantics and exposes a runnable model (Docker + Compiler Explorer). Memory model… | ||
| CHERI static analysis | Irina Dudina | 23m |
Adds CHERI support to the Clang Static Analyzer and implements four CHERI-aware checkers: a pointer alignment checker, a capability-copy detector, and a… | ||
| ESBMC-CHERI: Towards Verification of C/C++ Programs for CHERI Platforms with ESB... | Franz Brausse, Kunjian Song, Fedor Shmarov, Rafael Menezes, Mikhail R. Gadelha, Konstantin Korovin, Giles Reger, Lucas C. Cordeiro | 20m |
ESBMC is extended to accept CHERI-enabled clang output, translate it to its goto IR, and symbolically execute programs while modeling CHERI intrinsics, tag… | ||
| Rust on Morello | Sarah Harris, Simon Cooksey, Michael Vollmer, Mark Batty | 28m |
A Rust toolchain is ported to Morello prototype hardware, swapping the LLVM backend and making the compiler and core/std build and run; pointer storage is 128… | ||
| Concurrent Mutation must go | Matthew J. Parkinson, Sylvan Clebsch, Tobias Wrigstad, Sophia Drossopoulou, Elias Castegren, Ellen Arvidsson, Luke Cheeseman | 19m |
Argument: concurrent mutation causes the costly read-reclaim race so the simple claim is remove concurrent mutation for temporal safety. Evidence: survey of… | ||
| Object Capabilities | Sophia Drossopoulou, Susan Eisenbach, Julian Mackay, James Noble | 36m |
Claim: object capabilities act as necessary conditions for effects, not just rights, and tracking which objects can reach which capabilities lets one… | ||
| nothing matches | ||