Thomas Bauereiß

Morello-Cerise: A Proof of Strong Encapsulation for the Arm Morello Capability Hardware Architecture

2025 · Proceedings of the ACM on Programming Languages

When designing new architectural security mechanisms, a key question is whether they actually provide the intended security, but this has historically been very hard to assess. One cannot gain much confidence by testing, as such …