Islaris: verification of machine code against authoritative ISA semantics
Michael Sammler, Angus Hammond, Rodolphe Lepigre, B. K. Campbell, Jean Pichon-Pharabod, Derek Dreyer, Deepak Garg, Peter Sewell
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.