Static Analysis Of Binary Code With Memory Indirections Using Polyhedra
| Autor: | Laure Gonnord, Jordy Ruiz, Giuseppe Lipari, Julien Forget, Clément Ballabriga |
|---|---|
| Přispěvatelé: | Centre de Recherche en Informatique, Signal et Automatique de Lille - UMR 9189 (CRIStAL), Centrale Lille-Université de Lille-Centre National de la Recherche Scientifique (CNRS), Laboratoire de l'Informatique du Parallélisme (LIP), École normale supérieure de Lyon (ENS de Lyon)-Université Claude Bernard Lyon 1 (UCBL), Université de Lyon-Université de Lyon-Institut National de Recherche en Informatique et en Automatique (Inria)-Centre National de la Recherche Scientifique (CNRS), CASH - Compilation and Analysis, Software and Hardware (CASH), Inria Grenoble - Rhône-Alpes, Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria)-Laboratoire de l'Informatique du Parallélisme (LIP), Université de Lyon-Université de Lyon-Institut National de Recherche en Informatique et en Automatique (Inria)-Centre National de la Recherche Scientifique (CNRS)-École normale supérieure de Lyon (ENS de Lyon)-Université Claude Bernard Lyon 1 (UCBL), Université de Lyon-Université de Lyon-Centre National de la Recherche Scientifique (CNRS), Université Claude Bernard Lyon 1 (UCBL), Université de Lyon, ANR-17-CE23-0004,CODAS,Ordonnancement de programmes à structures de données complexes(2017), ANR-17-CE25-0003,Corteva,Une méthodologie correcte par construction pour supporter la variabilité du temps d'exécution dans les systèmes temps réel(2017), École normale supérieure - Lyon (ENS Lyon)-Université Claude Bernard Lyon 1 (UCBL), Université de Lyon-Université de Lyon-Institut National de Recherche en Informatique et en Automatique (Inria)-Centre National de la Recherche Scientifique (CNRS)-École normale supérieure - Lyon (ENS Lyon)-Université Claude Bernard Lyon 1 (UCBL), Université de Lyon-Université de Lyon-Institut National de Recherche en Informatique et en Automatique (Inria)-Centre National de la Recherche Scientifique (CNRS)-Inria Grenoble - Rhône-Alpes, Institut National de Recherche en Informatique et en Automatique (Inria) |
| Jazyk: | angličtina |
| Rok vydání: | 2019 |
| Předmět: |
050101 languages & linguistics
Correctness Computer science Computation 05 social sciences [INFO.INFO-DS]Computer Science [cs]/Data Structures and Algorithms [cs.DS] 02 engineering and technology Parallel computing Static analysis polyhedra computer.software_genre [INFO.INFO-CL]Computer Science [cs]/Computation and Language [cs.CL] Domain (software engineering) Polyhedron 0202 electrical engineering electronic engineering information engineering Code (cryptography) 020201 artificial intelligence & image processing 0501 psychology and cognitive sciences Binary code [INFO.INFO-ES]Computer Science [cs]/Embedded Systems Compiler Worst-case Execution Time WCET computer binary analysis |
| Zdroj: | VMCAI'19-International Conference on Verification, Model Checking, and Abstract Interpretation VMCAI'19-International Conference on Verification, Model Checking, and Abstract Interpretation, Jan 2019, Cascais, Portugal. pp.114-135, ⟨10.1007/978-3-030-11245-5_6⟩ Lecture Notes in Computer Science ISBN: 9783030112448 VMCAI |
| DOI: | 10.1007/978-3-030-11245-5_6⟩ |
| Popis: | International audience; 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. |
| Databáze: | OpenAIRE |
| Externí odkaz: |
|