Relational Hoare Logic for Realistically Modelled Machine Code
Fuente:
arXiv
Saved in:
| Main Authors: | , , , , , , |
|---|---|
| Format: | Preprint |
| Published: |
2025
|
| Subjects: | |
| Online Access: | |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
| _version_ | 1866912384203882496 |
|---|---|
| author | Mazzucato, Denis Mohamed, Abdalrhman Lee, Juneyoung Barrett, Clark Grundy, Jim Harrison, John Pasareanu, Corina S. |
| author_facet | Mazzucato, Denis Mohamed, Abdalrhman Lee, Juneyoung Barrett, Clark Grundy, Jim Harrison, John Pasareanu, Corina S. |
| contents | 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. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2505_14348 |
| institution | arXiv |
| publishDate | 2025 |
| record_format | arxiv |
| spellingShingle | Relational Hoare Logic for Realistically Modelled Machine Code Mazzucato, Denis Mohamed, Abdalrhman Lee, Juneyoung Barrett, Clark Grundy, Jim Harrison, John Pasareanu, Corina S. Logic in Computer Science 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. |
| title | Relational Hoare Logic for Realistically Modelled Machine Code |
| topic | Logic in Computer Science |
| url | https://arxiv.org/abs/2505.14348 |