Get the latest tech news
Formal CHERI: design-time proof of full-scale architecture security properties (2022)
Memory safety bugs continue to be a major source of security vulnerabilities, with their root causes ingrained in the industry: - the C and C++ systems programming languages that do not enforce memory protection, and the huge legacy codebase written in them that we depend on; - the legacy design choices of hardware that provides only coarse-grain protection mechanisms, based on virtual memory; and - test-and-debug development methods, in which only a tiny fraction of all possible execution paths can be checked, leaving ample unexplored corners for exploitable bugs. Over the last twelve years, the CHERI project has been working on addressing the first two of these problems by extending conventional hardware Instruction-Set Architectures (ISAs) with new architectural features to enable fine-grained memory protection and highly scalable software compartmentalisation, prototyped first as CHERI-MIPS and CHERI-RISC-V architecture designs and FPGA implementations, with an extensive software stack ported to run above them.
The academic experimental results are very promising, but achieving widespread adoption of CHERI needs an industry-scale evaluation of a high-performance silicon processor implementation and software stack. In this blog post, we describe how we used rigorous engineering methods to provide high assurance of key security properties of CHERI architectures, with machine-checked mathematical proof, as well as to complement and support traditional design and development workflows, e.g. by automatically generating test suites. However, stronger properties typically involve specific software idioms, e.g. calling conventions or exception handlers, and their proofs use techniques that have not yet been scaled up to full architectures.
Or read this on Hacker News
