Islaris: Verification of Machine Code Against Authoritative ISA Semantics

References:

Problem

Machine code verification:

  1. some critical code manipulates arch features that are not exposed in higher-level languages, e.g., to access system registers to install exception vector tables, or to configure address translation; this is necessarily written in assembly.
  2. verification without needing trust or verification of any compilation or assembly steps.
  3. verify the machine code after any modifications introduced by linking or initialisation (perhaps parametrically w.r.t. these).
  4. some code is written in assembly for performance reasons.

w.r.t. With Respect To.

Grand Challenge:

In low-level code verification, it remains a grand challenge to develop tools that are demonstrably sound w.r.t. the underlying architecture and support reasoning about all of it, including all system features.

Key aspects:

  • Relaxed-memory concurrency.
    • underlying models for user code;
    • systems concurrency;
    • low-level-code verifications targeting relaxed memory, e.g., for hypervisors.

  • Fidelity and completeness w.r.t. the underlying instruction-set architecture (ISA), the sequential semantics of machine instructions.

    • hand-write ISA semantics, for the fragment of the ISA needed – typically a small user-level fragment of the ISA.
      • Typically are simplified in various ways, and have, at best, only limited validation with respect to the architectural intent or hardware implementations.
    • For x86, hand-written larger fragments in ACL2[c25], and empirical and hand-written models [c16,c17,c30].
    • Recently for Armv8-A and RISC-V:
      • Comprehensive: complete enough to boot an operating system or hypervisor
      • Authoritative.
      • Expressed in Sail [c6,c8,c9,c44,c53].

    • Problem:

      • the fidelity and coverage also makes these models intimidatingly large and complex, and only sometimes practical for mechanised proof.

        • Sail Armv8-A: 113k lines; RISC-V: 14K lines; (non-whitespace lines of specification)
        • For Armv8-A:
          • Isabelle version (auto-generated from Sail) has been used for some metatheory [c6,chapter8], [c9], but not for program verification.
          • Coq version even simple definition unfoldings take an unreasonabley long time or fail to terminate.

      • e.g. Armv8-A instruction add sp, sp, 64

        • with 146 lines in Sail, in 9 functions;
        • do much more than just computation:
          • compute arithmentic flags;
          • support subtraction as well as addition;
          • other registers;
          • sp as a banked family of regitsers, selected based on the current exception level register value.

      • e.g. ldrb instruction to load a byte.

        • over 2000 lines of specification (in Sail?)
        • alignment checks;
        • big/little endianness;
        • tagged memory;
        • different address sizes;
        • exception levels;
        • the store and prefetch instructions that are specified simultaneously.

This paper: focus on the fidelity and completeness of the model.

The challenge is how one can reason above such models while avoiding up-front idealisation, so that we retain the ability to reason about the whole architecture, and the confidence in the authoritative model.

Islaris’ Insight: the verification problem can be split into two subtasks, separating the irrelevant complexity from the inherent complexity, so that each can then be solved by techniques well suited for the respective task: SMT-based symbolic evaluation, and a mechanised program logic.

Irrelevant Complexity

Many aspects of the ISA definitions are irrelevant, because they do not influence the results of instructions or are ruled out by the system configuration.

To handle this irrelevant complexity, the Isla symbolic evaluation tool for Sail ISA specifications are extended.

Isla:

  • takes an opcode and SMT constraints, and symbolically evaluates the Sail model using an SMT solver.
  • e.g.
    • Input: the exception-level register has a specific value or some general-purpose register is aligned.
    • Output: a trace of the instruction’s register and memory accesses, constrained by the SMT formulas.
  • This can be much simpler than the full Sail definition, without irrelevant and unreachable parts, and is in a much simpler language.

Inherent Complexity

Problem Scope:

  • Address and memory manipulation.
  • Higer-order reasoning with code-pointers.
  • Reasoning about the relevant aspects of the systems architecture.
  • Modular reasoning about user-defined specifications.

Islaris:

  • define a higer-order separation logic for the Isla traces that produces machine-checkable proofs, based on Iris[c32].

  • adapts Lithium, to design proof automation that makes the verification practical.

    • Lithium: an automated (separation) logic programming language originally designed for the RefinedC type system[c56].
    • Lithium’s efficiency:
      • can be retained even without the type information relied on by RefinedC.
      • retained by using the separation logic context to guide proof search.

Overall automation

Proof automation is comparable to previous foundational approaches [c13] [c41], but for full ISA semantics rather than a simple intermediate language.

workflow

islaris workflow

Inputs:

  • Binary machine code to verify
  • Constraints (sys configuration, used for pruning)
  • user-defined specificatino in Islaris separation logic. (Used for Coq proof)
  • manual proof steps in Coq.

Tool Dependencies:

  • Coq.
  • ISA Sail Model.
  • SMT solver.
  • Iris.
  • Lithium.

ISA spec pruning and Trace generation:

  • Islaris frontend
    • invokes Isla to generate a trace describing the effects of the instructions based on the Sail ISA model.
    • Isla symbolic evaluation prunes the part of ISA specification that cannot be reached under the given constraints.
    • Traces generated by Isla is simplified based on the ISA model.
    • Islaris output a deep embedding of this trace in Coq.

Coq generation:

  • Isla trace in Coq.
  • Sail ISA model in Coq.
  • Translatino validation between Isla trace in Coq and Sail ISA model in Coq.

Islaris proof automation in Coq:

  • Islaris higher-order separation logic implemented based on Iris.
  • Lithium-based proof automation.
    • produces machine-checkable proofs.

Outputs:

  • Proof result.

Limitations

  • Islaris currently assumes single-threaded execution.

    • Supporting a sequentially consistent concurrency semantics would not be hard.
    • Armv8-A or RISC-V relaxed-memory concurrency models requires a more sophisticated separation logic, the subject of active research.

  • Islaris also does not currenlty support self-modifying code or address translation, which involve additional forms of relaxed-memory concurrency, likewise subjects of active research [c60] [c61]

    • Our underlying ISA semantics includes translation-table walks, but here we only use machine configurations that turn translation off. ???

  • Focus on 64-bit little-endian cases.

  • on small but tricky examples.

  • scaling remains future work.

Evaluation

More

Created Dec 20, 2022 // Last Updated Jan 20, 2023

If you could revise
the fundmental principles of
computer system design
to improve security...

... what would you change?