Relational Hoare Logic for Realistically Modelled Machine Code

TL;DR

This paper introduces a Hoare-style logic for low-level, relational verification of machine code, enabling formal proofs of security properties like constant-time behavior directly on realistic assembly code.

Contribution

It presents a novel low-level relational Hoare logic formalized in HOL Light, capable of verifying security and correctness properties of real-world assembly programs.

Findings

Verified constant-time property of cryptographic routines

Proved equivalence between optimized and verification-friendly assembly code

Demonstrated applicability on large real-world assembly codebase

Abstract

Many security- and performance-critical domains, such as cryptography, rely on low-level verification to minimize the trusted computing surface and allow code to be written directly in assembly. However, verifying assembly code against a realistic machine model is a challenging task. Furthermore, certain security properties -- such as constant-time behavior -- require relational reasoning that goes beyond traditional correctness by linking multiple execution traces within a single specification. Yet, relational verification has been extensively explored at a higher level of abstraction. In this work, we introduce a Hoare-style logic that provides low-level, expressive relational verification. We demonstrate our approach on the s2n-bignum library, proving both constant-time discipline and equivalence between optimized and verification-friendly routines. Formalized in HOL Light, our results confirm the real-world applicability of relational verification in large assembly codebases.