#Memory-Safety
3 posts in tag “Memory-Safety”.
CHERI and Capability Hardware: Memory Safety at the Gate Level
2025-03-11How 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-01An 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-26A 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.