mugshot

Peter Sewell

Professor of Computer Science, Computer Laboratory, University of Cambridge
Member of the Cambridge Programming, Logic, and Semantics Group
Fellow of Wolfson college

Here are my contact details, a photo, short bio, and CV

PhD students, RAs, and Co-authors   Meetings   Funding   Papers (by date)   Papers (by topic)

Teaching

Research

My research aims to put the engineering of real-world computer systems on better foundations, developing techniques (both mathematically rigorous and pragmatically useful) to make systems that are better-understood, more robust, and more secure. This applied semantics needs tightly integrated theoretical and practical research, spanning a range of Computer Science: I work in architectural description, programming languages, networking, and security, developing and using techniques from semantics, type systems, automated reasoning, and concurrency theory.

REMS logo This work currently forms part of the REMS: Rigorous Engineering for Mainstream Systems project, originally funded by the eponymous EPSRC Programme Grant, in collaboration with Systems, Security, Architecture, and Semantics researchers from Cambridge, Imperial, and Edinburgh, and with colleagues in ARM, IBM, and elsewhere, and the EU ERC Advanced Grant ELVER: Engineering with Logic and Verification: Mathematically Rigorous Engineering for Safe and Secure Computer Systems. It is additionally supported by donations from Arm and Google.

The CHERI project, led by Robert Watson, Simon Moore, and myself at Cambridge, and Peter Neumann at SRI International, extends conventional hardware Instruction-Set Architectures (ISAs) with new architectural features to enable fine-grained memory protection and highly scalable software compartmentalization. It is a hardware/software/semantics co-design project, involving architecture design, hardware implementation, system software adaption, and formal semantics and mechanised proof of security properties. In 2019, UKRI announced the Digital Security by Design Challenge, with £70m government and £117m industry funding, including an industrial prototype Arm Morello CHERI-ARM 64-bit CPU, SoC, and board. This aims to evaluate and demonstrate the mass-market industrial feasibility of CHERI. Here are our DSbD page, blog, and CL news article; an Arm blog post on Morello, a UK Government press release, and an article at The Register.

Recent Papers

Research Topics

I also maintain a page of Action Calculi links.

Other

Another photo

[Validate this page.]