References:
[1] CHERI ISA v5 (2016).
Existing formal methodology applied to software security has significant problems with multi-address-space security models; formal approaches have relied on the usefullness of addresses(pointers) as unique names for objects. Whereas this weakness in formal methods is a significant problem for traditional CPU designs, which offser security primarily through rings and address-space translation, CHERI’s capability model is scoped within address spaces. This offers the possibility of applying existing software proof methodology in the context of hardware isolation (and other related properties) in a manner that was previously infeasible.
– Formal Methodology, CHERI ISA v5, chapter 1.6.
Q&A Is there any bug that cannot (or hard to) be found without the formal model in the paper? In section VI, subtle bugs are found in CHERI ISA: CLC instruction: load data without permission check; bug in arch document and L3 model. legacy MIPS store allowed writing one byte past the region of the memory the code had permission to, and, if the code had access to the end of the address space, stores could write to the beginning of the address space.
If you could revise
the fundmental principles of
computer system design
to improve security...
... what would you change?