Architecture: That an architectural capability-system model can be successfully atom smashed with a contemporary, MMU-enabled ISA such as Armv8-A. Formal methods: That it is possible to formally model and verify the security of that architecture specification, with machine-checked mathematical proof about its full 60,000 line definition, showing it ensures goals such as malicious code confinement, as well as to automatically generate hardware test suites from the same models. Microarchitecture: That an architectural capability-system model can be implemented in a high-performance, industrial quality multicore superscalar processor implementation, including microarchitecture such as CHERI’s compressed capabilities and a tag controller/cache model. Morello is based on Arm’s widely used Neoverse N1 microarchitecture – very much the “real thing” – and achieves 2.5Ghz, its target clock frequency. Memory-safe C/C++: That it is possible to support memory-safe variants o
Architecture: That an architectural capability-system model can be successfully atom smashed with a contemporary, MMU-enabled ISA such as Armv8-A. Formal methods: That it is possible to formally model and verify the security of that architecture specification, with machine-checked mathematical proof about its full 60,000 line definition, showing it ensures goals such as malicious code confinement, as well as to automatically generate hardware test suites from the same models. Microarchitecture: That an architectural capability-system model can be implemented in a high-performance, industrial quality multicore superscalar processor implementation, including microarchitecture such as CHERI’s compressed capabilities and a tag controller/cache model. Morello is based on Arm’s widely used Neoverse N1 microarchitecture – very much the “real thing” – and achieves 2.5Ghz, its target clock frequency. Memory-safe C/C++: That it is possible to support memory-safe variants o