Class 24: The Real World

We are super lucky to have a double act by two guest speakers today: Peter Sewell and Thomas Bauereiss (Cambridge). They will talk about formal verificaton of computer architecture security properties, plus the proof automation that made that possible.

For class, please skim this blog post, as well as the paper ISA Semantics for ARMv8-A, RISC-V, and CHERI-MIPS by many authors. You just need to skim this enough to have a single question to ask the speakers, which you'll post on the forum.

Since we have a guest speaker, this week will be a bit different, just like it was when Tony gave a talk. Please write a short paragraph as a comment in the class forum thread with a single question or comment you would relay to the speaker based on the corresponding reading. It's okay if the speaker ends up answering the question or addressing the comment in the talk---often that's actually a good sign!

Here are some example things you may wish to include in such a question or comment:

1. Confusions about how things work, including technical details.
2. Ideas for future work---and questions about whether the speaker has thought about implementing them.
3. Concerns for how things may go wrong, and questions about how the speaker handles those situations.
4. Curiosities about things you found particularly impressive or interesting, and would like to hear a lot more about.

I strongly encourage you to ask questions after the talk, though it's fine if they are not the questions you originally write in the discussion board. You may want to look at other people's responses before class in order to shape the discussion. And again remember that you need to write just one paragraph to get credit, though you are free to write more if interested.