University of Cambridge > Talks.cam > Isaac Newton Institute Seminar Series > Wrestling with real systems

Wrestling with real systems

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

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.

Tell a friend about this talk:

This talk is included in these lists:

Note that ex-directory lists are not shown.

 

© 2006-2022 Talks.cam, University of Cambridge. Contact Us | Help and Documentation | Privacy and Publicity