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.
Supplemental Material
- 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 ScholarDigital Library
- 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 ScholarDigital Library
- 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 ScholarDigital Library
- 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 ScholarDigital Library
- 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 ScholarDigital Library
- 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 ScholarDigital Library
- Chromium. Issue 12079010: Avoid undefined behavior when checking for pointer wraparound, 2013. https://codereview.chromium.org/12079010/.Google Scholar
- 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 ScholarDigital Library
- Clang. Clang Compiler User's Manual: Controlling Code Generation, 2013. http://clang.llvm.org/docs/UsersManual.html#controlling-code-generation.Google Scholar
- J. Corbet. Fun with NULL pointers, part 1, July 2009. http://lwn.net/Articles/342330/.Google Scholar
- 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 ScholarDigital Library
- 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 ScholarDigital Library
- 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 Scholar
- 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 ScholarDigital Library
- 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 Scholar
- 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 ScholarDigital Library
- GCC. Bug 30475 - assert(int+100 > int) optimized away, 2007. http://gcc.gnu.org/bugzilla/show_bug.cgi?id=30475.Google Scholar
- GCC. Bug 49820 - explicit check for integer negative after abs optimized away, 2011. http://gcc.gnu.org/bugzilla/show_bug.cgi?id=49820.Google Scholar
- GCC. Bug 53265 - warn when undefined behavior implies smaller iteration count, 2013. http://gcc.gnu.org/bugzilla/show_bug.cgi?id=53265.Google Scholar
- D. Gohman. The nsw story, Nov. 2011. http://lists.cs.uiuc.edu/pipermail/llvmdev/2011-November/045730.html.Google Scholar
- IBM. Power ISA Version 2.06 Revision B, Book I: Power ISA User Instruction Set Architecture, July 2010.Google Scholar
- Intel. Intel 64 and IA-32 Architectures Software Developer's Manual, Volume 2: Instruction Set Reference, A--Z, Jan. 2013.Google Scholar
- ISO/IEC JTC1/SC22/WG14. Rationale for International Standard - Programming Languages - C, Apr. 2003.Google Scholar
- ISO/IEC JTC1/SC22/WG14. ISO/IEC 9899:2011, Programming languages - C, Dec. 2011.Google Scholar
- B. Jack. Vector rewrite attack: Exploitable NULL pointer vulnerabilities on ARM and XScale architectures. White paper, Juniper Networks, May 2007.Google Scholar
- R. Krebbers and F. Wiedijk. Subtleties of the ANSI/ISO C standard. Document N1639, ISO/IEC JTC1/SC22/WG14, Sept. 2012.Google Scholar
- T. Lane. Anyone for adding -fwrapv to our standard CFLAGS?, Dec. 2005. http://www.postgresql.org/message-id/[email protected].Google Scholar
- T. Lane. Re: gcc versus division-by-zero traps, Sept. 2009. http://www.postgresql.org/message-id/[email protected].Google Scholar
- 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 Scholar
- 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 ScholarDigital Library
- Linux kernel. Bug 14287 - ext4: fixpoint divide exception at ext4_fill_super, 2009. https://bugzilla.kernel.org/show_bug.cgi?id=14287.Google Scholar
- D. MacKenzie, B. Elliston, and A. Demaille. Auto-conf: Creating Automatic Configuration Scripts for version 2.69. Free Software Foundation, Apr. 2012.Google Scholar
- 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 Scholar
- B. Momjian. Re: Fix for Win32 division involving INT_MIN, June 2006. http://www.postgresql.org/message-id/[email protected].Google Scholar
- S. S. Muchnick. Advanced Compiler Design and Implementation. Morgan Kaufmann, 1997. Google ScholarDigital Library
- 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 Scholar
- Python. Issue 17016: _sre: avoid relying on pointer overflow, 2013. http://bugs.python.org/issue17016.Google Scholar
- S. Ranise, C. Tinelli, and C. Barrett. QF_BV logic, 2013. http://smtlib.cs.uiowa.edu/logics/QF_BV.smt2.Google Scholar
- J. Regehr. A guide to undefined behavior in C and C++, July 2010. http://blog.regehr.org/archives/213.Google Scholar
- J. Regehr. Undefined behavior consequences contest winners, July 2012. http://blog.regehr.org/archives/767.Google Scholar
- 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 Scholar
- R. M. Stallman and the GCC Developer Community. Using the GNU Compiler Collection for GCC 4.8.0. Free Software Foundation, 2013.Google Scholar
- 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 ScholarDigital Library
- 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 Scholar
- 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 Scholar
- L. Torvalds. Re: {patch} CFS scheduler, -v8, May 2007. https://lkml.org/lkml/2007/5/7/213.Google Scholar
- J. Tourrilhes. Invalid compilation without -fno-strict-aliasing, Feb. 2003. https://lkml.org/lkml/2003/2/25/270.Google Scholar
- 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 ScholarDigital Library
- 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 ScholarDigital Library
- 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 ScholarDigital Library
- 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 ScholarDigital Library
- 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 ScholarDigital Library
Towards optimization-safe systems: analyzing the impact of undefined behavior
Recommendations
Hybrid particle swarm optimisation with mutation for code smell detection
Code smells are characterised as the structural defects in the software which indicate a poor software design and in turn makes the software hard to maintain. However, detecting and fixing the code smell in the software is a time consuming process, and ...
Towards a live, moldable code editor
Programming '17: Companion Proceedings of the 1st International Conference on the Art, Science, and Engineering of ProgrammingCreating and evolving object-oriented applications requires developers to reason about source code and run-time state. Integrated development environments (IDEs) are tools that support developers in this activity. Many mainstream IDEs, however, focus on ...
Towards the Definition of Patterns and Code Smells for Multi-language Systems
EuroPLoP '20: Proceedings of the European Conference on Pattern Languages of Programs 2020Developers often combine multiple programming languages to build large-scale applications. They choose programming languages properly for their tasks at hand instead of solving all of their problems with a single language. Foreign Functions Interface ...
Comments