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)

Open positions

We are looking for postdoctoral researchers and postgraduate research engineers to help develop semantics and verification to improve the foundations and security of mainstream computer systems, for CHERI verification and Arm system software verification. Closing date 30 January 2020 - see the advert.

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, 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 by the EU ERC Advanced Grant ELVER. REMS is exploring how we can use rigorous mathematics to improve engineering practice for mainstream computer systems, to make them more robust and secure. The REMS pages give the associated people, papers, models, and tools.

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.]