"Secure by Design Principles" are increasingly mandated by government and regulatory bodies globally. However, further guidance is needed across high-integrity industries on what can be considered an acceptable means of compliance with security requirements. This talk will focus on "digital security through verification" and, more specifically, the potential for using CHERI microprocessor architectures as memory-safe verification environments to generate required evidence to argue that a system is secure before deployment. CHERI is a hardware architecture enhancing security, mitigating vulnerabilities, and enabling fine-grained memory protection.

This talk will explain why, even though memory-safe programming languages are essential for high-integrity software, in some scenarios they don't go far enough, and memory-safe hardware, like CHERI, is also necessary for high-assurance security solutions. The talk will explain why CHERI alone is insufficient to provide security through verification and why coupling CHERI with a fuzzer brings a novel approach to vulnerability identification for high-integrity software. More specifically, we will describe research and development undertaken at AdaCore, and through the SCHEME project, to develop a portable smart grey box fuzzing solution, codenamed the "Adaptive" engine, for embedded targets and why the dynamic analysis anomaly detection features of CHERI enhance the fuzzer capabilities even when compared against traditional approaches like memory sanitisers and runtime constraint checks built into some memory-safe programming languages.