“Relational Hoare Logic for Realistically Modelled Machine Code” by Denis Mazzucato, Abdalrhman Mohamed, Juneyoung Lee, Clark Barrett, Jim Grundy, John Harrison, and Corina S. P{\u{a}}s{\u{a}}reanu. In Proceedings of the 37^th International Conference on Computer Aided Verification (CAV '25), (Ruzica Piskac and Zvonimir Rakamaric, eds.), July 2025, pp. 389-413. Zagreb, Croatia.
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.
BibTeX entry:
@inproceedings{MML+25,
author = {Denis Mazzucato and Abdalrhman Mohamed and Juneyoung Lee and
Clark Barrett and Jim Grundy and John Harrison and Corina S.
P{\u{a}}s{\u{a}}reanu},
editor = {Ruzica Piskac and Zvonimir Rakamari{\'c}},
title = {Relational Hoare Logic for Realistically Modelled Machine Code},
booktitle = {Proceedings of the {\it 37^{th}} International Conference
on Computer Aided Verification (CAV '25)},
series = {Lecture Notes in Computer Science},
volume = {15931},
pages = {389--413},
publisher = {Springer},
month = jul,
year = {2025},
doi = {10.1007/978-3-031-98668-0_19},
note = {Zagreb, Croatia},
url = {https://doi.org/10.1007/978-3-031-98668-0_19}
}
(This webpage was created with bibtex2web.)