Journal of Automated Reasoning

, Volume 60, Issue 3, pp 337–363 | Cite as

Relational Program Reasoning Using Compiler IR

Combining Static Verification and Dynamic Analysis
  • Moritz Kiefer
  • Vladimir Klebanov
  • Mattias Ulbrich
Article
  • 49 Downloads

Abstract

Relational program reasoning is concerned with formally comparing pairs of executions of programs. Prominent examples of relational reasoning are program equivalence checking (which considers executions from different programs) and detecting illicit information flow (which considers two executions of the same program). The abstract logical foundations of relational reasoning are, by now, sufficiently well understood. In this paper, we address some of the challenges that remain to make the reasoning practicable. Two major ones are dealing with the feature richness of programming languages such as C and with the weakly structured control flow that many real-world programs exhibit. A popular approach to control this complexity is to define the analyses on the level of an intermediate program representation (IR) such as one generated by modern compilers. In this paper we describe the ideas and insights behind IR-based relational verification. We present a program equivalence checker for C programs that operates on LLVM IR. To extend the reach of the approach and to make it more efficient, we show how dynamic analyses can be employed to support and strengthen the static verification. The effectiveness of the approach is demonstrated by automatically verifying equivalence of functions from different implementations of the standard C library.

Notes

Acknowledgements

This work was partially supported by the German National Science Foundation (DFG) under the IMPROVE APS project within the priority program SPP 1593 “Design For Future—Managed Software Evolution”.

References

  1. 1.
    Balliu, M., Dam, M., Guanciale, R.: Automating information flow analysis of low level code. In: Proceedings of the 2014 ACM SIGSAC Conference on Computer and Communications Security, CCS ’14, pp. 1080–1091. ACM (2014)Google Scholar
  2. 2.
    Banerjee, A., Naumann, D.A., Nikouei, M.: Relational logic with framing and hypotheses. In: 36th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science, FSTTCS 2016, December 13–15, 2016, Chennai, India, pp. 11:1–11:16 (2016). doi: 10.4230/LIPIcs.FSTTCS.2016.11
  3. 3.
    Barnett, M., Chang, B.Y.E., DeLine, R., Jacobs, B., Leino, K.R.M.: Boogie: A modular reusable verifier for object-oriented programs. In: Proceedings of the 4th International Conference on Formal Methods for Components and Objects, FMCO’05, pp. 364–387. Springer, Berlin (2006)Google Scholar
  4. 4.
    Barthe, G., Crespo, J.M., Kunz, C.: Relational verification using product programs. In: M. Butler, W. Schulte (eds.) Proceedings, 17th International Symposium on Formal Methods (FM), Lecture Notes in Computer Science, vol. 6664, pp. 200–214. Springer (2011)Google Scholar
  5. 5.
    Barthe, G., Crespo, J.M., Kunz, C.: Beyond 2-safety: Asymmetric product programs for relational program verification. In: Logical Foundations of Computer Science, International Symposium, LFCS 2013, San Diego, CA, USA, January 6–8, 2013. Proceedings, pp. 29–43 (2013). doi: 10.1007/978-3-642-35722-0_3
  6. 6.
    Beringer, L.: Relational decomposition. In: Proceedings of the 2nd International Conference on Interactive Theorem Proving (ITP), Lecture Notes in Computer Science, vol. 6898, pp. 39–54. Springer, Berlin (2011)Google Scholar
  7. 7.
    Beyene, T.A., Popeea, C., Rybalchenko, A.: Solving existentially quantified Horn clauses. In: N. Sharygina, H. Veith (eds.) Computer Aided Verification—25th International Conference, CAV 2013, Proceedings, Lecture Notes in Computer Science, vol. 8044, pp. 869–882. Springer, Berlin (2013)Google Scholar
  8. 8.
    Bjørner, N., McMillan, K.L., Rybalchenko, A.: On solving universally quantified Horn clauses. In: F. Logozzo, M. Fähndrich (eds.) Static Analysis—20th International Symposium, SAS 2013, Proceedings, Lecture Notes in Computer Science, vol. 7935, pp. 105–125. Springer (2013)Google Scholar
  9. 9.
    De Angelis, E., Fioravanti, F., Pettorossi, A., Proietti, M.: Relational verification through Horn clause transformation. In: Static Analysis - 23rd International Symposium, SAS 2016, Edinburgh, UK, September 8–10, 2016, Proceedings, pp. 147–169 (2016). doi: 10.1007/978-3-662-53413-7_8
  10. 10.
    Duff, T.: Explanation, please! Online posting. Available at https://www.lysator.liu.se/c/duffs-device.html (1988)
  11. 11.
    Ernst, M.D., Perkins, J.H., Guo, P.J., McCamant, S., Pacheco, C., Tschantz, M.S., Xiao, C.: The daikon system for dynamic detection of likely invariants. Sci. Comput. Program. 69(1–3), 35–45 (2007).https://homes.cs.washington.edu/~mernst/pubs/daikon-tool-scp2007.pdf
  12. 12.
    Falke, S., Kapur, D., Sinz, C.: Termination analysis of imperative programs using bitvector arithmetic. In: Proceedings of the 4th International Conference on Verified Software: Theories, Tools, Experiments (VSTTE’12), pp. 261–277. Springer, Berlin (2012)Google Scholar
  13. 13.
    Felsing, D., Grebing, S., Klebanov, V., Rümmer, P., Ulbrich, M.: Automating regression verification. In: Proceedings of the 29th ACM/IEEE International Conference on Automated Software Engineering, ASE ’14, pp. 349–360. ACM (2014)Google Scholar
  14. 14.
    Giesl, J., Thiemann, R., Schneider-Kamp, P., Falke, S.: Automated termination proofs with AProVE. In: V. van Oostrom (ed.) Rewriting Techniques and Applications, 15th International Conference (RTA 2004), Proceedings, Lecture Notes in Computer Science, vol. 3091, pp. 210–220. Springer (2004)Google Scholar
  15. 15.
  16. 16.
    Godlin, B., Strichman, O.: Regression verification. In: Proceedings of the 46th Annual Design Automation Conference, DAC ’09, pp. 466–471. ACM (2009)Google Scholar
  17. 17.
    Gurfinkel, A., Kahsai, T., Komuravelli, A., Navas, J.A.: The SeaHorn verification framework. In: D. Kroening, C.S. Pasareanu (eds.) Computer Aided Verification (CAV), Proceedings, Lecture Notes in Computer Science, vol. 9206, pp. 343–361. Springer (2015)Google Scholar
  18. 18.
    Hawblitzel, C., Kawaguchi, M., Lahiri, S.K., Rebêlo, H.: Mutual summaries: Unifying program comparison techniques. In: Proceedings, First International Workshop on Intermediate Verification Languages (BOOGIE) (2011). Available at http://research.microsoft.com/en-us/um/people/moskal/boogie2011/boogie2011_pg40.pdf
  19. 19.
    Hawblitzel, C., Kawaguchi, M., Lahiri, S.K., Rebêlo, H.: Towards modularly comparing programs using automated theorem provers. In: M.P. Bonacina (ed.) Automated Deduction - CADE-24 - 24th International Conference on Automated Deduction, 2013. Proceedings, Lecture Notes in Computer Science, vol. 7898, pp. 282–299. Springer (2013)Google Scholar
  20. 20.
    Hoder, K., Bjørner, N.: Generalized property directed reachability. In: Proceedings of the 15th International Conference on Theory and Applications of Satisfiability Testing, SAT’12, pp. 157–171. Springer, Berlin (2012)Google Scholar
  21. 21.
    Lahiri, S.K., Hawblitzel, C., Kawaguchi, M., Rebêlo, H.: SymDiff: A language-agnostic semantic diff tool for imperative programs. In: Proceedings of the 24th International Conference on Computer Aided Verification, CAV’12, pp. 712–717. Springer, Berlin (2012)Google Scholar
  22. 22.
    Lattner, C., Adve, V.: LLVM: A compilation framework for lifelong program analysis & transformation. In: Proceedings of the International Symposium on Code Generation and Optimization: Feedback-directed and Runtime Optimization, CGO ’04. IEEE Computer Society (2004)Google Scholar
  23. 23.
    von Leitner, F.: diet libc.https://www.fefe.de/dietlibc/ (2016)
  24. 24.
    McMillan, K., Rybalchenko, A.: Computing relational fixed points using interpolation. Tech. Rep. MSR-TR-2013-6, Microsoft Research (2013).http://research.microsoft.com/apps/pubs/default.aspx?id=180055
  25. 25.
    Merz, F., Falke, S., Sinz, C.: LLBMC: Bounded model checking of C and C++ programs using a compiler IR. In: Proceedings of the 4th International Conference on Verified Software: Theories, Tools, Experiments, VSTTE’12, pp. 146–161. Springer-Verlag, Berlin, Heidelberg (2012)Google Scholar
  26. 26.
    Myers, E.W.: An O(ND) difference algorithm and its variations. Algorithmica 1(2), 251–266 (1986)MathSciNetCrossRefMATHGoogle Scholar
  27. 27.
    Necula, G.C.: Translation validation for an optimizing compiler. SIGPLAN Notes 35(5), 83–94 (2000). doi: 10.1145/358438.349314 CrossRefGoogle Scholar
  28. 28.
    Nguyen, T., Kapur, D., Weimer, W., Forrest, S.: Dig: a dynamic invariant generator for polynomial and array invariants. ACM Trans. Softw. Eng. Methodol. 23(4), 30:1–33:30 (2014). doi: 10.1145/2556782 CrossRefGoogle Scholar
  29. 29.
  30. 30.
    Partush, N., Yahav, E.: Abstract semantic differencing via speculative correlation. In: Proceedings of the 2014 ACM International Conference on Object Oriented Programming Systems Languages & Applications, OOPSLA ’14, pp. 811–828. ACM (2014). doi: 10.1145/2660193.2660245
  31. 31.
    Rakamaric, Z., Emmi, M.: SMACK: decoupling source language details from verifier implementations. In: Computer Aided Verification—26th International Conference, CAV 2014, Held as Part of the Vienna Summer of Logic, VSL 2014, Vienna, Austria, July 18–22, 2014. Proceedings, pp. 106–113 (2014). doi: 10.1007/978-3-319-08867-9_7
  32. 32.
    Rümmer, P., Hojjat, H., Kuncak, V.: Disjunctive interpolants for Horn-clause verification. In: Proceedings of the 25th International Conference on Computer Aided Verification, CAV’13, pp. 347–363. Springer, Berlin (2013)Google Scholar
  33. 33.
    Sharma, R., Aiken, A.: From invariant checking to invariant inference using randomized search. In: A. Biere, R. Bloem (eds.) Computer Aided Verification: 26th International Conference, CAV 2014, Held as Part of the Vienna Summer of Logic, VSL 2014, Vienna, Austria, July 18–22, 2014. Proceedings, pp. 88–105. Springer International Publishing, Cham (2014). doi: 10.1007/978-3-319-08867-9_6
  34. 34.
    Sharma, R., Gupta, S., Hariharan, B., Aiken, A., Liang, P., Nori, A.V.: A data driven approach for algebraic loop invariants. In: M. Felleisen, P. Gardner (eds.) Programming Languages and Systems: 22nd European Symposium on Programming, ESOP 2013, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2013, Rome, Italy, March 16–24, 2013. Proceedings, pp. 574–592. Springer Berlin Heidelberg, Berlin, Heidelberg (2013). doi: 10.1007/978-3-642-37036-6_31
  35. 35.
    Smith, E.W., Dill, D.L.: Automatic formal verification of block cipher implementations. In: Proceedings of the 2008 International Conference on Formal Methods in Computer-Aided Design, FMCAD ’08, pp. 6:1–6:7. IEEE Press, Piscataway, NJ, USA (2008). http://dl.acm.org/citation.cfm?id=1517424.1517430
  36. 36.
    Stepp, M., Tate, R., Lerner, S.: Equality-based translation validator for LLVM. In: Proceedings of the 23rd international conference on Computer Aided Verification, pp. 737–742. Springer, Berlin (2011). http://www.cs.cornell.edu/~ross/publications/eqsat/
  37. 37.
    Tristan, J.B., Govereau, P., Morrisett, G.: Evaluating value-graph translation validation for llvm. SIGPLAN Notes 46(6), 295–305 (2011). doi: 10.1145/1993316.1993533 CrossRefGoogle Scholar
  38. 38.
    Ulbrich, M.: Dynamic logic for an intermediate language: Verification, interaction and refinement. Ph.D. thesis, Karlsruhe Institute of Technology (2013).http://nbn-resolving.org/urn:nbn:de:swb:90-411691
  39. 39.
    Verdoolaege, S., Janssens, G., Bruynooghe, M.: Equivalence checking of static affine programs using widening to handle recurrences. ACM Trans. Program. Lang. Syst 34(3), 11:1–11:35 (2012). doi: 10.1145/2362389.2362390 CrossRefMATHGoogle Scholar
  40. 40.
    Verdoolaege, S., Palkovic, M., Bruynooghe, M., Janssens, G., Catthoor, F.: Experience with widening based equivalence checking in realistic multimedia systems. J. Electron. Test. 26(2), 279–292 (2010)CrossRefGoogle Scholar
  41. 41.
    Welsch, Y., Poetzsch-Heffter, A.: Verifying backwards compatibility of object-oriented libraries using Boogie. In: Proceedings of the 14th Workshop on Formal Techniques for Java-like Programs, FTfJP ’12, pp. 35–41. ACM (2012)Google Scholar
  42. 42.
    Zaks, A., Pnueli, A.: Covac: Compiler validation by program analysis of the cross-product. In: FM 2008: Formal Methods, 15th International Symposium on Formal Methods, Turku, Finland, May 26–30, 2008, Proceedings, pp. 35–51 (2008). doi: 10.1007/978-3-540-68237-0_5
  43. 43.
    Zaks, A., Pnueli, A.: Program analysis for compiler validation. In: Proceedings of the 8th ACM SIGPLAN-SIGSOFT Workshop on Program Analysis for Software Tools and Engineering, PASTE ’08, pp. 1–7. ACM, New York, NY, USA (2008). doi: 10.1145/1512475.1512477

Copyright information

© Springer Science+Business Media B.V. 2017

Authors and Affiliations

  1. 1.Karlsruhe Institute of TechnologyKarlsruheGermany

Personalised recommendations