Memory-Safety

• CHERI and Capability Hardware: Memory Safety at the Gate Level · 2025-03-11

  How CHERI Concentrate compression, the load barrier for temporal safety, and the Arm Morello prototype are reshaping what it means to build a secure processor — and why formal verification of capability integrity is the hard part.

• Separation Logic: The Frame Rule, Separating Conjunction, and Concurrent Verification · 2022-01-01

  An exploration of separation logic—O'Hearn and Reynolds's revolutionary extension of Hoare logic for local reasoning about mutable state, the frame rule, and concurrent separation logic.

• Capability-Based Security: CHERI Architecture, Hardware Capabilities, Spatial and Referential Safety, and Compartmentalization · 2021-02-26

  A deep exploration of the CHERI capability architecture — how hardware-enforced capabilities provide spatial memory safety, referential integrity, and fine-grained compartmentalization at the instruction level.