Static Analysis of Endian Portability by Abstract InterpretationVirtual
Sun 17 Oct 2021 21:50 - 22:05 at Zurich B - Session 3A Chair(s): Suvam Mukherjee
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 little- and 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.
Sun 17 OctDisplayed time zone: Central Time (US & Canada) change
13:50 - 15:10 | |||
13:50 15mTalk | Static Analysis of Endian Portability by Abstract InterpretationVirtual SAS David Delmas Airbus & Sorbonne Université, Abdelraouf Ouadjaout Sorbonne Université, Antoine Miné Sorbonne Université | ||
14:05 15mTalk | Verified Functional Programming of an Abstract InterpreterVirtual SAS | ||
14:30 15mTalk | Data Abstraction: A General Framework to Handle Program Verification of Data StructuresVirtual SAS | ||
14:45 25mLive Q&A | Session 3A Discussion, Questions and AnswersVirtual SAS |
21:50 - 23:10 | |||
21:50 15mTalk | Static Analysis of Endian Portability by Abstract InterpretationVirtual SAS David Delmas Airbus & Sorbonne Université, Abdelraouf Ouadjaout Sorbonne Université, Antoine Miné Sorbonne Université | ||
22:05 15mTalk | Verified Functional Programming of an Abstract InterpreterVirtual SAS | ||
22:30 15mTalk | Data Abstraction: A General Framework to Handle Program Verification of Data StructuresVirtual SAS | ||
22:45 25mLive Q&A | Session 3A Discussion, Questions and AnswersVirtual SAS |