Top

Published in:

2019 | OriginalPaper | Chapter

Static Analysis of Binary Code with Memory Indirections Using Polyhedra

Authors : Clément Ballabriga, Julien Forget, Laure Gonnord, Giuseppe Lipari, Jordy Ruiz

Published in: Verification, Model Checking, and Abstract Interpretation

Publisher: Springer International Publishing

Activate our intelligent search to find suitable subject content or patents.

search-config

AI-assisted search

Off

Abstract

In this paper we propose a new abstract domain for static analysis of binary code. Our motivation stems from the need to improve the precision of the estimation of the Worst-Case Execution Time (WCET) of safety-critical real-time code. WCET estimation requires computing information such as upper bounds on the number of loop iterations, unfeasible execution paths, etc. These estimations are usually performed on binary code, mainly to avoid making assumptions on how the compiler works. Our abstract domain, based to polyhedra and on two mapping functions that associate polyhedra variables with registers and memory, targets the precise computation of such information. We prove the correctness of the method, and demonstrate its effectiveness on benchmarks and examples from typical embedded code.

Dont have a licence yet? Then find out more about our products and how to get one now:

Springer Professional "Wirtschaft+Technik"

Online-Abonnement

Mit Springer Professional "Wirtschaft+Technik" erhalten Sie Zugriff auf:

über 102.000 Bücher
über 537 Zeitschriften

aus folgenden Fachgebieten:

Automobil + Motoren
Bauwesen + Immobilien
Business IT + Informatik
Elektrotechnik + Elektronik
Energie + Nachhaltigkeit
Finance + Banking
Management + Führung
Marketing + Vertrieb
Maschinenbau + Werkstoffe
Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

inform now

Springer Professional "Technik"

Online-Abonnement

Mit Springer Professional "Technik" erhalten Sie Zugriff auf:

über 67.000 Bücher
über 390 Zeitschriften

aus folgenden Fachgebieten:

Automobil + Motoren
Bauwesen + Immobilien
Business IT + Informatik
Elektrotechnik + Elektronik
Energie + Nachhaltigkeit
Maschinenbau + Werkstoffe

Jetzt Wissensvorsprung sichern!

inform now

Springer Professional "Wirtschaft"

Online-Abonnement

Mit Springer Professional "Wirtschaft" erhalten Sie Zugriff auf:

über 67.000 Bücher
über 340 Zeitschriften

aus folgenden Fachgebieten:

Bauwesen + Immobilien
Business IT + Informatik
Finance + Banking
Management + Führung
Marketing + Vertrieb
Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

inform now

previous chapter Lazy but Effective Functional Synthesis

next chapter Disjunctive Relational Abstract Interpretation for Interprocedural Program Analysis

The original bench listing is available here: https://pastebin.com/C5UPYRx3.

Aho, A.V., Lam, M.S., Sethi, R., Ullman, J.D.: Compilers: Principles, Techniques, and Tools, 2nd edn. Addison-Wesley Longman Publishing Co. Inc., Boston (2006)MATH

Ammarguellat, Z., Harrison, III, W.L.: Automatic recognition of induction variables and recurrence relations by abstract interpretation. In: Proceedings of the ACM SIGPLAN 1990 Conference on Programming Language Design and Implementation, PLDI 1990, pp. 283–295. ACM, New York (1990)

Bagnara, R., Hill, P.M., Zaffanella, E.: The Parma Polyhedra Library: toward a complete set of numerical abstractions for the analysis and verification of hardware and software systems. Sci. Comput. Program. 72(1), 3–21 (2008)MathSciNetCrossRef

Balakrishnan, G., Reps, T.: Analyzing memory accesses in x86 executables. In: Duesterwald, E. (ed.) CC 2004. LNCS, vol. 2985, pp. 5–23. Springer, Heidelberg (2004). https://doi.org/10.1007/978-3-540-24723-4_2CrossRef

Ballabriga, C., Cassé, H., Rochange, C., Sainrat, P.: OTAWA: an open toolbox for adaptive WCET analysis. In: Min, S.L., Pettit, R., Puschner, P., Ungerer, T. (eds.) SEUS 2010. LNCS, vol. 6399, pp. 35–46. Springer, Heidelberg (2010). https://doi.org/10.1007/978-3-642-16256-5_6CrossRef

Ballabriga, C., Forget, J., Lipari, G.: Symbolic WCET computation. ACM Trans. Embed. Comput. Syst. (TECS) 17(2), 39 (2018)

Bardin, S., Herrmann, P., Védrine, F.: Refinement-based CFG reconstruction from unstructured programs. In: Jhala, R., Schmidt, D. (eds.) VMCAI 2011. LNCS, vol. 6538, pp. 54–69. Springer, Heidelberg (2011). https://doi.org/10.1007/978-3-642-18275-4_6CrossRef

Bonenfant, A., de Michiel, M., Sainrat, P.: oRange: a tool for static loop bound analysis. In: Workshop on Resource Analysis, University of Hertfordshire, Hatfield, UK (2008)

Broman, D.: A brief overview of the KTA WCET tool. arXiv preprint arXiv:1712.05264 (2017)

10.

Bygde, S., Lisper, B., Holsti, N.: Fully bounded polyhedral analysis of integers with wrapping. Electron. Notes Theor. Comput. Sci. 288, 3–13 (2012)CrossRef

11.

Correnson, L., Signoles, J.: Combining analyses for C program verification. In: Stoelinga, M., Pinger, R. (eds.) FMICS 2012. LNCS, vol. 7437, pp. 108–130. Springer, Heidelberg (2012). https://doi.org/10.1007/978-3-642-32469-7_8CrossRef

12.

Cousot, P., Halbwachs, N.: Automatic discovery of linear restraints among variables of a program. In: Proceedings of the 5th ACM SIGACT-SIGPLAN Symposium on Principles of Programming Languages (POPL), pp. 84–96. ACM (1978). https://doi.org/10.1145/512760.512770

13.

Djoudi, A., Bardin, S.: BINSEC: binary code analysis with low-level regions. In: Baier, C., Tinelli, C. (eds.) TACAS 2015. LNCS, vol. 9035, pp. 212–217. Springer, Heidelberg (2015). https://doi.org/10.1007/978-3-662-46681-0_17CrossRef

14.

Ermedahl, A., Sandberg, C., Gustafsson, J., Bygde, S., Lisper, B.: Loop bound analysis based on a combination of program slicing, abstract interpretation, and invariant analysis. In: Rochange, C. (ed.) 7th International Workshop on Worst-Case Execution Time Analysis (WCET 2007). OpenAccess Series in Informatics (OASIcs), vol. 6. Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik, Dagstuhl, Germany (2007)

15.

Gulwani, S., Mehra, K.K., Chilimbi, T.: Speed: precise and efficient static estimation of program computational complexity. In: ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL 2009), pp. 127–139. ACM (2009)

16.

Gustafsson, J., Betts, A., Ermedahl, A., Lisper, B.: The Mälardalen WCET benchmarks: past, present and future. In: OASIcs-OpenAccess Series in Informatics, vol. 15. Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik (2010)

17.

Hardekopf, B., Lin, C.: The ant and the grasshopper: fast and accurate pointer analysis for millions of lines of code. ACM SIGPLAN Not. 42(6), 290–299 (2007)CrossRef

18.

Henry, J., Monniaux, D., Moy, M.: Pagai: a path sensitive static analyser. Electron. Notes Theor. Comput. Sci. 289, 15–25 (2012)CrossRef

19.

Hind, M.: Pointer analysis: haven’t we solved this problem yet? In: ACM SIGPLAN-SIGSOFT Workshop on Program Analysis for Software Tools and Engineering (PASTE 2001), pp. 54–61. ACM, New York (2001)

20.

Karr, M.: Affine relationships among variables of a program. Acta Inform. 6(2), 133–151 (1976)MathSciNetCrossRef

21.

Kästner, D., et al.: Astrée: proving the absence of runtime errors. In: Embedded Real Time Software and Systems (ERTS2 2010), p. 9, May 2010

22.

Lisper, B.: SWEET – a tool for wcet flow analysis (extended abstract). In: Margaria, T., Steffen, B. (eds.) ISoLA 2014. LNCS, vol. 8803, pp. 482–485. Springer, Heidelberg (2014). https://doi.org/10.1007/978-3-662-45231-8_38CrossRef

23.

Tamburini, P., Stagni, R., Cappello, A.: Design of a modular platform for static analysis. In: Spoto, F. (ed.) 9th Workshop on Tools for Automatic Program Analysis (TAPAS 2018). Lecture Notes in Computer Science (LNCS). Springer, Cham, p. 4, August 2018

24.

Miné, A.: Field-sensitive value analysis of embedded C programs with union types and pointer arithmetics. In: ACM SIGPLAN/SIGBED Conference on Languages, Compilers, and Tools for Embedded Systems (LCTES 2006), pp. 54–63 (2006)

25.

Pouchet, L.N.: Polybench: the polyhedral benchmark suite (2012). http://www.cs.ucla.edu/pouchet/software/polybench

26.

Reps, T., Balakrishnan, G.: Improved memory-access analysis for x86 executables. In: Hendren, L. (ed.) CC 2008. LNCS, vol. 4959, pp. 16–35. Springer, Heidelberg (2008). https://doi.org/10.1007/978-3-540-78791-4_2CrossRef

27.

Sepp, A., Mihaila, B., Simon, A.: Precise static analysis of binaries by extracting relational information. In: 18th Working Conference on Reverse Engineering (WCRE 2011). IEEE (2011)

28.

Sharir, M., Pnueli, A.: Two approaches to interprocedural data flow analysis. Technical report, New York University. Courant Institute of Mathematical Sciences. Computer Science Department (1978)

29.

Tarjan, R.: Depth-first search and linear graph algorithms. SIAM J. Comput. 1(2), 146–160 (1972)MathSciNetCrossRef

30.

Venet, A.: The gauge domain: scalable analysis of linear inequality invariants. In: 24th International Conference on Computer Aided Verification (CAV 2012), pp. 139–154 (2012)CrossRef

Title: Static Analysis of Binary Code with Memory Indirections Using Polyhedra
Authors: Clément Ballabriga
Julien Forget
Laure Gonnord
Giuseppe Lipari
Jordy Ruiz
Publisher: Springer International Publishing
Book: Verification, Model Checking, and Abstract Interpretation
Print ISBN: 978-3-030-11244-8

Electronic ISBN: 978-3-030-11245-5

Copyright Year: 2019
DOI: https://doi.org/10.1007/978-3-030-11245-5_6

Springer Professional

Abstract

Please log in to get access to your license.

Dont have a licence yet? Then find out more about our products and how to get one now:

Springer Professional "Wirtschaft+Technik"

Springer Professional "Technik"

Springer Professional "Wirtschaft"

Premium Partner