Advertisement

Generating Inductive Shape Predicates for Runtime Checking and Formal Verification

  • Jan H. Boockmann
  • Gerald LüttgenEmail author
  • Jan Tobias Mühlberg
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 11245)

Abstract

Knowing the shapes of dynamic data structures is key when formally reasoning about pointer programs. While modern shape analysis tools employ symbolic execution and machine learning to infer shapes, they often assume well-structured C code or programs written in an idealised language. In contrast, our Data Structure Investigator (DSI) tool for program comprehension analyses concrete executions and handles even C programs with complex coding styles.

Our current research on memory safety develops ways for DSI to synthesise inductive shape predicates in separation logic. In the context of trusted computing, we investigate how the inferred predicates can be employed to generate runtime checks for securely communicating dynamic data structures across trust boundaries. We also explore to what extent these predicates, together with additional information extracted by DSI, can be used within general program verifiers such as VeriFast.

This paper accompanies a talk at the ISoLA 2018 track “A Broader View on Verification: From Static to Runtime and Back”. It introduces DSI, highlights the above use cases, and sketches our approach for synthesising inductive shape predicates.

References

  1. 1.
    Aftandilian, E.E., Kelley, S., Gramazio, C., Ricci, N., Su, S.L., Guyer, S.Z.: Heapviz: interactive heap visualization for program understanding and debugging. In: Software Visualization (SOFTVIS 2010), pp. 53–62. ACM (2010)Google Scholar
  2. 2.
    Agten, P., Jacobs, B., Piessens, F.: Sound modular verification of C code executing in an unverified context. In: Principles of Programming Languages (POPL 2015), pp. 581–594. ACM (2015)Google Scholar
  3. 3.
    Blom, S., Darabi, S., Huisman, M., Oortwijn, W.: The VerCors tool set: verification of parallel and concurrent software. In: Polikarpova, N., Schneider, S. (eds.) IFM 2017. LNCS, vol. 10510, pp. 102–110. Springer, Cham (2017).  https://doi.org/10.1007/978-3-319-66845-1_7CrossRefGoogle Scholar
  4. 4.
    Brockschmidt, M., Chen, Y., Kohli, P., Krishna, S., Tarlow, D.: Learning shape analysis. In: Ranzato, F. (ed.) SAS 2017. LNCS, vol. 10422, pp. 66–87. Springer, Cham (2017).  https://doi.org/10.1007/978-3-319-66706-5_4CrossRefGoogle Scholar
  5. 5.
    Caballero, J., Grieco, G., Marron, M., Lin, Z., Urbina, D.: Artiste: automatic generation of hybrid data structure signatures from binary code executions. Technical Report TR-IMDEA-SW-2012-001, IMDEA, Spain (2012)Google Scholar
  6. 6.
    Calcagno, C., Distefano, D.: Infer: an automatic program verifier for memory safety of C programs. In: Bobaru, M., Havelund, K., Holzmann, G.J., Joshi, R. (eds.) NFM 2011. LNCS, vol. 6617, pp. 459–465. Springer, Heidelberg (2011).  https://doi.org/10.1007/978-3-642-20398-5_33CrossRefGoogle Scholar
  7. 7.
    Calcagno, C., et al.: Moving fast with software verification. In: Havelund, K., Holzmann, G., Joshi, R. (eds.) NFM 2015. LNCS, vol. 9058, pp. 3–11. Springer, Cham (2015).  https://doi.org/10.1007/978-3-319-17524-9_1Google Scholar
  8. 8.
    Haller, I., Slowinska, A., Bos, H.: Scalable data structure detection and classification for C/C++ binaries. Emp. Softw. Eng. 21(3), 778–810 (2016)CrossRefGoogle Scholar
  9. 9.
    Holík, L., Lengál, O., Rogalewicz, A., Šimáček, J., Vojnar, T.: Fully automated shape analysis based on forest automata. In: Sharygina, N., Veith, H. (eds.) CAV 2013. LNCS, vol. 8044, pp. 740–755. Springer, Heidelberg (2013).  https://doi.org/10.1007/978-3-642-39799-8_52CrossRefGoogle Scholar
  10. 10.
    Jung, C., Clark, N.: DDT: design and evaluation of a dynamic program analysis for optimizing data structure usage. In: Microarchitecture Symposium (MICRO 2009), pp. 56–66. ACM (2009)Google Scholar
  11. 11.
    Linux kernel 4.1 Cyclic DLL (include/linux/list.h). http://www.kernel.org/. Accessed 31 Jan 2017
  12. 12.
    Marron, M., Sanchez, C., Su, Z., Fähndrich, M.: Abstracting runtime heaps for program understanding. IEEE Trans. Softw. Eng. 39(6), 774–786 (2013)CrossRefGoogle Scholar
  13. 13.
    McKeen, F., et al.: Innovative instructions and software model for isolated execution. In: Hardware and Architectural Support for Security and Privacy (HASP 2013), p. 10. ACM (2013)Google Scholar
  14. 14.
    Mohsen, M., Jacobs, B.: One step towards automatic inference of formal specifications using automated VeriFast. In: ter Beek, M.H., Gnesi, S., Knapp, A. (eds.) FMICS/AVoCS -2016. LNCS, vol. 9933, pp. 56–64. Springer, Cham (2016).  https://doi.org/10.1007/978-3-319-45943-1_4CrossRefGoogle Scholar
  15. 15.
    Mühlberg, J.T., White, D.H., Dodds, M., Lüttgen, G., Piessens, F.: Learning assertions to verify linked-list programs. In: Calinescu, R., Rumpe, B. (eds.) SEFM 2015. LNCS, vol. 9276, pp. 37–52. Springer, Cham (2015).  https://doi.org/10.1007/978-3-319-22969-0_3CrossRefGoogle Scholar
  16. 16.
    Noorman, J., et al.: Sancus 2.0: a low-cost security architecture for IoT devices. ACM Trans. Priv. Secur. 20(3), 7:1–7:33 (2017)CrossRefGoogle Scholar
  17. 17.
    Philippaerts, P., Mühlberg, J.T., Penninckx, W., Smans, J., Jacobs, B., Piessens, F.: Software verification with VeriFast: industrial case studies. Sci. Comput. Programm. 82, 77–97 (2014)CrossRefGoogle Scholar
  18. 18.
    Reynolds, J.C.: Separation logic: a logic for shared mutable data structures. In: Logic in Computer Science (LICS 2002), pp. 55–74. IEEE (2002)Google Scholar
  19. 19.
    Rupprecht, T., Chen, X., White, D.H., Boockmann, J.H., Lüttgen, G., Bos, H.: DSIbin: identifying dynamic data structures in C/C++ binaries. In: Automated Software Engineering (ASE 2017), pp. 331–341. IEEE/ACM (2017)Google Scholar
  20. 20.
    Urbina, D., Gu, Y., Caballero, J., Lin, Z.: SigPath: a memory graph based approach for program data introspection and modification. In: Kutyłowski, M., Vaidya, J. (eds.) ESORICS 2014. LNCS, vol. 8713, pp. 237–256. Springer, Cham (2014).  https://doi.org/10.1007/978-3-319-11212-1_14CrossRefGoogle Scholar
  21. 21.
    van Ginkel, N., Strackx, R., Piessens, F.: Automatically generating secure wrappers for SGX enclaves from separation logic specifications. In: Chang, B.-Y.E. (ed.) APLAS 2017. LNCS, vol. 10695, pp. 105–123. Springer, Cham (2017).  https://doi.org/10.1007/978-3-319-71237-6_6CrossRefGoogle Scholar
  22. 22.
    Vogels, F., Jacobs, B., Piessens, F., Smans, J.: Annotation inference for separation logic based verifiers. In: Bruni, R., Dingel, J. (eds.) FMOODS/FORTE -2011. LNCS, vol. 6722, pp. 319–333. Springer, Heidelberg (2011).  https://doi.org/10.1007/978-3-642-21461-5_21CrossRefGoogle Scholar
  23. 23.
    White, D.H., Lüttgen, G.: Identifying dynamic data structures by learning evolving patterns in memory. In: Piterman, N., Smolka, S.A. (eds.) TACAS 2013. LNCS, vol. 7795, pp. 354–369. Springer, Heidelberg (2013).  https://doi.org/10.1007/978-3-642-36742-7_25CrossRefGoogle Scholar
  24. 24.
    White, D.H., Rupprecht, T., Lüttgen, G.: DSI: an evidence-based approach to identify dynamic data structures in C programs. In: Software Testing and Analysis (ISSTA 2016), pp. 259–269. ACM (2016)Google Scholar
  25. 25.
    Zhu, H., Petri, G., Jagannathan, S.: Automatically learning shape specifications. In: Programming Language Design and Implementation (PLDI 2016), pp. 491–507. ACM (2016)Google Scholar

Copyright information

© Springer Nature Switzerland AG 2018

Authors and Affiliations

  • Jan H. Boockmann
    • 1
  • Gerald Lüttgen
    • 1
    Email author
  • Jan Tobias Mühlberg
    • 2
  1. 1.Software Technologies Research GroupUniversity of BambergBambergGermany
  2. 2.imec-DistriNetKU LeuvenLeuvenBelgium

Personalised recommendations