Wrestling with real systems

Add to your list(s) Download to your calendar using vCal

• Peter Sewell (University of Cambridge)
• Thursday 07 July 2022, 13:30-14:30
• Seminar Room 1, Newton Institute.

If you have a question about this talk, please contact nobody.

VS2W01 - Vistas in Verified Software

Systems software is often security critical, so a tempting target for verification, but verification needs a trustworthy semantics for the underlying architecture, and verification techniques that can handle it. Neither exist yet, for any major production architecture, so previous work has had to idealise, simplify, or pretend – but we’re getting closer.  In this talk I’ll describe recent and ongoing work to establish the pieces of this challenging jigsaw, and start fitting them together and using them, focussing especially on Morello (capability-enabled CHERI -Arm) sequential semantics and security proofs, and on Arm-A sequential and relaxed virtual-memory concurrent semantics and reasoning. I’ll mention some pros and cons of wrestling with real-world architecture.

This talk is part of the Isaac Newton Institute Seminar Series series.

This talk is included in these lists:

• All CMS events
• Featured lists
• INI info aggregator
• Isaac Newton Institute Seminar Series
• School of Physical Sciences
• Seminar Room 1, Newton Institute
• bld31

Note that ex-directory lists are not shown.