• Formal Mechanised Semantics of CHERI C: Capabilities, Provenance, and Undefined Behaviour. Vadim Zaliva, Kayvan Memarian, Ricardo Almeida, Jessica Clarke, Brooks Davis, Alex Richardson, David Chisnall, Brian Campbell, Ian Stark, Robert N. M. Watson, and Peter Sewell. In ASPLOS 2024. [ bib | pdf | abstract ]
• The Arm Morello Evaluation Platform---Validating CHERI-Based Security in a High-Performance System. Richard Grisenthwaite, Graeme Barnes, Robert N. M. Watson, Simon W. Moore, Peter Sewell, and Jonathan Woodruff. IEEE Micro, 43(3):50--57, 2023. [ bib | doi | http | abstract ]
• Improving Security with Hardware Support: CHERI and Arm's Morello. Robert N. M. Watson, Peter Sewell, and William Martin. The Next Wave (The National Security Agency's review of emerging technologies), 4(1):10--21, 2023. ISSN 2640-1789 (print), ISSN 2640-1797 (online). [ bib | project page | pdf | abstract ]
• Formal CHERI: rigorous engineering and design-time proof of full-scale architecture security properties, Peter Sewell, Thomas Bauereiss, Brian Campbell, and Robert N. M. Watson. Blog post, https://www.lightbluetouchpaper.org/2022/07/22/formal-cheri/, July 2022. [ bib | project page | http ]
• Verified Security for the Morello Capability-enhanced Prototype Arm Architecture. Thomas Bauereiss, Brian Campbell, Thomas Sewell, Alasdair Armstrong, Lawrence Esswood, Ian Stark, Graeme Barnes, Robert N. M. Watson, and Peter Sewell. In ESOP 2022. [ bib | doi | project page | pdf | http | abstract ]
• CHERI C/C++ Programming Guide. Robert N. M. Watson, Alexander Richardson, Brooks Davis, John Baldwin, David Chisnall, Jessica Clarke, Nathaniel Filardo, Simon W. Moore, Edward Napierala, Peter Sewell, and Peter G. Neumann. Technical Report UCAM-CL-TR-947, University of Cambridge, Computer Laboratory, June 2020. [ bib | project page | pdf | abstract ]
• Rigorous engineering for hardware security: Formal modelling and proof in the CHERI design and implementation process. 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. In Security and Privacy 2020. [ bib | doi | project page | pdf | abstract ]
• An Introduction to CHERI. Robert N. M. Watson, Simon W. Moore, Peter Sewell, and Peter Neumann. Technical Report UCAM-CL-TR-941, University of Cambridge, Computer Laboratory, September 2019. [ bib | project page | pdf | abstract ]
• Rigorous engineering for hardware security: Formal modelling and proof in the CHERI design and implementation process. Kyndylan Nienhuis, Alexandre Joannou, Anthony Fox, Michael Roe, Thomas Bauereiss, Brian Campbell, Matthew Naylor, Robert M. Norton, Simon W. Moore, Peter G. Neumann, Ian Stark, Robert N. M. Watson, and Peter Sewell. Technical Report UCAM-CL-TR-940, University of Cambridge, Computer Laboratory, September 2019. [ bib | pdf | abstract ]
• Capability Hardware Enhanced RISC Instructions: CHERI Instruction-Set Architecture (Version 7). Robert N. M. Watson, Peter G. Neumann, Jonathan Woodruff, Michael Roe, Hesham Almatary, Jonathan Anderson, John Baldwin, David Chisnall, Brooks Davis, Nathaniel Wesley Filardo, Alexandre Joannou, Ben Laurie, A. Theodore Markettos, Simon W. Moore, Steven J. Murdoch, Kyndylan Nienhuis, Robert Norton, Alex Richardson, Peter Rugg, Peter Sewell, Stacey Son, and Hongyan Xia. Technical Report UCAM-CL-TR-927, University of Cambridge, Computer Laboratory, June 2019. 496pp. [ bib | pdf | abstract ]
• CheriABI: Enforcing Valid Pointer Provenance and Minimizing Pointer Privilege in the POSIX C Run-time Environment. Brooks Davis, Robert N. M. Watson, Alexander Richardson, Peter G. Neumann, Simon W. Moore, John Baldwin, David Chisnall, James Clarke, Nathaniel Wesley Filardo, Khilan Gudka, Alexandre Joannou, Ben Laurie, A. Theodore Markettos, J. Edward Maste, Alfredo Mazzinghi, Edward Tomasz Napierala, Robert M. Norton, Michael Roe, Peter Sewell, Stacey Son, and Jonathan Woodruff. In ASPLOS 2019, Best paper award. [ bib | doi | project page | pdf | http | abstract ]
• CHERI Concentrate: Practical Compressed Capabilities. Jonathan Woodruff, Alexandre Joannou, Hongyan Xia, Anthony Fox, Robert Norton, Thomas Bauereiss, David Chisnall, Brooks Davis, Khilan Gudka, Nathaniel W. Filardo, A. Theodore Markettos, Michael Roe, Peter G. Neumann, Robert N. M. Watson, and Simon W. Moore. IEEE Transactions on Computers, 2019. [ bib | doi | pdf | abstract ]
• CheriABI: Enforcing valid pointer provenance and minimizing pointer privilege in the POSIX C run-time environment. Brooks Davis, Robert N. M. Watson, Alexander Richardson, Peter G. Neumann, Simon W. Moore, John Baldwin, David Chisnall, James Clarke, Nathaniel Wesley Filardo, Khilan Gudka, Alexandre Joannou, Ben Laurie, A. Theodore Markettos, J. Edward Maste, Alfredo Mazzinghi, Edward Tomasz Napierala, Robert M. Norton, Michael Roe, Peter Sewell, Stacey Son, and Jonathan Woodruff. Technical Report UCAM-CL-TR-932, University of Cambridge, Computer Laboratory, January 2019. [ bib | project page | pdf | abstract ]
• Through computer architecture, darkly. A. Theodore Markettos, Robert N. M. Watson, Simon W. Moore, Peter Sewell, and Peter G. Neumann. Commun. ACM, 62(6):25--27, 2019. [ bib | doi | http ]
• ISA Semantics for ARMv8-A, RISC-V, and CHERI-MIPS. Alasdair Armstrong, Thomas Bauereiss, Brian Campbell, Alastair Reid, Kathryn E. Gray, Robert M. Norton, Prashanth Mundkur, Mark Wassell, Jon French, Christopher Pulte, Shaked Flur, Ian Stark, Neel Krishnaswami, and Peter Sewell. In POPL 2019, Proc. ACM Program. Lang. 3, POPL, Article 71. [ bib | doi | supplementary material | project page | pdf | abstract ]
• Exploring C Semantics and Pointer Provenance. Kayvan Memarian, Victor B. F. Gomes, Brooks Davis, Stephen Kell, Alexander Richardson, Robert N. M. Watson, and Peter Sewell. In POPL 2019, Proc. ACM Program. Lang. 3, POPL, Article 67. Also available as ISO/IEC JTC1/SC22/WG14 N2311. [ bib | doi | supplementary material | project page | pdf | abstract ]
• Detailed Models of Instruction Set Architectures: From Pseudocode to Formal Semantics. Alasdair Armstrong, Thomas Bauereiss, Brian Campbell, Shaked Flur, Kathryn E. Gray, Prashanth Mundkur, Robert M. Norton, Christopher Pulte, Alastair Reid, Peter Sewell, Ian Stark, and Mark Wassell. In Automated Reasoning Workshop (ARW) 2018, Two-page abstract. [ bib | project page | pdf | abstract ]
• Extracting Behaviour from an Executable Instruction Set Model. Brian Campbell and Ian Stark. In FMCAD 2016, Full proceedings http://www.cs.utexas.edu/users/hunt/FMCAD/FMCAD16/proceedings/fmcad-2016-proceedings.pdf. [ bib | pdf | abstract ]
• Into the depths of C: elaborating the de facto standards. Kayvan Memarian, Justus Matthiesen, James Lingard, Kyndylan Nienhuis, David Chisnall, Robert N.M. Watson, and Peter Sewell. In PLDI 2016, PLDI 2016 Distinguished Paper award. [ bib | doi | project page | pdf | http | abstract ]