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
Ken is an Independent Consultant in South Florida for secure cloud-based software and mobile access software. Graduated in the UK, developed the first Capability-Based Computers (PP-250), became a Charted Engineer, and awarded a Fellowship of the IEE (London). Partnered on a dozen patents developing Object Engineering fundamentals while working in UK, USA, Germany, and Belgium. Invitation speaker at conferences on Operating Systems and Communications.