Static Analysis of Endian Portability by Abstract Interpretation - Sorbonne Université
Conference Papers Year : 2021

Static Analysis of Endian Portability by Abstract Interpretation

Abstract

We present a static analysis of endian portability for C programs. Our analysis can infer that a given program, or two syntactically close versions thereof, compute the same outputs when run with the same inputs on platforms with different byte-orders, a.k.a. endiannesses. We target low-level C programs that abuse C pointers and unions, hence rely on implementation-specific behaviors undefined in the C standard. Our method is based on abstract interpretation, and parametric in the choice of a numerical abstract domain. We first present a novel concrete collecting semantics, relating the behaviors of two versions of a program, running on platforms with different endiannesses. We propose a joint memory abstraction, able to infer equivalence relations between littleand big-endian memories. We introduce a novel symbolic predicate domain to infer relations between individual bytes of the variables in the two programs, which has near-linear cost, and the right amount of relationality to express (bitwise) arithmetic properties relevant to endian portability. We implemented a prototype static analyzer, able to scale to large real-world industrial software, with zero false alarms.
Fichier principal
Vignette du fichier
paper_ok.pdf (5.39 Mo) Télécharger le fichier
Origin Files produced by the author(s)

Dates and versions

hal-03450165 , version 1 (25-11-2021)

Identifiers

Cite

David Delmas, Abdelraouf Ouadjaout, Antoine Miné. Static Analysis of Endian Portability by Abstract Interpretation. 28th Static Analysis Symposium (SAS 2021), Oct 2021, Chicago, Illinois, United States. pp.102-123, ⟨10.1007/978-3-030-88806-0_5⟩. ⟨hal-03450165⟩
64 View
96 Download

Altmetric

Share

More