- Morello-team - lists.cheri-alliance.org

Morello board request - Seung Hoon Park
by dan.sullivan＠cheri-alliance.org 05 Oct '26

05 Oct '26

Dear all, Please find below a new request for a Morello board: ----- I am a PhD student at Imperial College London, supervised by Prof. Philippa Gardner, working in formal verification, specifically on formal foundations for symbolic execution with separation logic specifications. As part of the SCorCH project (https://scorch-project.github.io/), I previously formalised an executable CHERI-C memory model in Isabelle/HOL and used it to test CHERI-C programs (https://link.springer.com/chapter/10.1007/978-3-031-30823-9_28). Building on that work, we have now formalised a symbolic CHERI-C memory model that supports separation logic specifications in Gillian, a OCaml-based compositional symbolic execution framework. We plan to apply it to case studies. We have a basic CHERI-aware memory allocator in mind, where we verify the formal correctness of such memory allocators. We would use the Morello board to validate our model against real CHERI hardware: compiling the case-study programs with the Morello LLVM toolchain, running them in purecap mode, and checking that the observed behaviour (capability faults, bounds and representability behaviour, tag clearing, etc.) matches what our model predicts. QEMU is itself a software model of the architecture, so validating against it cannot rule out misreadings of the specification shared by both models; the hardware implementation is the ground truth we need. Our use is functional validation rather than performance measurement. We expect this work to result in publications. Specifically, we aim to introduce a mechanised, formalised symbolic CHERI-C memory model that is sound with respect to the ground model (i.e. the concrete model). The board would be hosted by Verified Trustworthy Software Specification (VTSS), Department of Computing, Imperial College London, for approximately six months. ------ Please let me know your decision. Kind regards, Dan Sullivan Project & Community Coordinator CHERI Alliance cheri-alliance.org<http://www.cheri-alliance.org/> My working days are Monday to Wednesday

2 1

New request
by Mike Eftimakis 05 Oct '26

05 Oct '26

Dear team, We have a new request from UC Davis: I’m an Assistant Professor in Computer Science at UC Davis working in software security and programming languages. A core focus of my group is the migration of software written in unsafe languages to safe languages. This task includes securing partially migrated code, for example, C/C++ codebases that have been partially migrated to Rust. We have been exploring the selective use of CHERI-based capability hardware to secure unsafe components in a safe codebase. For a Rust codebase, this includes code written in unsafe Rust and C code invoked over foreign function interfaces. We plan to use the Morello board for research on compiler and systems support for securing such "polyglot applications". We would use Morello to prototype capability-aware compiler transformations and runtime mechanisms, evaluate their security and performance overheads on real hardware, and study how CHERI capabilities can strengthen isolation and memory safety in existing software systems. The board would primarily support academic research and student research projects at UC Davis. I had a chat with the guy and they jointly work with Bloomberg research, so there is also additional visibility on this side. What do you think? Thanks! –– Mike Eftimakis – Founding director CHERI Alliance mike.eftimakis(a)cheri-alliance.org <mailto:mike.eftimakis@cheri-alliance.org> Web: cheri-alliance.org <http://cheri-alliance.org/>

2 2

New request
by dan.sullivan＠cheri-alliance.org 15 Sep '26

15 Sep '26

Dear all, Please find below a new request for a Morello board: ----- Hi! I am Adriaan Jacobs (https://adriaanjacobs.github.io/) from the DistriNet research group (KU Leuven) in Ghent, Belgium, working under prof. Stijn Volckaert (https://stijn-volckaert.github.io/personal/). Our research generally focuses on exploit mitigation and compartmentalization, often using "legacy"/"already available" mechanisms rather than a capability-first processor redesign like CHERI. However, over the last few years, we have repeatedly been interested in evaluating CHERI hardware as well. At this moment, we have two ongoing projects that could benefit greatly from physical access to real CHERI hardware: 1. We are developing new "availability"/"software resilience" mechanisms, specifically for CHERI, which focus on minimizing the _power drain_ that denial-of-service attacks can cause for energy-constrained devices (such as pacemakers). For this project, we would like to perform power measurements on a real chip, since estimations in FPGAs and other platforms are not as accurate. 2. In another research line, we have been developing custom processor extensions to mitigate Spectre attacks. These can generally be regarded as a "probabilistic" capability implementation (far less strong than CHERI, but with legacy binary compatibility), and we would like to compare the speculative security guarantees in detail. Morello would by far be the easiest available platform to perform these experiments on, and perhaps also the only realistic option. We are happy to provide additional details about these projects if desired. In the past, we have repeatedly collaborated with Merve Gülmez and Thomas Nymann from Ericsson (CHERI Alliance member), and they put us in touch with Mike Eftemakis, who was kind enough to add myself and Stijn to the CHERI Alliance organization (KUL's participation was organized by Dominique Devriese) and to encourage us to apply for a Morello board. We hope that our motivation suffices to procure one, if there is still enough supply. If so, we can coordinate shipping and conditions on your terms. Kind regards, Adriaan ------ Please let me know your decision. Kind regards, Dan Sullivan Project & Community Coordinator CHERI Alliance cheri-alliance.org<http://www.cheri-alliance.org/> My working days are Monday to Wednesday

2 1

New request
by Mike Eftimakis 08 Sep '26

08 Sep '26

Dear all, Please find below a new request for a Morello board: I would like to request an Arm Morello development board on behalf of the University of Edinburgh. Following discussions with George Neville-Neil regarding our compiler and systems research, we aim to use Morello as a hardware oracle for validating capability-aware memory models and optimising secure memory allocators. Our research focuses on compiler verification, memory safety, and systems efficiency: - Hardware Oracle for MLIR/LLVM Memory Models: We are building differential testing and fuzzing pipelines to validate memory model lowerings within MLIR and LLVM. Morello will serve as the ground-truth hardware oracle to detect subtle miscompilations, spatial/temporal safety violations, and bounds errors. - Capability-Aware Memory Allocation: Building on our prior work optimising memory allocators (GreenMalloc), we are expanding toward low-level OS, heterogeneous, and capability-hardened allocation architectures targeting CHERI. - Further development on previous work on testing system simulators (SearchSys), we are looking to continue our previous work which focused primarily on ArmV8 simulation in the Gem5 system to more niche simulation environments, guided by better and more deep introspection. This aims to further improve the CHERI ecosystem in the following ways: - Toolchain Robustness: Discovering and diagnosing edge cases in CHERI-targeting compiler backends. - Open-Source Artifacts: All fuzzing harnesses, MLIR test suites, and allocator evaluations will be published open-source for the CHERI and LLVM communities. - Disseminating findings through systems/compiler conferences, highlighting the practical security benefits of CHERI hardware. Why Morello Hardware is Essential: - Fuzzing & Execution Scale: Large-scale compiler fuzzing requires millions of iterations. QEMU’s emulation overhead is a prohibitive bottleneck for high-throughput differential testing. - Full 64-Bit Application Scale: Sonata targets 32-bit embedded RISC-V microcontrollers, whereas our MLIR lowerings, compiler optimisations, and allocator workloads target 64-bit, multi-core application processors. - Bare-Metal Concurrency & Microarchitecture: Accurate validation of multi-core memory models, hardware tag propagation, and capability faults requires physical silicon execution rather than idealised emulation. Happy to get your feedback. Thanks and best regards, –– Mike Eftimakis – Founding director CHERI Alliance mike.eftimakis(a)cheri-alliance.org <mailto:mike.eftimakis@cheri-alliance.org> Web: cheri-alliance.org <http://cheri-alliance.org/>

1 1

New request
by Mike Eftimakis 12 Aug '26

12 Aug '26

Dear all, We have a new request for a Morello board: Sensor IT has just been awarded funding by Innovate UK for a project in Advanced Connectivity Solutions. As part of this grant, Sensor IT will implement Open RAN software onto the Morello Board, which includes both porting standard packages (Linux) that may be required as part of the implementation, as well as migrating Open RAN packages such as srsRAN and Open5GS. The team is geographically dispersed, with some of them based in London and others further up north. Even though once we settle on the final architecture one board shared through a VPN line may be enough, if it was possible to have access to another one that will be shipped to our other, north-based, team of resources would make the development much more feasible, hence this request. This is a concrete project. They already have a board, but would like a second one for their other team. Are you happy to support this? Thanks! –– Mike Eftimakis – Founding director CHERI Alliance mike.eftimakis(a)cheri-alliance.org <mailto:mike.eftimakis@cheri-alliance.org> Web: cheri-alliance.org <http://cheri-alliance.org/>

3 3

Another Morello request
by Mike Eftimakis 27 Jul '26

27 Jul '26

Dear all, We’ve received another request… Message: Hi, My name is Po-An Chen, a PhD student at UC Irvine's Secure Systems and Software Laboratory, advised by Prof. Michael Franz. I'm writing on behalf of our lab to request a loan of a Morello board. Over the past two years we've built a working system that recompiles stripped x86-64 binaries directly into genuine pure-capability CHERI binaries, without source, targeting both CHERI-RISC-V and Arm Morello. The prototype runs end-to-end today and is already validated for correctness in QEMU-CHERI simulation, and we're now eagerly trying to move it onto real hardware. What's left is a performance question: how much runtime overhead our recovery approach costs, and how far we can close that gap against code natively compiled for CHERI. The simulator can't answer this. Emulated wall-clock time is dominated by the emulator's own interpretation cost and swings under host load, so cache behavior, memory-hierarchy effects, and actual capability-check latency in silicon are all invisible to it. A physical board is what lets us measure the thing we actually care about. We think this also lines up with the Alliance's own roadmap. The population we are targeting are already-compiled, general-purpose C/C++ software on x86 that predates CHERI and often can't be rebuilt with a modern toolchain. x86 has dominated the server tier for decades, so bringing exactly that installed base of x86 software to CHERI-RISC-V and Morello sits right at the intersection of the trends. A little about us: Prof. Michael Franz is a Distinguished Professor of Computer Science at UC Irvine and director of the Secure Systems and Software Laboratory, with a long record in systems and software security spanning software diversification, secure just-in-time compilation, and binary analysis. Since we target both CHERI-RISC-V and Morello, if your team can also help with a CHERI-RISC-V board, or point us to the right group, we'd be very grateful. We'd welcome staying involved with the CHERI ecosystem beyond this project. Happy to answer any questions or share more detail, and thank you for considering our request. Thank you. Please tell me what you think? Thanks and best regards, –– Mike Eftimakis – Founding director CHERI Alliance mike.eftimakis(a)cheri-alliance.org <mailto:mike.eftimakis@cheri-alliance.org> Web: cheri-alliance.org <http://cheri-alliance.org/>

4 4

Request for a board
by Mike Eftimakis 23 Jul '26

23 Jul '26

Dear all, We have a request from Juniper Network for a Morello board to do some research on CHERI. Are you happy for us to send one? Thanks! –– Mike Eftimakis – Founding director CHERI Alliance mike.eftimakis(a)cheri-alliance.org <mailto:mike.eftimakis@cheri-alliance.org> Web: cheri-alliance.org <http://cheri-alliance.org/>

4 5

New version of the Morelo board?
by Mike Eftimakis 10 Jun '26

10 Jun '26

Dear all, I think I saw a new version of the board: not sure CHERI is included! –– Mike Eftimakis – Founding director CHERI Alliance mike.eftimakis(a)cheri-alliance.org <mailto:mike.eftimakis@cheri-alliance.org> Web: cheri-alliance.org <http://cheri-alliance.org/>

1 0

New request for a Morello board
by Mike Eftimakis 28 May '26

28 May '26

Dear all, We’ve got a request… from someone at Arm! 😁 I guess there must be some boards available internally (maybe accessible remotely to employees?)… Mark, do you know? Thanks! –– Mike Eftimakis – Founding director CHERI Alliance mike.eftimakis(a)cheri-alliance.org <mailto:mike.eftimakis@cheri-alliance.org> Web: cheri-alliance.org <http://cheri-alliance.org/>

2 2

New request
by Mike Eftimakis 18 May '26

18 May '26

Dear all, We have a new request for a Morello board, from a start-up who wants to develop human interfaces for building control - they work on edge devices that collects data and control devices, integrating AI at the edge. They work on a pilot with Raspberry Pi but would want to co-develop on CHERI to make sure that the production would be using CHERI chips. I have sent you a poll invite… Could you please vote whether you agree / disagree on the loan of a Morello board? Thanks! –– Mike Eftimakis – Founding director CHERI Alliance mike.eftimakis(a)cheri-alliance.org <mailto:mike.eftimakis@cheri-alliance.org> Web: cheri-alliance.org <http://cheri-alliance.org/>

1 0

2026

2025

Morello-team

2026

2025

Morello-team ----- 2026 ----- October 2026 September 2026 August 2026 July 2026 June 2026 May 2026 April 2026 March 2026 February 2026 January 2026 ----- 2025 ----- December 2025 November 2025 October 2025

Morello-team