Skip to Main content Skip to Navigation
New interface
Journal articles

Relational abstract interpretation of arrays in assembly code

Clément Ballabriga 1 Julien Forget 1 Jordy Ruiz 2 
1 SYCOMORES - Analyse symbolique et conception orientée composants pour des systèmes embarqués temps-réel modulaires
Inria Lille - Nord Europe, CRIStAL - Centre de Recherche en Informatique, Signal et Automatique de Lille - UMR 9189
Abstract : In this paper, we propose a static analysis technique for assembly code, based on abstract interpretation, to discover properties on arrays. Considering assembly code rather than source code has important advantages: we do not require to make assumptions on the compiler behaviour, and we can handle closed-source programs. The main disadvantage however, is that information about source code variables and their types, in particular about arrays, is unavailable. Instead, the binary code reasons about data-locations (registers and memory addresses) and their sizes in bytes. Without any knowledge of the source code, our analysis infers which sets of memory addresses correspond to arrays, and establishes properties on these addresses and their contents. The underlying abstract domain is relational, meaning that we can infer relations between variables of the domain. As a consequence, we can infer properties on arrays whose start address and size are dened with respect to variables of the domain, and thus can be unknown statically. Currently, no other tool operating at the assembly or binary level can infer such properties.
Document type :
Journal articles
Complete list of metadata
Contributor : Julien Forget Connect in order to contact the contributor
Submitted on : Monday, October 3, 2022 - 4:20:26 PM
Last modification on : Tuesday, December 6, 2022 - 12:42:14 PM


 Restricted access
To satisfy the distribution rights of the publisher, the document is embargoed until : 2023-04-03

Please log in to resquest access to the document




Clément Ballabriga, Julien Forget, Jordy Ruiz. Relational abstract interpretation of arrays in assembly code. Formal Methods in System Design, 2022, ⟨10.1007/s10703-022-00399-3⟩. ⟨hal-03794951⟩



Record views