Skip to main content

Runtime Detection of Temporal Memory Errors

  • Conference paper
  • First Online:
Runtime Verification (RV 2017)

Part of the book series: Lecture Notes in Computer Science ((LNPSE,volume 10548))

Included in the following conference series:

Abstract

State-of-the-art memory debuggers have become efficient in detecting spatial memory errors – dereference of pointers to unallocated memory. These tools, however, cannot always detect errors arising from the use of stale pointers to valid memory (temporal memory errors). This paper presents an approach to reliable detection of temporal memory errors during a run of a program. This technique tracks allocated memory tagging allocated objects and pointers with tokens that allow to reason about their temporal properties. The technique further checks pointer dereferences and detects temporal (and spatial) memory errors before they occur. The present approach has been implemented in E-ACSL – a runtime verification tool for C programs. Experimentation with E-ACSL using TempLIST benchmark comprising small C programs seeded with temporal errors shows that the suggested technique detects temporal memory errors missed by state-of-the-art memory debuggers. Further experiments with computationally intensive runs of programs from SPEC CPU indicate that the overheads of the proposed approach are within acceptable range to be used during testing or debugging.

This work has received funding for the S3P project from French DGE and BPIFrance, and for the AnaStaSec project from the French National Research Agency (ANR, grant ANR-14-CE28-0014).

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 39.99
Price excludes VAT (USA)
  • Available as EPUB and PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Notes

  1. 1.

    Recent versions of AddressSanitizer provide experimental support for detecting stack-based temporal errors [18, 27]. However, at the time of developing the proposed approach this feature was not enabled in the mainstream version of the tool.

  2. 2.

    http://nikolai.kosmatov.free.fr/TempLIST.zip.

References

  1. Akritidis, P., Costa, M., Castro, M., Hand, S.: Baggy bounds checking: an efficient and backwards-compatible defense against out-of-bounds errors. In: Proceedings of the USENIX Security Symposium, pp. 51–66. USENIX Association, August 2009

    Google Scholar 

  2. Austin, T.M., Breach, S.E., Sohi, G.S.: Efficient detection of all pointer and array access errors. In: Proceedings of the ACM SIGPLAN Conference on Programming Language Design and Implementation, pp. 290–301. ACM, June 1994

    Google Scholar 

  3. Bruening, D., Zhao, Q.: Practical memory checking with Dr. Memory. In: Proceedings of the Annual IEEE/ACM International Symposium on Code Generation and Optimization, CGO 2011, pp. 213–223. IEEE Computer Society, Washington, DC (2011)

    Google Scholar 

  4. Delahaye, M., Kosmatov, N., Signoles, J.: Common specification language for static and dynamic analysis of C programs. In: Proceedings of the ACM Symposium on Applied Computing, pp. 1230–1235. ACM, March 2013

    Google Scholar 

  5. Dhurjati, D., Adve, V.S.: Backwards-compatible array bounds checking for C with very low overhead. In: Proceedings of the International Conference on Software Engineering, pp. 162–171. ACM, May 2006

    Google Scholar 

  6. Eigler, F.C.: Mudflap: pointer use checking for C/C++. In: Proceedings of the GCC Developers Summit, pp. 57–70, May 2003

    Google Scholar 

  7. Hastings, R., Joyce, B.: Purify: fast detection of memory leaks and access errors. In: Proceedings of the Winter USENIX Conference, pp. 125–136, January 1992

    Google Scholar 

  8. Herrmann, P., Signoles, J.: Frama-C’s annotation generator plug-in. CEA LIST, Software Safety Laboratory, Saclay, F-91191 (2016). https://frama-c.com/rte.html

  9. Jakobsson, A., Kosmatov, N., Signoles, J.: Fast as a shadow, expressive as a tree: optimized memory monitoring for C. Sci. Comput. Program. 132(Part 2), 226–246 (2016). Special Issue on Software Verification and Testing (SAC-SVT’15)

    Article  Google Scholar 

  10. Jakobsson, A., Kosmatov, N., Signoles, J.: Rester statique pour devenir plus rapide, plus précis et plus mince. In: Baelde, D., Alglave, J. (eds.) Journes Francophones des Langages Applicatifs. Le Val d’Ajol, France, January 2015

    Google Scholar 

  11. Jim, T., Morrisett, J.G., Grossman, D., Hicks, M.W., Cheney, J., Wang, Y.: Cyclone: a safe dialect of C. In: Proceedings of the General Track: 2002 USENIX Annual Technical Conference, pp. 275–288. USENIX, June 2002

    Google Scholar 

  12. Jones, R.W.M., Kelly, P.H.J.: Backwards-compatible bounds checking for arrays and pointers in C programs. In: Proceedings of the International Workshop on Automatic Debugging, pp. 13–26. Linköping University Electronic Press, September 1997

    Google Scholar 

  13. Kirchner, F., Kosmatov, N., Prevosto, V., Signoles, J., Yakobowski, B.: Frama-C: a software analysis perspective. Formal Aspects Comput. 27(3), 573–609 (2015)

    Article  MathSciNet  Google Scholar 

  14. Kwon, A., Dhawan, U., Smith, J.M., Knight Jr., F.K., DeHon, A.: Low-fat pointers: compact encoding and efficient gate-level implementation of fat pointers for spatial safety and capability-based security. In: Proceedings of the ACM SIGSAC Conference on Computer and Communications Security, pp. 721–732. ACM, November 2013

    Google Scholar 

  15. Necula, G.C., Condit, J., Harren, M., McPeak, S., Weimer, W.: CCured: type-safe retrofitting of legacy software. ACM Trans. Program. Lang. Syst. 27(3), 477–526 (2005)

    Article  Google Scholar 

  16. Nethercote, N., Seward, J.: Valgrind: a program supervision framework. Electron. Not. Theor. Comput. Sci. 89(2), 44–66 (2003)

    Article  Google Scholar 

  17. Nethercote, N., Seward, J.: Valgrind: a framework for heavyweight dynamic binary instrumentation. SIGPLAN Not. 42(6), 89–100 (2007)

    Article  Google Scholar 

  18. Potapenko, A.: AddressSanitizerUseAfterReturn (2015). https://github.com/google/sanitizers/wiki/AddressSanitizerUseAfterReturn

  19. Ruwase, O., Lam, M.S.: A practical dynamic buffer overflow detector. In: Proceedings of the Network and Distributed System Security Symposium. The Internet Society, December 2004

    Google Scholar 

  20. Serebryany, K., Bruening, D., Potapenko, A., Vyukov, D.: AddressSanitizer: a fast address sanity checker. In: Proceedings of the USENIX Annual Technical Conference, pp. 309–319. USENIX Association, June 2012

    Google Scholar 

  21. Serebryany, K., Potapenko, A., Iskhodzhanov, T., Vyukov, D.: Dynamic race detection with LLVM compiler — compile-time instrumentation for ThreadSanitizer. In: Khurshid, S., Sen, K. (eds.) RV 2011. LNCS, vol. 7186, pp. 110–114. Springer, Heidelberg (2012). doi:10.1007/978-3-642-29860-8_9

    Chapter  Google Scholar 

  22. Seward, J., Nethercote, N.: Using Valgrind to detect undefined value errors with bit-precision. In: Proceedings of the USENIX Annual Technical Conference, pp. 17–30. USENIX (2005)

    Google Scholar 

  23. SGCheck: an experimental stack and global array overrun detector. http://valgrind.org/docs/manual/sg-manual.html

  24. Simpson, M.S., Barua, R.: MemSafe: ensuring the spatial and temporal memory safety of C at runtime. Softw. Practice Exp. 43(1), 93–128 (2013)

    Article  Google Scholar 

  25. Standard Performance Evaluation Corporation: SPEC CPU (2006). http://www.spec.org/benchmarks.html

  26. Stepanov, E., Serebryany, K.: MemorySanitizer: fast detector of uninitialized memory use in C++. In: Proceedings of the Annual IEEE/ACM International Symposium on Code Generation and Optimization, pp. 46–55. IEEE Computer Society, February 2015

    Google Scholar 

  27. Stepanov, E.: AddressSanitizerUseAfterScope (2016). https://github.com/google/sanitizers/wiki/AddressSanitizerUseAfterScope

  28. Vorobyov, K., Signoles, J., Kosmatov, N.: Shadow state encoding for efficient monitoring of block-level properties. In: Proceedings of the International Symposium on Memory Management, pp. 47–58. ACM, June 2017

    Google Scholar 

Download references

Author information

Authors and Affiliations

Authors

Corresponding author

Correspondence to Kostyantyn Vorobyov .

Editor information

Editors and Affiliations

Rights and permissions

Reprints and permissions

Copyright information

© 2017 Springer International Publishing AG

About this paper

Cite this paper

Vorobyov, K., Kosmatov, N., Signoles, J., Jakobsson, A. (2017). Runtime Detection of Temporal Memory Errors. In: Lahiri, S., Reger, G. (eds) Runtime Verification. RV 2017. Lecture Notes in Computer Science(), vol 10548. Springer, Cham. https://doi.org/10.1007/978-3-319-67531-2_18

Download citation

  • DOI: https://doi.org/10.1007/978-3-319-67531-2_18

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-319-67530-5

  • Online ISBN: 978-3-319-67531-2

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics