Peter Sewell’s research aims to enable rigorous semantics-based engineering of mainstream systems, including real-world and CHERI.

Speaker

Professor Peter Sewell (University of Cambridge)

Agenda

17:30 - Event opens
18:00 - Talk by Professor Peter Sewell
19:00 - 19:30 - Tea/coffee/biscuits
20:00 - End of event

Synopsis

Despite 80+ years of research on semantics and verification, mainstream computer systems and their engineering development processes remain almost entirely non-formal, reliant on ad hoc testing and prose specifications. These have been good enough for industry to thrive, but their inability to exclude errors is one of the root causes of today's endemic security failures.

In this talk I will discuss what it takes to put mathematically rigorous semantics to work for full-scale mainstream systems, touching on scientific, engineering, and social aspects, and on the benefits and costs. This will draw on work with many colleagues on various key interfaces: processor architectures, programming languages, and network protocols; and on the CHERI and Morello projects, extending conventional architectures and languages with hardware support for capabilities, for fine-grained memory protection and encapsulation.

Taking mainstream engineering artefacts seriously also prompts new theory and tools, e.g., for the relaxed shared-memory concurrency semantics of real machines, quite different from traditional concurrency semantics, and for the semantics of C and of CHERI capabilities.

About the speaker

Peter Sewell is a Professor of Computer Science at the University of Cambridge. His research aims to enable rigorous semantics-based engineering of mainstream systems, including real-world concurrency semantics, instruction-set semantics, and CHERI. His PhD was with Robin Milner in Edinburgh. He has held ERC AdG, EPSRC, and Royal Society research fellowships. With Watson, Moore, and Arm, he was one of the instigators of the UKRI Digital Security by Design programme, supporting development of the Arm Morello prototype CHERI Armv8-A architecture, processor, software, and semantics.

Our events are for adults aged 16 years and over.

This event is brought to you by: BCS FACS specialist group in association with London Mathematical Society (LMS)

LMS/FACS talk: Underpinning mainstream engineering (mathematical semantics)
Date and time
Thursday 18 November, 6:00pm - 7:00pm
Location
De Morgan House
57-58 Russell Square
London
WC1B 4HS
United Kingdom
Price
This event is sold out