Advertisement

Static Analysis of Binary Code with Memory Indirections Using Polyhedra

  • Clément BallabrigaEmail author
  • Julien ForgetEmail author
  • Laure GonnordEmail author
  • Giuseppe LipariEmail author
  • Jordy RuizEmail author
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 11388)

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.

References

  1. 1.
    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)zbMATHGoogle Scholar
  2. 2.
    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)Google Scholar
  3. 3.
    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)MathSciNetCrossRefGoogle Scholar
  4. 4.
    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_2CrossRefGoogle Scholar
  5. 5.
    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_6CrossRefGoogle Scholar
  6. 6.
    Ballabriga, C., Forget, J., Lipari, G.: Symbolic WCET computation. ACM Trans. Embed. Comput. Syst. (TECS) 17(2), 39 (2018)Google Scholar
  7. 7.
    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_6CrossRefGoogle Scholar
  8. 8.
    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)Google Scholar
  9. 9.
    Broman, D.: A brief overview of the KTA WCET tool. arXiv preprint arXiv:1712.05264 (2017)
  10. 10.
    Bygde, S., Lisper, B., Holsti, N.: Fully bounded polyhedral analysis of integers with wrapping. Electron. Notes Theor. Comput. Sci. 288, 3–13 (2012)CrossRefGoogle Scholar
  11. 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_8CrossRefGoogle Scholar
  12. 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. 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_17CrossRefGoogle Scholar
  14. 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)Google Scholar
  15. 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)Google Scholar
  16. 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)Google Scholar
  17. 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)CrossRefGoogle Scholar
  18. 18.
    Henry, J., Monniaux, D., Moy, M.: Pagai: a path sensitive static analyser. Electron. Notes Theor. Comput. Sci. 289, 15–25 (2012)CrossRefGoogle Scholar
  19. 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)Google Scholar
  20. 20.
    Karr, M.: Affine relationships among variables of a program. Acta Inform. 6(2), 133–151 (1976)MathSciNetCrossRefGoogle Scholar
  21. 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 2010Google Scholar
  22. 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_38CrossRefGoogle Scholar
  23. 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 2018Google Scholar
  24. 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)Google Scholar
  25. 25.
    Pouchet, L.N.: Polybench: the polyhedral benchmark suite (2012). http://www.cs.ucla.edu/pouchet/software/polybench
  26. 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_2CrossRefGoogle Scholar
  27. 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)Google Scholar
  28. 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)Google Scholar
  29. 29.
    Tarjan, R.: Depth-first search and linear graph algorithms. SIAM J. Comput. 1(2), 146–160 (1972)MathSciNetCrossRefGoogle Scholar
  30. 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)CrossRefGoogle Scholar

Copyright information

© Springer Nature Switzerland AG 2019

Authors and Affiliations

  1. 1.CRIStAL (Univ. Lille, CNRS, Centrale Lille, UMR 9189)LilleFrance
  2. 2.Univ. Lyon, LIP (UMR CNRS/ENS Lyon/UCB Lyon1/INRIA)LyonFrance

Personalised recommendations