Rigorous Engineering for Hardware Security: Formal Modelling and Proof in the CHERI Design and Implementation Process

Describes the formal models and proof work used alongside CHERI architecture and hardware development.

Authors

Kyndylan NienhuisAlexandre JoannouThomas BauereissAnthony FoxMichael RoeBrian CampbellMatthew NaylorRobert M. NortonSimon MoorePeter G. NeumannIan StarkRobert WatsonPeter Sewell

Citation

Kyndylan Nienhuis, Alexandre Joannou, Thomas Bauereiss, Anthony Fox, Michael Roe, Brian Campbell, Matthew Naylor, Robert M. Norton, Simon W. Moore, Peter G. Neumann, Ian Stark, Robert N. M. Watson, and Peter Sewell. IEEE Symposium on Security and Privacy 2020, 2020.