Skip to main content
Disciplines
Automotive Business IT + Informatics Construction + Real Estate Electrical Engineering + Electronics Energy + Sustainability Insurance + Risk Finance + Banking Management + Leadership Marketing + Sales Mechanical Engineering + Materials
Events
DE
EN
Books
Journals
Topic Page
Marketing
Start single access now
Access for companies
EXTENDED SEARCH
Log in
Top
International Journal on Software Tools for Technology Transfer
Published in: International Journal on Software Tools for Technology Transfer 2/2020

06-08-2019 | SPIN 2018

Joint forces for memory safety checking revisited

Authors: Marek Chalupa, Jan Strejček, Martina Vitovská

Published in: International Journal on Software Tools for Technology Transfer | Issue 2/2020

Log in

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

search-config
loading …

Abstract

We present an improved version of the memory safety verification approach implemented in Symbiotic 5, the winner of the MemSafety category at the Competition on Software Verification (SV-COMP) 2018. The approach can verify programs for standard errors in memory usage like invalid pointer dereference or memory leaking. It is based on instrumentation, static pointer analysis extended to consider memory deallocations, static program slicing, and symbolic execution. The improved version brings higher precision of the extended pointer analysis and further optimizations in instrumentation. It is implemented in the current version of Symbiotic, which contains also some improvements in program slicing and symbolic execution. We explain the approach in theory, describe implementation of selected components, and provide experimental results showing the impact of particular components.
previous article Model-based testing of apps in real network scenarios
next article IC3 software model checking

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
Footnotes
3
https://​github.​com/​sosy-lab/​sv-benchmarks/​, revision tag svcomp18 with an additional commit 514e387c that fixes a bug in one of the benchmarks.
 
4
The reader may notice a difference to the conference paper in the number of solved safe benchmarks. This difference is caused by removing a heuristic we have previously added to Klee and that turned out to be incorrect in some cases (although not on the SV-COMP benchmarks).
 
Literature
1.
Andersen, L.O.: Program Analysis and Specialization for the C Programming Language. PhD thesis, DIKU, University of Copenhagen (1994)
2.
Beyer, D., Erkan Keremoglu, M.: CPAchecker: a tool for configurable software verification. In: Computer Aided Verification—23rd International Conference, CAV 2011, Snowbird, UT, USA, July 14–20, 2011. Proceedings, volume 6806 of Lecture Notes in Computer Science, pp. 184–190. Springer (2011)
3.
Beyer, D., Henzinger, T.A., Jhala, R., Majumdar, R.: Checking memory safety with blast. In: Fundamental Approaches to Software Engineering, 8th International Conference, FASE 2005, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2005, Edinburgh, UK, April 4–8, 2005, Proceedings, volume 3442 of Lecture Notes in Computer Science, pp. 2–18. Springer (2005)
4.
Beyer, D., Löwe, S., Wendler, P.: Benchmarking and resource measurement. In: Model Checking Software—22nd International Symposium, SPIN 2015, Stellenbosch, South Africa, August 24–26, 2015, Proceedings, volume 9232 of Lecture Notes in Computer Science, pp. 160–178. Springer (2015)
5.
Cadar, C., Dunbar, D., Engler, D.R.: KLEE: unassisted and automatic generation of high-coverage tests for complex systems programs. In: 8th USENIX Symposium on Operating Systems Design and Implementation, OSDI 2008, December 8–10, 2008, San Diego, California, USA, Proceedings, pp. 209–224. USENIX Association (2008)
6.
Carter, M., He, S., Whitaker, J., Rakamarić, Z., Emmi, M.: SMACK software verification toolchain. In: Proceedings of the 38th IEEE/ACM International Conference on Software Engineering (ICSE) Companion, pp. 589–592. ACM (2016)
7.
Chalupa, M., Strejček, J., Vitovská, M.: Joint forces for memory safety checking. In: Gallardo, M.d.M., Merino, P., (Eds.), Model Checking Software—-25th International Symposium, SPIN 2018, Malaga, Spain, June 20–22, 2018, Proceedings, volume 10869 of Lecture Notes in Computer Science, pp. 115–132. Springer (2018)
8.
Chalupa, M., Vitovská, M., Strejček, J.: Symbiotic 5: boosted instrumentation (competition contribution). In: Tools and Algorithms for the Construction and Analysis of Systems—24th International Conference, TACAS 2018, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2018, Thessaloniki, Greece, April 14–20, 2018, Proceedings, Part II, volume 10806 of Lecture Notes in Computer Science, pp. 442–446. Springer (2018)
9.
Chebaro, O., Kosmatov, N., Giorgetti, A., Julliand, J.: The SANTE tool: value analysis, program slicing and test generation for C program debugging. In: Tests and Proofs—5th International Conference, TAP 2011, Zurich, Switzerland, June 30–July 1, 2011. Proceedings, volume 6706 of Lecture Notes in Computer Science, pp. 78–83. Springer (2011)
10.
Chebaro, O., Cuoq, P., Kosmatov, N., Marre, B., Pacalet, A., Williams, N., Yakobowski, B.: Behind the scenes in sante: a combination of static and dynamic analyses. Autom. Softw. Eng. 21(1), 107–143 (2014)CrossRef
11.
12.
Cytron, R., Ferrante, J., Rosen, B.K., Wegman, M.N., Kenneth Zadeck, F.: An efficient method of computing static single assignment form. In: Conference Record of the Sixteenth Annual ACM Symposium on Principles of Programming Languages, Austin, Texas, USA, January 11–13, 1989, pp. 25–35. ACM (1989)
13.
Dhurjati, D., Adve, V.: Backwards-compatible array bounds checking for C with very low overhead. In: Proceedings of the 28th International Conference on Software Engineering, ICSE ’06, pp. 162–171. ACM (2006)
14.
Dhurjati, D., Kowshik, S., Adve, V.: SAFECode: enforcing alias analysis for weakly typed languages. In PLDI ’06: Proceedings of the 2006 ACM SIGPLAN Conference on Programming Language Design and Implementation, pp. 144–157. ACM (2006)
15.
Dor, N., Rodeh, M., Sagiv, M.: Detecting memory errors via static pointer analysis (preliminary experience). In: Proceedings of the 1998 ACM SIGPLAN-SIGSOFT Workshop on Program Analysis for Software Tools and Engineering, PASTE ’98, pp. 27–34. ACM (1998)
16.
Dudka, K., Peringer, P., Vojnar, T.: Byte-precise verification of low-level list manipulation. In: Logozzo, F, Fähndrich, M. (Eds.), Static Analysis—20th International Symposium, SAS 2013, Seattle, WA, USA, June 20–22, 2013. Proceedings, volume 7935 of Lecture Notes in Computer Science, pp. 215–237. Springer (2013)
17.
Ferrante, J., Ottenstein, K.J., Warren, J.D.: The program dependence graph and its use in optimization. In: International Symposium on Programming, 6th Colloquium, Toulouse, April 17–19, 1984, Proceedings, volume 167 of Lecture Notes in Computer Science, pp. 125–132. Springer (1984)
18.
Gurfinkel, A., Kahsai, T., Komuravelli, A., Navas, J.A.: The SeaHorn verification framework. In: Computer Aided Verification—27th International Conference, CAV 2015, San Francisco, CA, USA, July 18–24, 2015, Proceedings, Part I, volume 9206 of Lecture Notes in Computer Science, pp. 343–361. Springer (2015)
19.
Guyer, S.Z., Lin, C.: Error checking with client-driven pointer analysis. Sci. Comput. Program. 58(1), 83–114 (2005)MathSciNetCrossRef
20.
Heizmann, M., Hoenicke, J., Podelski, A.: Software model checking for people who love automata. In: Computer Aided Verification—25th International Conference, CAV 2013, Saint Petersburg, Russia, July 13–19, 2013. Proceedings, volume 8044 of Lecture Notes in Computer Science, pp. 36–52. Springer (2013)
21.
Hind, M.: Pointer analysis: Haven’t we solved this problem yet? In: Proceedings of the 2001 ACM SIGPLAN–SIGSOFT Workshop on Program Analysis For Software Tools and Engineering, PASTE’01, Snowbird, Utah, USA, June 18–19, 2001, pp. 54–61. ACM (2001)
22.
Hind, M., Burke, M., Carini, P., Choi, J.-D.: Interprocedural pointer alias analysis. ACM Trans. Program. Lang. Syst. (TOPLAS) 21, 848–894 (1999)CrossRef
23.
Holík, L., Kotoun, M., Peringer, P., Šoková, V., Trtík, M., Vojnar, T.: Predator shape analysis tool suite. In: Proceedings of HVC 2016, volume 10028 of Lecture Notes in Computer Science, pp. 202–209. Springer (2016)
24.
Horwitz, S., Reps, T.W., Binkley, D.W.: Interprocedural slicing using dependence graphs. ACM Trans. Program. Lang. Syst. 12(1), 26–60 (1990)CrossRef
25.
Jones, R.W.M., Kelly, P.H.J.: Backwards-compatible bounds checking for arrays and pointers in C programs. In: AADEBUG, pp. 13–26 (1997)
26.
27.
Kroening, D., Tautschnig, Mi.: CBMC–C bounded model checker—(competition contribution). In: Tools and Algorithms for the Construction and Analysis of Systems—20th International Conference, TACAS 2014, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2014, Grenoble, France, April 5–13, 2014. Proceedings, volume 8413 of Lecture Notes in Computer Science, pp. 389–391. Springer (2014)
28.
Lattner, C., Adve, V.: LLVM: a compilation framework for lifelong program analysis & transformation. In: 2nd IEEE/ACM International Symposium on Code Generation and Optimization (CGO 2004), 20–24 March 2004, San Jose, CA, USA, CGO ’04, pp. 75–88. IEEE Computer Society (2004)
29.
Lattner, C., Adve, V.: Automatic pool allocation: improving performance by controlling data structure layout in the heap. SIGPLAN Not. 40(6), 129–142 (2005)CrossRef
30.
31.
Menezes, R., Rocha, H., Cordeiro, L.C., Barreto, R.S.: Map2check using LLVM and KLEE—(competition contribution). In: Beyer, D., Huisman, M., (Eds.), Tools and Algorithms for the Construction and Analysis of Systems—24th International Conference, TACAS 2018, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2018, Thessaloniki, Greece, April 14–20, 2018, Proceedings, Part II, volume 10806 of Lecture Notes in Computer Science, pp. 437–441. Springer (2018)
32.
Midi, D., Payer, M., Bertino, E.: Memory safety for embedded devices with nesCheck. In: Proceedings of the 2017 ACM on Asia Conference on Computer and Communications Security, ASIA CCS ’17, pp. 127–139. ACM (2017)
33.
Nagarakatte, S., Zhao, J., Martin, M.M.K., Zdancewic, S.: Softbound: highly compatible and complete spatial memory safety for c. In: Proceedings of the 30th ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI ’09, pp. 245–258. ACM (2009)
34.
Nagarakatte, S., Zhao, J., Martin, M.M.K., Zdancewic, S.: Cets: Compiler enforced temporal safety for c. SIGPLAN Not. 45(8), 31–40 (2010)
35.
Necula, G.C., McPeak, S., Weimer, W.: CCured: type-safe retrofitting of legacy code. SIGPLAN Not. 37(1), 128–139 (2002)CrossRef
36.
Nutz, A., Dietsch, D., Mohamed, M.M., Podelski, A.: ULTIMATE KOJAK with memory safety checks—(competition contribution). In: Tools and Algorithms for the Construction and Analysis of Systems—21st International Conference, TACAS 2015, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2015, London, UK, April 11–18, 2015. Proceedings, volume 9035 of Lecture Notes in Computer Science, pp. 458–460 (2015)
37.
Rinetzky, N., Sagiv, S.: Interprocedural shape analysis for recursive programs. In: Compiler Construction, 10th International Conference, CC 2001 Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2001 Genova, Italy, April 2–6, 2001, Proceedings, volume 2027 of Lecture Notes in Computer Science, pp. 133–149. Springer (2001)
38.
Rocha, H.O., Barreto, R.S., Cordeiro, L.C.: Hunting memory bugs in C programs with map2check—(competition contribution). In: Tools and Algorithms for the Construction and Analysis of Systems—22nd International Conference, TACAS 2016, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2016, Eindhoven, The Netherlands, April 2–8, 2016, Proceedings, volume 9636 of Lecture Notes in Computer Science, pp. 934–937. Springer (2016)
39.
Rodrigues, R.E., Campos, V.H.S., Pereira, F.M.Q.: A fast and low-overhead technique to secure programs against integer overflows. In: Proceedings of the 2013 IEEE/ACM International Symposium on Code Generation and Optimization, CGO 2013, Shenzhen, China, February 23–27, 2013, pp. 33:1–33:11. IEEE Computer Society (2013)
40.
Ruwase, O., Lam, M.S.: A practical dynamic buffer overflow detector. In: Proceedings of the Network and Distributed System Security Symposium, NDSS 2004, San Diego, CA, USA, pp. 159–169. The Internet Society (2004)
41.
Saeed, A., Ahmadinia, A., Just, M.: Tag-protector: an effective and dynamic detection of out-of-bound memory accesses. In: Proceedings of the Third Workshop on Cryptography and Security in Computing Systems, CS2 ’16, pp. 31–36. ACM (2016)
42.
Serebryany, K., Bruening, D., Potapenko, A., Vyukov, D.: Addresssanitizer: a fast address sanity checker. In: Proceedings of the 2012 USENIX Conference on Annual Technical Conference, USENIX ATC’12, pp. 28–28. USENIX Association (2012)
43.
44.
45.
Vitovská, M., Chalupa, M., Strejček, J.: SBT-instrumentation: a tool for configurable instrumentation of LLVM bitcode (2018). arXiv:​1810.​12617
46.
Xia, Y., Luo, J., Zhang, M.: Detecting memory access errors with flow-sensitive conditional range analysis. In: Embedded Software and Systems: Second International Conference, ICESS 2005, Xi’an, China, December 16–18, 2005. Proceedings, volume 3820 of Lecture Notes in Computer Science, pp. 320–331. Springer (2005)
47.
Yong, S.H., Horwitz, S.: Protecting C programs from attacks via invalid pointer dereferences. In: Proceedings of the 9th European Software Engineering Conference Held Jointly with 11th ACM SIGSOFT International Symposium on Foundations of Software Engineering, ESEC/FSE-11, pp. 307–316. ACM (2003)
Metadata
Title
Joint forces for memory safety checking revisited
Authors
Marek Chalupa
Jan Strejček
Martina Vitovská
Publication date
06-08-2019
Publisher
Springer Berlin Heidelberg
Published in
International Journal on Software Tools for Technology Transfer / Issue 2/2020
Print ISSN: 1433-2779
Electronic ISSN: 1433-2787
DOI
https://doi.org/10.1007/s10009-019-00526-2

Other articles of this Issue 2/2020

International Journal on Software Tools for Technology Transfer 2/2020 Go to the issue

Regular Paper

A greedy particle swarm optimization (GPSO) algorithm for testing real-world smart card applications

SPIN 2018

IC3 software model checking

Regular Paper

A formal approach to AADL model-based software engineering

Spin 2018

Counting Petri net markings from reduction equations

Introduction

Introduction to the Special Issue devoted to SPIN 2018

Regular Paper

Spatial logics and model checking for medical imaging

Premium Partner

    Image Credits