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).
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Notes
- 1.
- 2.
References
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
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
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)
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
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
Eigler, F.C.: Mudflap: pointer use checking for C/C++. In: Proceedings of the GCC Developers Summit, pp. 57–70, May 2003
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
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
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)
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
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
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
Kirchner, F., Kosmatov, N., Prevosto, V., Signoles, J., Yakobowski, B.: Frama-C: a software analysis perspective. Formal Aspects Comput. 27(3), 573–609 (2015)
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
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)
Nethercote, N., Seward, J.: Valgrind: a program supervision framework. Electron. Not. Theor. Comput. Sci. 89(2), 44–66 (2003)
Nethercote, N., Seward, J.: Valgrind: a framework for heavyweight dynamic binary instrumentation. SIGPLAN Not. 42(6), 89–100 (2007)
Potapenko, A.: AddressSanitizerUseAfterReturn (2015). https://github.com/google/sanitizers/wiki/AddressSanitizerUseAfterReturn
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
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
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
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)
SGCheck: an experimental stack and global array overrun detector. http://valgrind.org/docs/manual/sg-manual.html
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)
Standard Performance Evaluation Corporation: SPEC CPU (2006). http://www.spec.org/benchmarks.html
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
Stepanov, E.: AddressSanitizerUseAfterScope (2016). https://github.com/google/sanitizers/wiki/AddressSanitizerUseAfterScope
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
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights 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)