Any views expressed within media held on this service are those of the contributors, should not be taken as approved or endorsed by the University, and do not necessarily reflect the views of the University in respect of any particular issue.

Morello / Edinburgh

Morello / Edinburgh

Digital Security by Design Technology Platform Prototype

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 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

Papers

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.

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.

css.php

Report this page

To report inappropriate content on this page, please use the form below. Upon receiving your report, we will be in touch as per the Take Down Policy of the service.

Please note that personal data collected through this form is used and stored for the purposes of processing this report and communication with you.

If you are unable to report a concern about content via this form please contact the Service Owner.

Please enter an email address you wish to be contacted on. Please describe the unacceptable content in sufficient detail to allow us to locate it, and why you consider it to be unacceptable.
By submitting this report, you accept that it is accurate and that fraudulent or nuisance complaints may result in action by the University.

  Cancel