Static Analysis Of Binary Code With Memory ...
Document type :
Communication dans un congrès avec actes
Title :
Static Analysis Of Binary Code With Memory Indirections Using Polyhedra
Author(s) :
Ballabriga, Clement [Auteur]
Centre de Recherche en Informatique, Signal et Automatique de Lille - UMR 9189 [CRIStAL]
Forget, Julien [Auteur]
Centre de Recherche en Informatique, Signal et Automatique de Lille - UMR 9189 [CRIStAL]
Gonnord, Laure [Auteur]
Université Claude Bernard Lyon 1 [UCBL]
CASH - Compilation and Analysis, Software and Hardware [CASH]
Laboratoire de l'Informatique du Parallélisme [LIP]
Lipari, Giuseppe [Auteur]
Centre de Recherche en Informatique, Signal et Automatique de Lille - UMR 9189 [CRIStAL]
Ruiz, Jordy [Auteur]
Centre de Recherche en Informatique, Signal et Automatique de Lille - UMR 9189 [CRIStAL]

Centre de Recherche en Informatique, Signal et Automatique de Lille - UMR 9189 [CRIStAL]
Forget, Julien [Auteur]

Centre de Recherche en Informatique, Signal et Automatique de Lille - UMR 9189 [CRIStAL]
Gonnord, Laure [Auteur]
Université Claude Bernard Lyon 1 [UCBL]
CASH - Compilation and Analysis, Software and Hardware [CASH]
Laboratoire de l'Informatique du Parallélisme [LIP]
Lipari, Giuseppe [Auteur]

Centre de Recherche en Informatique, Signal et Automatique de Lille - UMR 9189 [CRIStAL]
Ruiz, Jordy [Auteur]
Centre de Recherche en Informatique, Signal et Automatique de Lille - UMR 9189 [CRIStAL]
Conference title :
VMCAI'19 - International Conference on Verification, Model Checking, and Abstract Interpretation
City :
Cascais
Country :
Portugal
Start date of the conference :
2019-01-13
Journal title :
LNCS
Publisher :
Springer
English keyword(s) :
binary analysis
Worst-case Execution Time WCET
polyhedra
Worst-case Execution Time WCET
polyhedra
HAL domain(s) :
Informatique [cs]/Informatique et langage [cs.CL]
Informatique [cs]/Systèmes embarqués
Informatique [cs]/Algorithme et structure de données [cs.DS]
Informatique [cs]/Systèmes embarqués
Informatique [cs]/Algorithme et structure de données [cs.DS]
English abstract : [en]
In this paper we propose a new abstract domain for staticanalysis of binary code. Our motivation stems from the need to im-prove the precision of the estimation of the Worst-Case Execution Time(WCET) of safety-critical ...
Show more >In this paper we propose a new abstract domain for staticanalysis of binary code. Our motivation stems from the need to im-prove the precision of the estimation of the Worst-Case Execution Time(WCET) of safety-critical real-time code. WCET estimation requirescomputing information such as upper bounds on the number of loopiterations, unfeasible execution paths, etc. These estimations are usuallyperformed on binary code, mainly to avoid making assumptions on howthe compiler works. Our abstract domain, based on polyhedra and ontwo mapping functions that associate polyhedra variables with registersand memory, targets the precise computation of such information. Weprove the correctness of the method, and demonstrate its effectivenesson benchmarks and examples from typical embedded code.Show less >
Show more >In this paper we propose a new abstract domain for staticanalysis of binary code. Our motivation stems from the need to im-prove the precision of the estimation of the Worst-Case Execution Time(WCET) of safety-critical real-time code. WCET estimation requirescomputing information such as upper bounds on the number of loopiterations, unfeasible execution paths, etc. These estimations are usuallyperformed on binary code, mainly to avoid making assumptions on howthe compiler works. Our abstract domain, based on polyhedra and ontwo mapping functions that associate polyhedra variables with registersand memory, targets the precise computation of such information. Weprove the correctness of the method, and demonstrate its effectivenesson benchmarks and examples from typical embedded code.Show less >
Language :
Anglais
Peer reviewed article :
Oui
Audience :
Internationale
Popular science :
Non
ANR Project :
Collections :
Source :
Files
- https://hal.archives-ouvertes.fr/hal-01939659/document
- Open access
- Access the document
- https://hal.archives-ouvertes.fr/hal-01939659/document
- Open access
- Access the document
- https://hal.archives-ouvertes.fr/hal-01939659/document
- Open access
- Access the document