skip to main content
10.1145/2517349.2522728acmconferencesArticle/Chapter ViewAbstractPublication PagessospConference Proceedingsconference-collections
research-article
Open Access

Towards optimization-safe systems: analyzing the impact of undefined behavior

Published:03 November 2013Publication History

ABSTRACT

This paper studies an emerging class of software bugs called optimization-unstable code: code that is unexpectedly discarded by compiler optimizations due to undefined behavior in the program. Unstable code is present in many systems, including the Linux kernel and the Postgres database. The consequences of unstable code range from incorrect functionality to missing security checks.

To reason about unstable code, this paper proposes a novel model, which views unstable code in terms of optimizations that leverage undefined behavior. Using this model, we introduce a new static checker called Stack that precisely identifies unstable code. Applying Stack to widely used systems has uncovered 160 new bugs that have been confirmed and fixed by developers.

Skip Supplemental Material Section

Supplemental Material

d2-04-xi-wang.mp4

References

  1. A. Belay, A. Bittau, A. Mashtizadeh, D. Terei, D. Mazières, and C. Kozyrakis. Dune: Safe user-level access to privileged CPU features. In Proceedings of the 10th Symposium on Operating Systems Design and Implementation (OSDI), pages 335--348, Hollywood, CA, Oct. 2012. Google ScholarGoogle ScholarDigital LibraryDigital Library
  2. H.-J. Boehm. Threads cannot be implemented as a library. In Proceedings of the 2005 ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI), pages 261--268, Chicago, IL, June 2005. Google ScholarGoogle ScholarDigital LibraryDigital Library
  3. R. Brummayer and A. Biere. Boolector: An efficient SMT solver for bit-vectors and arrays. In Proceedings of the 15th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, pages 174--177, York, UK, Mar. 2009. Google ScholarGoogle ScholarDigital LibraryDigital Library
  4. C. Cadar, D. Dunbar, and D. Engler. KLEE: Unassisted and automatic generation of high-coverage tests for complex systems programs. In Proceedings of the 8th Symposium on Operating Systems Design and Implementation (OSDI), San Diego, CA, Dec. 2008. Google ScholarGoogle ScholarDigital LibraryDigital Library
  5. G. Canet, P. Cuoq, and B. Monate. A value analysis for C programs. In Proceedings of the 9th IEEE International Working Conference on Source Code Analysis and Manipulation, pages 123--124, Edmonton, Canada, Sept. 2009. Google ScholarGoogle ScholarDigital LibraryDigital Library
  6. H. Chen, Y. Mao, X. Wang, D. Zhou, N. Zeldovich, and M. F. Kaashoek. Linux kernel vulnerabilities: State-of-the-art defenses and open problems. In Proceedings of the 2nd Asia-Pacific Workshop on Systems, Shanghai, China, July 2011. Google ScholarGoogle ScholarDigital LibraryDigital Library
  7. Chromium. Issue 12079010: Avoid undefined behavior when checking for pointer wraparound, 2013. https://codereview.chromium.org/12079010/.Google ScholarGoogle Scholar
  8. A. Cimatti, A. Griggio, and R. Sebastiani. Computing small unsatisfiable cores in satisfiability modulo theories. Journal of Artificial Intelligence Research, 40:701--728, 2011. Google ScholarGoogle ScholarDigital LibraryDigital Library
  9. Clang. Clang Compiler User's Manual: Controlling Code Generation, 2013. http://clang.llvm.org/docs/UsersManual.html#controlling-code-generation.Google ScholarGoogle Scholar
  10. J. Corbet. Fun with NULL pointers, part 1, July 2009. http://lwn.net/Articles/342330/.Google ScholarGoogle Scholar
  11. W. Dietz, P. Li, J. Regehr, and V. Adve. Understanding integer overflow in C/C++. In Proceedings of the 34th International Conference on Software Engineering (ICSE), pages 760--770, Zurich, Switzerland, June 2012. Google ScholarGoogle ScholarDigital LibraryDigital Library
  12. I. Dillig, T. Dillig, and A. Aiken. Static error detection using semantic inconsistency inference. In Proceedings of the 2007 ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI), pages 435--445, San Diego, CA, June 2007. Google ScholarGoogle ScholarDigital LibraryDigital Library
  13. C. R. Dougherty and R. C. Seacord. C compilers may silently discard some wraparound checks. Vulnerability Note VU#162289, US-CERT, 2008. http://www.kb.cert.org/vuls/id/162289.Google ScholarGoogle Scholar
  14. C. Ellison and G. Roşu. An executable formal semantics of C with applications. In Proceedings of the 39th ACM Symposium on Principles of Programming Languages (POPL), pages 533--544, Philadelphia, PA, Jan. 2012. Google ScholarGoogle ScholarDigital LibraryDigital Library
  15. C. Ellison and G. Roşu. Defining the undefinedness of C. Technical report, University of Illinois, Apr. 2012. http://hdl.handle.net/2142/30780.Google ScholarGoogle Scholar
  16. D. Engler, D. Y. Chen, S. Hallem, A. Chou, and B. Chelf. Bugs as deviant behavior: A general approach to inferring errors in systems code. In Proceedings of the 18th ACM Symposium on Operating Systems Principles (SOSP), pages 57--72, Chateau Lake Louise, Banff, Canada, Oct. 2001. Google ScholarGoogle ScholarDigital LibraryDigital Library
  17. GCC. Bug 30475 - assert(int+100 > int) optimized away, 2007. http://gcc.gnu.org/bugzilla/show_bug.cgi?id=30475.Google ScholarGoogle Scholar
  18. GCC. Bug 49820 - explicit check for integer negative after abs optimized away, 2011. http://gcc.gnu.org/bugzilla/show_bug.cgi?id=49820.Google ScholarGoogle Scholar
  19. GCC. Bug 53265 - warn when undefined behavior implies smaller iteration count, 2013. http://gcc.gnu.org/bugzilla/show_bug.cgi?id=53265.Google ScholarGoogle Scholar
  20. D. Gohman. The nsw story, Nov. 2011. http://lists.cs.uiuc.edu/pipermail/llvmdev/2011-November/045730.html.Google ScholarGoogle Scholar
  21. IBM. Power ISA Version 2.06 Revision B, Book I: Power ISA User Instruction Set Architecture, July 2010.Google ScholarGoogle Scholar
  22. Intel. Intel 64 and IA-32 Architectures Software Developer's Manual, Volume 2: Instruction Set Reference, A--Z, Jan. 2013.Google ScholarGoogle Scholar
  23. ISO/IEC JTC1/SC22/WG14. Rationale for International Standard - Programming Languages - C, Apr. 2003.Google ScholarGoogle Scholar
  24. ISO/IEC JTC1/SC22/WG14. ISO/IEC 9899:2011, Programming languages - C, Dec. 2011.Google ScholarGoogle Scholar
  25. B. Jack. Vector rewrite attack: Exploitable NULL pointer vulnerabilities on ARM and XScale architectures. White paper, Juniper Networks, May 2007.Google ScholarGoogle Scholar
  26. R. Krebbers and F. Wiedijk. Subtleties of the ANSI/ISO C standard. Document N1639, ISO/IEC JTC1/SC22/WG14, Sept. 2012.Google ScholarGoogle Scholar
  27. T. Lane. Anyone for adding -fwrapv to our standard CFLAGS?, Dec. 2005. http://www.postgresql.org/message-id/[email protected].Google ScholarGoogle Scholar
  28. T. Lane. Re: gcc versus division-by-zero traps, Sept. 2009. http://www.postgresql.org/message-id/[email protected].Google ScholarGoogle Scholar
  29. C. Lattner. What every C programmer should know about undefined behavior, May 2011. http://blog.llvm.org/2011/05/what-every-c-programmer-should-know.html.Google ScholarGoogle Scholar
  30. C. Lattner and V. Adve. LLVM: A compilation framework for lifelong program analysis & transformation. In Proceedings of the 2004 International Symposium on Code Generation and Optimization (CGO), pages 75--86, Palo Alto, CA, Mar. 2004. Google ScholarGoogle ScholarDigital LibraryDigital Library
  31. Linux kernel. Bug 14287 - ext4: fixpoint divide exception at ext4_fill_super, 2009. https://bugzilla.kernel.org/show_bug.cgi?id=14287.Google ScholarGoogle Scholar
  32. D. MacKenzie, B. Elliston, and A. Demaille. Auto-conf: Creating Automatic Configuration Scripts for version 2.69. Free Software Foundation, Apr. 2012.Google ScholarGoogle Scholar
  33. W. M. Miller. C++ standard core language defect reports and accepted issues, issue 1457: Undefined behavior in left-shift, Feb. 2012. http://www.open-std.org/jtc1/sc22/wg21/docs/cwg_defects.html#1457.Google ScholarGoogle Scholar
  34. B. Momjian. Re: Fix for Win32 division involving INT_MIN, June 2006. http://www.postgresql.org/message-id/[email protected].Google ScholarGoogle Scholar
  35. S. S. Muchnick. Advanced Compiler Design and Implementation. Morgan Kaufmann, 1997. Google ScholarGoogle ScholarDigital LibraryDigital Library
  36. D. Novillo. A propagation engine for GCC. In Proceedings of the 2005 GCC & GNU Toolchain Developers' Summit, pages 175--184, Ottawa, Canada, June 2005.Google ScholarGoogle Scholar
  37. Python. Issue 17016: _sre: avoid relying on pointer overflow, 2013. http://bugs.python.org/issue17016.Google ScholarGoogle Scholar
  38. S. Ranise, C. Tinelli, and C. Barrett. QF_BV logic, 2013. http://smtlib.cs.uiowa.edu/logics/QF_BV.smt2.Google ScholarGoogle Scholar
  39. J. Regehr. A guide to undefined behavior in C and C++, July 2010. http://blog.regehr.org/archives/213.Google ScholarGoogle Scholar
  40. J. Regehr. Undefined behavior consequences contest winners, July 2012. http://blog.regehr.org/archives/767.Google ScholarGoogle Scholar
  41. R. C. Seacord. Dangerous optimizations and the loss of causality, Feb. 2010. https://www.securecoding.cert.org/confluence/download/attachments/40402999/Dangerous+Optimizations.pdf.Google ScholarGoogle Scholar
  42. R. M. Stallman and the GCC Developer Community. Using the GNU Compiler Collection for GCC 4.8.0. Free Software Foundation, 2013.Google ScholarGoogle Scholar
  43. M. Stephenson, J. Babb, and S. Amarasinghe. Bitwidth analysis with application to silicon compilation. In Proceedings of the 2000 ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI), pages 108--120, Vancouver, Canada, June 2000. Google ScholarGoogle ScholarDigital LibraryDigital Library
  44. E. Teo. {PATCH} add -fno-delete-null-pointer-checks to gcc CFLAGS, July 2009. https://lists.ubuntu.com/archives/kernel-team/2009-July/006609.html.Google ScholarGoogle Scholar
  45. J. Tinnes. Bypassing Linux NULL pointer dereference exploit prevention (mmap_min_addr), June 2009. http://blog.cr0.org/2009/06/bypassing-linux-null-pointer.html.Google ScholarGoogle Scholar
  46. L. Torvalds. Re: {patch} CFS scheduler, -v8, May 2007. https://lkml.org/lkml/2007/5/7/213.Google ScholarGoogle Scholar
  47. J. Tourrilhes. Invalid compilation without -fno-strict-aliasing, Feb. 2003. https://lkml.org/lkml/2003/2/25/270.Google ScholarGoogle Scholar
  48. P. Tu and D. Padua. Gated SSA-based demand-driven symbolic analysis for parallelizing compilers. In Proceedings of the 9th ACM International Conference on Supercomputing, pages 414--423, Barcelona, Spain, July 1995. Google ScholarGoogle ScholarDigital LibraryDigital Library
  49. X. Wang, H. Chen, A. Cheung, Z. Jia, N. Zeldovich, and M. F. Kaashoek. Undefined behavior: What happened to my code? In Proceedings of the 3rd Asia-Pacific Workshop on Systems, Seoul, South Korea, July 2012. Google ScholarGoogle ScholarDigital LibraryDigital Library
  50. X. Wang, H. Chen, Z. Jia, N. Zeldovich, and M. F. Kaashoek. Improving integer security for systems with Kint. In Proceedings of the 10th Symposium on Operating Systems Design and Implementation (OSDI), pages 163--177, Hollywood, CA, Oct. 2012. Google ScholarGoogle ScholarDigital LibraryDigital Library
  51. K. Winstein and H. Balakrishnan. Mosh: An interactive remote shell for mobile clients. In Proceedings of the 2012 USENIX Annual Technical Conference, pages 177--182, Boston, MA, June 2012. Google ScholarGoogle ScholarDigital LibraryDigital Library
  52. N. Zeldovich, S. Boyd-Wickizer, E. Kohler, and D. Mazières. Making information flow explicit in HiStar. In Proceedings of the 7th Symposium on Operating Systems Design and Implementation (OSDI), pages 263--278, Seattle, WA, Nov. 2006. Google ScholarGoogle ScholarDigital LibraryDigital Library
  1. Towards optimization-safe systems: analyzing the impact of undefined behavior

      Recommendations

      Comments

      Login options

      Check if you have access through your login credentials or your institution to get full access on this article.

      Sign in
      • Published in

        cover image ACM Conferences
        SOSP '13: Proceedings of the Twenty-Fourth ACM Symposium on Operating Systems Principles
        November 2013
        498 pages
        ISBN:9781450323888
        DOI:10.1145/2517349

        Copyright © 2013 Owner/Author

        Permission to make digital or hard copies of part or all of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for third-party components of this work must be honored. For all other uses, contact the Owner/Author.

        Publisher

        Association for Computing Machinery

        New York, NY, United States

        Publication History

        • Published: 3 November 2013

        Check for updates

        Qualifiers

        • research-article

        Acceptance Rates

        Overall Acceptance Rate131of716submissions,18%

        Upcoming Conference

        SOSP '24

      PDF Format

      View or Download as a PDF file.

      PDF

      eReader

      View online with eReader.

      eReader