Relational Hoare Logic for Realistically Modelled Machine Code
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.
Cite
@article{arxiv.2505.14348,
title = {Relational Hoare Logic for Realistically Modelled Machine Code},
author = {Denis Mazzucato and Abdalrhman Mohamed and Juneyoung Lee and Clark Barrett and Jim Grundy and John Harrison and Corina S. Pasareanu},
journal= {arXiv preprint arXiv:2505.14348},
year = {2025}
}
Comments
Denis Mazzucato and Abdalrhman Mohamed contributed equally to this work; Juneyoung Lee is the corresponding author: lebjuney@amazon.com; 29 pages, 3 Figures; accepted at the 37th International Conference on Computer Aided Verification (CAV) 2025