Dynamically diagnosing type errors in unsafe code

Abstract

Existing approaches for detecting type errors in unsafe languages are limited. Static analysis methods are imprecise, and often require source-level changes, while most dynamic methods check only memory properties (bounds, liveness, etc.), owing to a lack of run-time type information. This paper describes libcrunch, a system for binary-compatible run-time type checking of unmodified unsafe code, currently focusing on C. Practical experience shows that our prototype implementation is easily applicable to many real codebases without source-level modification, correctly flags programmer errors with a very low rate of false positives, offers a very low run-time overhead, and covers classes of error caught by no previously existing tool.

References

1. T. M. Austin, S. E. Breach, and G. S. Sohi. Efficient detection of all pointer and array access errors. In Proceedings of the ACM SIGPLAN 1994 Conference on Programming Language Design and Implementation, PLDI ’94, pages 290–301, New York, NY, USA, 1994. ACM.
2. G. Banavar, G. Lindstrom, and D. Orr. Type-safe composition of object modules. Technical Report UUCS-94-001, University of Utah, Salt Lake City, Utah, USA, 1994.
3. M. Burrows, S. N. Freund, and J. L. Wiener. Run-time type checking for binary programs. In CC’03: Proceedings of the 12th international conference on Compiler construction, pages 90–105, Berlin, Heidelberg, 2003. Springer-Verlag.
4. S. Chandra and T. Reps. Physical type checking for C. In Proceedings of the 1999 ACM SIGPLAN-SIGSOFT Workshop on Program Analysis for Software Tools and Engineering, PASTE ’99, pages 66–75, New York, NY, USA, 1999. ACM.
5. B. Chin, S. Markstrum, and T. Millstein. Semantic type qualifiers. In Proceedings of the 2005 ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI ’05, pages 85–95, New York, NY, USA, 2005. ACM.
6. D. Dhurjati, S. Kowshik, and V. Adve. SAFECode: Enforcing alias analysis for weakly typed languages. In Proceedings of the 2006 ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI ’06, pages 144– 157, New York, NY, USA, 2006. ACM.
7. C. Diamand, S. Kell, and D. Chisnall. Run-time type checking with clang, using libcrunch. Presented at EuroLLVM 2016, March 2016.
8. Presentation abstract, slides and video available at http://www.llvm.org/devmtg/2016-03/ as retrieved on 2016/8/26.
9. C. Ellison and G. Rosu. An executable formal semantics of C with applications. In Proceedings of the 39th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL ’12, pages 533–544, New York, NY, USA, 2012. ACM.
10. J. S. Foster, R. Johnson, J. Kodumal, and A. Aiken. Flowinsensitive type qualifiers. ACM Trans. Program. Lang. Syst., 28(6):1035–1087, Nov. 2006.
11. R. Hastings and B. Joyce. Purify: Fast detection of memory leaks and access errors. In Proc. of the Winter 1992 USENIX Conference, pages 125–138. USENIX Association, 1991.
12. ISO WG21. Programming languages — C. ISO/IEC Standard 9899:2011, Dec. 2011.
13. A non-final but recent version is available at www.open-std.org/JTC1/SC22/WG14/www/docs/n1539.pdf, retrieved on 2016/8/24.
14. T. Jim, J. G. Morrisett, D. Grossman, M. W. Hicks, J. Cheney, and Y. Wang. Cyclone: A safe dialect of C. In Proceedings of the General Track of the Annual Conference on USENIX Annual Technical Conference, ATEC ’02, pages 275–288, Berkeley, CA, USA, 2002. USENIX Association.
15. S. Kell. Towards a dynamic object model within Unix processes. In 2015 ACM International Symposium on New Ideas, New Paradigms, and Reflections on Programming and Software (Onward!), Onward! 2015, pages 224–239, New York, NY, USA, 2015. ACM.
16. R. Krebbers and F. Wiedijk. A typed C11 semantics for interactive theorem proving. In Proceedings of the 2015 Conference on Certified Programs and Proofs, CPP ’15, pages 15–27, New York, NY, USA, 2015. ACM.
17. S. Krishnamurthi and M. Felleisen. Safety in programming languages. Technical Report TR 99-352, Rice University, 1999.
18. A. Loginov, S. H. Yong, S. Horwitz, and T. W. Reps. Debugging via run-time type checking. In Proceedings of the 4th International Conference on Fundamental Approaches to Software Engineering, FASE ’01, pages 217–232, London, UK, UK, 2001. Springer-Verlag.
19. K. Memarian, J. Matthiesen, J. Lingard, K. Nienhuis, D. Chisnall, R. N. M. Watson, and P. Sewell. Into the depths of c: Elaborating the de facto standards. In Proceedings of the 37th ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI ’16, pages 1–15, New York, NY, USA, 2016. ACM.
20. S. Nagarakatte, J. Zhao, M. M. Martin, and S. Zdancewic. SoftBound: highly compatible and complete spatial memory safety for C. In Proceedings of the 2009 ACM SIGPLAN conference on Programming language design and implementation, PLDI ’09, pages 245–258, New York, NY, USA, 2009. ACM.
21. S. Nagarakatte, J. Zhao, M. M. K. Martin, and S. Zdancewic. CETS: compiler enforced temporal safety for C. In Proceedings of the 9th International Symposium on Memory Management, ISMM ’10, pages 31–40, 2010.
22. G. C. Necula, S. McPeak, S. P. Rahul, and W. Weimer. CIL: Intermediate language and tools for analysis and transformation of C programs. In R. N. Horspool, editor, Compiler Construction, volume 2304 of Lecture Notes in Computer Science, pages 213–228. Springer Berlin Heidelberg, 2002.
23. G. C. Necula, S. McPeak, and W. Weimer. CCured: Type-safe retrofitting of legacy code. In Proceedings of the 29th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL ’02, pages 128–139, New York, NY, USA, 2002. ACM.
24. M. Polishchuk, B. Liblit, and C. W. Schulze. Dynamic heap type inference for program understanding and debugging. In Proceedings of the 34th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL ’07, pages 39–46, New York, NY, USA, 2007. ACM.
25. K. Serebryany, D. Bruening, A. Potapenko, and D. Vyukov. AddressSanitizer: A fast address sanity checker. In Proceedings of the 2012 USENIX Annual Technical Conference, USENIX ATC’12, pages 28–28, Berkeley, CA, USA, 2012. USENIX Association.
26. J. Seward and N. Nethercote. Using Valgrind to detect undefined value errors with bit-precision. In ATEC ’05: Proceedings of the USENIX Annual Technical Conference, Berkeley, CA, USA, 2005. USENIX Association.
27. M. Siff, S. Chandra, T. Ball, K. Kunchithapadam, and T. Reps. Coping with type casts in C. In Proceedings of the 7th European Software Engineering Conference Held Jointly with the 7th ACM SIGSOFT International Symposium on Foundations of Software Engineering, ESEC/FSE-7, pages 180–198, London, UK, UK, 1999. Springer-Verlag.
28. P. Wilson, M. Johnstone, M. Neely, and D. Boles. Dynamic storage allocation: A survey and critical review. In Proc. International Workshop on Memory management, pages 1– 116. Springer Verlag, September 1995.
29. S. H. Yong and S. Horwitz. Reducing the overhead of dynamic analysis. Electr. Notes Theor. Comput. Sci., 70(4):158–178, 2002.
30. Q. Zhao, D. Bruening, and S. Amarasinghe. Umbra: Efficient and scalable memory shadowing. In Proceedings of the 8th Annual IEEE/ACM International Symposium on Code Generation and Optimization, CGO ’10, pages 22–31, New York, NY, USA, 2010. ACM.

Index Terms

• Software and its engineering

  • Software creation and management

    • Software verification and validation

      • Software defect analysis

        • Software testing and debugging