Paper Info
Title
Islaris: Verification of Machine Code Against Authoritative ISA Semantics
Abstract
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 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 SMT-solver-based symbolic execution (the Isla symbolic executor) and 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, code 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.
Year
DOI
Venue
2022
10.1145/3519939.3523434
PROCEEDINGS OF THE 43RD ACM SIGPLAN INTERNATIONAL CONFERENCE ON PROGRAMMING LANGUAGE DESIGN AND IMPLEMENTATION (PLDI '22)
Keywords
DocType
Citations 
assembly, verification, separation logic, proof automation, Iris, Isla, Sail, Coq, Arm, RISC-V
Conference
0
PageRank 
References 
Authors
0.34
0
8
Name
Order
Citations
PageRank
Michael Sammler132.10
Angus Hammond200.34
Rodolphe Lepigre300.34
Brian Campbell400.68
Jean Pichon-Pharabod510.69
Derek Dreyer654230.97
Deepak Garg758145.48
Peter Sewell8144668.16