Verified Software Toolchains: Islaris: Verification of Machine Code Against Authoritative ISA Semantics

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

• Angus Hammond (University of Cambridge)
• Wednesday 13 July 2022, 10:15-10:45
• Seminar Room 2, Newton Institute.

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

VSO2 - Verified software

Recent years have seen great advances towards verifying large-scale systems code. However, these verifications are usually based on hand-written assembly or machine-code semantics for the underlying architecture that only cover a small part of the instruction set architecture (ISA). In contrast, other recent work has used Sail to establish formal models for large real-world architectures, including Armv8-A and RISC -V, that are comprehensive (complete enough to boot an operating system or hypervisor) and authoritative (automatically derived from the Arm internal model and validated against the Arm validation suite, and adopted as the official formal specification by RISC -V International, respectively). But the scale and complexity of these models makes them challenging to use as a basis for verification. In this paper, we propose \emph{Islaris}, the first system to support verification of machine code above these complete and authoritative real-world ISA specifications.   Islaris uses a novel combination of \emph{SMT-solver-based symbolic execution} (the Isla symbolic executor) and \emph{automated reasoning in a foundational program logic} (a new separation logic we derive using Iris in Coq). We show that this approach can handle Armv8-A and RISC -V machine code exercising a wide range of systems features, including installing and calling exception vectors, parametric on a relocation address offset (from the production pKVM hypervisor); unaligned access faults; memory-mapped IO; and compiled C code using inline assembly and function pointers.

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 2, Newton Institute
• bld31

Note that ex-directory lists are not shown.