Morello
Digital Security by Design Technology Platform Prototype
The Morello processor is a CPU prototype under development by Arm as a more secure hardware architecture for future systems, offering fine-grained memory protection and lightweight compartmentalization. The University of Edinburgh is a research partner in the development of Morello under the UK Digital Security by Design programme, an initiative that aims to radically improve the secure basis of contemporary computing infrastructure.
Central to this programme is the CHERI architecture of Capability Hardware Enhanced RISC Instructions that extends existing processor designs with unforgeable architectural capabilities as tokens of authority. With CHERI, even historically memory-unsafe programming languages like C and C++ can be adapted to provide strong and efficient protection against security vulnerabilities.
The CHERI project follows a hardware/software/semantics co-design approach of rigorous engineering for high-assurance rapid development. As part of this, Edinburgh and Cambridge universities have collaborated on the Sail language for precise specification of instruction set architectures. Given a Sail specification we have automated tools to run simulations, generate test suites, explore concurrency behaviour, and aid machine-checked proof of the corresponding processor hardware and software.
Read this article on the Light Blue Touchpaper security blog for more on the research project and its results.
More Information
- Morello at Arm
- CHERI: Capability Hardware Enhanced RISC Instructions
- CheriBSD and Linux for Morello
- The Sail Specification Language
- REMS: Rigorous Engineering of Mainstream Systems
- DSbD: Digital Security by Design
Morello Hardware Release
Arm Morello: What Is It and Why Is It Important? Arm Blueprint, January 2022.
Arm releases experimental CHERI-enabled Morello board as part of £187M UKRI Digital Security by Design programme. Light Blue Touch Paper, January 2022.
An Armful of CHERIs. Microsoft Security Response Center, January 2022.
Morello research program hits major milestone with hardware now available for testing. Arm Newsroom, January 2020.
People
Software
- coq-cheri-capabilities
- Coq library providing a general specification of CHERI capabilities and a concrete instantiation for Arm Morello.
- CHERI CSA
- Static analyser to support transitioning C/C++ code to CHERI hardware.
Papers
Static Analysis for Transitioning to C/C++. Irina Dudina and Ian Stark. In SOAP 2024: Proceedings of the 13th ACM SIGPLAN International Workshop on the State Of the Art in Program Analysis, pages 52–59. June 2024. DOI https://doi.org/10.1145/3652588.3663323.
Formal Mechanised Semantics of CHERI C: Capabilities, Undefined Behaviour, and Provenance. Vadim Zaliva, Kayvan Memarian, Ricardo Almeida, Jessica Clarke, Brooks Davis, Alexander Richardson, David Chisnall, Brian Campbell, Ian Stark, Robert N. M. Watson, and Peter Sewell. In ASPLOS ’24: Proceedings of the 29th ACM International Conference on Architectural Support for Programming Languages and Operating Systems, volume 1, pages 181–196. April 2024. DOI https://doi.org/10.1145/3617232.3624859.
Verified Security for the Morello Capability-enhanced Prototype Arm Architecture. Thomas Bauereiss, Brian Campbell, Thomas Sewell, Alasdair Armstrong, Lawrence Esswood, Ian Stark, Graeme Barnes, Robert N. M. Watson, and Peter Sewell. In Programming Languages and Systems: Proceedings of the 31st European Symposium on Programming ESOP 2022. Lecture Notes in Computer Science 13240, pages 174–203. April 2022. DOI https://doi.org/10.1007/978-3-030-99336-8_7.
Isla: Integrating Full-Scale ISA Semantics and Axiomatic Concurrency Models. Alasdair Armstrong, Brian Campbell, Ben Simner, Christopher Pulte, and Peter Sewell. In Computer Aided Verification: Proceedings of the 33rd International Conference CAV 2021. Lecture Notes in Computer Science 12759, pages 303–316. July 2021. DOI https://doi.org/10.1007/978-3-030-81685-8_14.
Rigorous Engineering for Hardware Security: Formal Modelling and Proof in the CHERI Design and Implementation Process. 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. In Security and Privacy: Proceedings of the 2020 IEEE Symposium SP 2020, pages 1003–1020. May 2020. DOI https://doi.org/10.1109/SP40000.2020.00055.
ISA Semantics for ARMv8-A, RISC-V, and CHERI-MIPS. 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. Proceedings of the ACM on Programming Languages 3, POPL, Article 71, 31 pages. January 2019. DOI https://doi.org/10.1145/3290384.
Related Projects
REMS: Rigorous Engineering of Mainstream Systems. EPSRC-funded research collaboration between Edinburgh, Cambridge, and Imperial, 2013–2020. The Sail language was developed as part of REMS and rigorous engineering is key to the CHERI hardware/software/semantics co-design.
Security, Privacy and Trust. Research group in the School of Informatics.
Edinburgh Cyber Security, Privacy and Trust Institute. Brings together researchers from computer science, law, engineering, health, politics, and sociology.
