Islaris: Verification of Machine Code Against Authoritative ISA Semantics

Michael Sammler, Angus Hammond, Rodolphe Lepigre, Brian Campbell, Jean Pichon-Pharabod, Derek Dreyer, Deepak Garg, Peter Sewell

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Abstract / Description of output

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.
Original languageEnglish
Title of host publicationProceedings of the 43rd ACM SIGPLAN International Conference on Programming Language Design and Implementation
EditorsRanjit Jhala, Işil Dillig
Number of pages16
ISBN (Print) 978-1-4503-9265-5
Publication statusPublished - 9 Jun 2022
Event 43rd ACM SIGPLAN Conference on Programming Language Design and Implementation - San Diego, United States
Duration: 15 Jun 202217 Jun 2022
Conference number: 43


Conference 43rd ACM SIGPLAN Conference on Programming Language Design and Implementation
Abbreviated titlePLDI 2022
Country/TerritoryUnited States
CitySan Diego
Internet address

Keywords / Materials (for Non-textual outputs)

  • assembly
  • verification
  • separation logic
  • proof automation
  • Iris
  • Isla
  • Sail
  • Coq
  • Arm
  • RISC-V


Dive into the research topics of 'Islaris: Verification of Machine Code Against Authoritative ISA Semantics'. Together they form a unique fingerprint.

Cite this