Arvid Jakobsson
Nikolai Kosmatov
ABSTRACT
One classical approach to ensuring memory safety of C programs is based on storing block metadata in a tree-like datastructure. However it becomes relatively slow when the number of memory locations in the tree becomes high. Another solution, based on shadow memory, allows very fast constant-time access to metadata and led to development of several highly optimized tools for detection of memory safety errors. However, this solution appears to be insufficient for evaluation of complex memory-related properties of an expressive specification language.
In this work, we address memory monitoring in the context of runtime assertion checking of C programs annotated in E-ACSL, an expressive specification language offered by the FRAMA-C framework for analysis of C code. We present an original combination of a tree-based and a shadow-memory-based techniques that reconciles both the efficiency of shadow memory with the higher expressiveness of annotations whose runtime evaluation can be ensured by a tree of metadata. Shadow memory with its instant access to stored metadata is used whenever small shadow metadata suffices to evaluate required annotations, while richer metadata stored in a compact prefix tree (Patricia trie) is used for evaluation of more complex memory annotations supported by E-ACSL. This combined monitoring technique has been implemented in the runtime assertion checking tool for E-ACSL. Our initial experiments confirm that the proposed hybrid approach leads to a significant speedup with respect to an earlier implementation based on a Patricia trie alone without any loss of precision.
- P. Akritidis, M. Costa, M. Castro, and S. Hand. Baggy bounds checking: An efficient and backwards-compatible defense against out-of-bounds errors. In USENIX 2009, pages 51--66. USENIX Association, 2009. Google Scholar
Digital Library
- T. M. Austin, S. E. Breach, and G. S. Sohi. Efficient detection of all pointer and array access errors. In PLDI 1994, pages 290--301. ACM, 1994. Google ScholarDigital Library
- M. Barnett, K. R. M. Leino, and W. Schulte. The Spec# programming system: An overview. In the Construction and Analysis of Safe, Secure, and Interoperable Smart Devices, Int. Workshop (CASSIS 2004), volume 3362 of LNCS, pages 49--69. Springer, 2004. Google ScholarDigital Library
- P. Baudin, J. C. Filliâtre, T. Hubert, C. Marché, B. Monate, Y. Moy, and V. Prevosto. ACSL: ANSI/ISO C Specification Language. URL: http://frama-c.com/acsl.html.Google Scholar
- P. Baudin, A. Pacalet, J. Raguideau, D. Schoen, and N. Williams. CAVEAT: a tool for software validation. In DSN 2002, page 537. IEEE Computer Society, 2002. Google ScholarDigital Library
- Y. Cheon. A Runtime Assertion Checker for the Java Modeling Language. Iowa State Univ., 2003.Google ScholarCross Ref
- L. A. Clarke and D. S. Rosenblum. A historical perspective on runtime assertion checking in software development. ACM SIGSOFT Software Engineering Notes, 31(3):25--37, 2006. Google ScholarDigital Library
- P. Cuoq, F. Kirchner, N. Kosmatov, V. Prevosto, J. Signoles, and B. Yakobowski. Frama-C, a program analysis perspective. In SEFM 2012, volume 7504 of LNCS, pages 233--247. Springer, 2012. Google ScholarDigital Library
- M. Delahaye, N. Kosmatov, and J. Signoles. Common specification language for static and dynamic analysis of C programs. In SAC 2013, pages 1230--1235. ACM, 2013. Google ScholarDigital Library
- D. Dhurjati and V. S. Adve. Backwards-compatible array bounds checking for C with very low overhead. In ICSE 2006, pages 162--171, 2006. Google ScholarDigital Library
- M. Fähndrich, M. Barnett, and F. Logozzo. Embedded contract languages. In SAC 2010, pages 2103--2110. ACM, 2010. Google ScholarDigital Library
- J.-C. Filliâtre and C. Marché. The Why/Krakatoa/Caduceus platform for deductive program verification. In CAV 2007, volume 4590 of LNCS, pages 173--177. Springer, 2007. Google ScholarDigital Library
- R. W. M. Jones and P. H. J. Kelly. Backwards-compatible bounds checking for arrays and pointers in c programs. In the Third International Workshop on Automatic Debugging (AADEBUG 1997), pages 13--26, 1997.Google Scholar
- N. Kosmatov, G. Petiot, and J. Signoles. An optimized memory monitoring for runtime assertion checking of c programs. In RV 2013, volume 8174 of LNCS, pages 167--182. Springer, 2013.Google ScholarCross Ref
- G. T. Leavens, Y. Cheon, C. Clifton, C. Ruby, and D. R. Cok. How the design of JML accomodates both runtime assertion checking and formal verification. In FMCO 2002, volume 2852 of LNCS, pages 262--284. Springer, 2002.Google Scholar
- M. Leucker and C. Schallhart. A brief account of runtime verification. J. Log. Algebr. Program., 78(5):293--303, 2009.Google ScholarCross Ref
- B. Meyer. Object-Oriented Software Construction. Prentice-Hall, Inc., 1988. Google ScholarDigital Library
- G. C. Necula, J. Condit, M. Harren, S. McPeak, and W. Weimer. CCured: type-safe retrofitting of legacy software. ACM Trans. Program. Lang. Syst., 27(3):477--526, 2005. Google ScholarDigital Library
- N. Nethercote and J. Seward. How to shadow every byte of memory used by a program. In VEE 2007, pages 65--74. ACM, 2007. Google ScholarDigital Library
- Y. Oiwa. Implementation of the memory-safe full ANSI-C compiler. In PLDI 2009, pages 259--269. ACM, 2009. Google ScholarDigital Library
- O. Ruwase and M. S. Lam. A practical dynamic buffer overflow detector. In NDSS 2004, pages 159--169, 2004.Google Scholar
- K. Serebryany, D. Bruening, A. Potapenko, and D. Vyukov. AddressSanitizer: a fast address sanity checker. In the 2012 USENIX Annual Technical Conference (USENIX ATC 2012), pages 309--318. USENIX Association, 2012. Google ScholarDigital Library
- J. Signoles. E-ACSL: Executable ANSI/ISO C Specification Language. URL: http://frama-c.com/download/e-acsl/e-acsl.pdf.Google Scholar
- M. S. Simpson and R. Barua. MemSafe: ensuring the spatial and temporal memory safety of C at runtime. Softw., Pract. Exper., 43(1):93--128, 2013. Google ScholarDigital Library
- M. Sullivan and R. Chillarege. Software defects and their impact on system availability: A study of field failures in operating systems. In FTCS 1991, pages 2--9. IEEE Computer Society, 1991.Google ScholarCross Ref
- W. Szpankowski. Patricia tries again revisited. J. ACM, 37(4):691--711, Oct. 1990. Google ScholarDigital Library
- W. Xu, D. C. DuVarney, and R. Sekar. An efficient and backwards-compatible transformation to ensure memory safety of C programs. In FSE 2004, pages 117--126. ACM, 2004. Google ScholarDigital Library
- J. Yuan and R. Johnson. CAWDOR: compiler assisted worm defense. In SCAM 2012, pages 54--63. IEEE Computer Society, 2012. Google ScholarDigital Library
Index Terms
- Fast as a shadow, expressive as a tree: hybrid memory monitoring for C
Recommendations
Fast as a shadow, expressive as a tree
One classical approach to ensuring memory safety of C programs is based on storing block metadata in a tree-like datastructure. However it becomes relatively slow when the number of memory locations in the tree becomes high. Another solution, based on ...
Fast algorithms for computing tree LCS
The LCS of two rooted, ordered, and labeled trees F and G is the largest forest that can be obtained from both trees by deleting nodes. We present algorithms for computing tree LCS which exploit the sparsity inherent to the tree LCS problem. Assuming G ...
Shadow Stack Scratch-Pad-Memory for Low Power SoC
SEC '08: Proceedings of the 2008 Fifth IEEE International Symposium on Embedded ComputingIn many embedded system, researches focus on how to use on-chip memory, like SPM, to reduce the energy consumption generated by off-chip memory, such as SDRAM or DRAM. They put the often use instructions and important data into on-chip memory to reduce ...
Comments