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.
Research supported by the German Research Foundation (DFG) under grant “DSI2: Learning Data Structure Behaviour from Executions of Pointer Programs” (LU 1748/4-2) and by the Research Fund KU Leuven.
This is a preview of subscription content, log in via an institution.
Buying options
Tax calculation will be finalised at checkout
Purchases are for personal use only
Learn about institutional subscriptionsReferences
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)
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)
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_7
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_4
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)
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_33
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_1
Haller, I., Slowinska, A., Bos, H.: Scalable data structure detection and classification for C/C++ binaries. Emp. Softw. Eng. 21(3), 778–810 (2016)
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_52
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)
Linux kernel 4.1 Cyclic DLL (include/linux/list.h). http://www.kernel.org/. Accessed 31 Jan 2017
Marron, M., Sanchez, C., Su, Z., Fähndrich, M.: Abstracting runtime heaps for program understanding. IEEE Trans. Softw. Eng. 39(6), 774–786 (2013)
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)
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_4
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_3
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)
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)
Reynolds, J.C.: Separation logic: a logic for shared mutable data structures. In: Logic in Computer Science (LICS 2002), pp. 55–74. IEEE (2002)
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)
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_14
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_6
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_21
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_25
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)
Zhu, H., Petri, G., Jagannathan, S.: Automatically learning shape specifications. In: Programming Language Design and Implementation (PLDI 2016), pp. 491–507. ACM (2016)
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2018 Springer Nature Switzerland AG
About this paper
Cite this paper
Boockmann, J.H., Lüttgen, G., Mühlberg, J.T. (2018). Generating Inductive Shape Predicates for Runtime Checking and Formal Verification. In: Margaria, T., Steffen, B. (eds) Leveraging Applications of Formal Methods, Verification and Validation. Verification. ISoLA 2018. Lecture Notes in Computer Science(), vol 11245. Springer, Cham. https://doi.org/10.1007/978-3-030-03421-4_5
Download citation
DOI: https://doi.org/10.1007/978-3-030-03421-4_5
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-030-03420-7
Online ISBN: 978-3-030-03421-4
eBook Packages: Computer ScienceComputer Science (R0)