BEGIN:VCALENDAR VERSION:2.0 PRODID:-//Talks.cam//talks.cam.ac.uk// X-WR-CALNAME:Talks.cam BEGIN:VEVENT SUMMARY:Verified Software Toolchains: Islaris: Verification of Machine Cod e Against Authoritative ISA Semantics - Angus Hammond (University of Cambr idge) DTSTART:20220713T091500Z DTEND:20220713T094500Z UID:TALK176243@talks.cam.ac.uk DESCRIPTION:Recent years have seen great advances towards verifying large- scale systems code.\nHowever\, these verifications are usually based on ha nd-written assembly or machine-code semantics for the underlying architect ure 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 hypervis or) and authoritative (automatically derived from the Arm internal model a nd validated against the Arm validation suite\, and adopted as the officia l formal specification by RISC-V International\, respectively). But the sc ale and complexity of these models makes them challenging to use as a basi s for verification.\nIn this paper\, we propose \\emph{Islaris}\, the firs t 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 progr am logic} (a new separation logic we derive using Iris in Coq). We show th at this approach can handle Armv8-A and RISC-V machine code exercising a w ide 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 compil ed C code using inline assembly and function pointers. LOCATION:Seminar Room 2\, Newton Institute END:VEVENT END:VCALENDAR