Xi Wang
M. Frans Kaashoek
- Bessey, A., Block, K., Chelf, B., Chou, A., Fulton, B., Hallem, S., Henri-Gros, C., Kamsky, A., McPeak, S., Engler, D. A few billion lines of code later: Using static analysis to find bugs in the real world. Commun. ACM 53, 2 (Feb. 2010), 66--75. Google Scholar
Digital Library
- Blackshear, S., Lahiri, S. Almost-correct specifications: A modular semantic framework for assigning confidence to warnings. In Proceedings of the 2013 ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI) (Seattle, WA, Jun. 2013), 209--218. Google ScholarDigital Library
- Boehm, H.-J. Threads cannot be implemented as a library. In Proceedings of the 2005 ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI) (Chicago, IL, Jun. 2005), 261--268. Google ScholarDigital Library
- Brummayer, R., Biere, A. 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 (York, UK, Mar. 2009), 174--177. Google ScholarDigital Library
- Bug 30475 -- <code>assert(int+100 > int)</code> optimized away, 2007. http://gcc.gnu.org/bugzilla/show_bug.cgi?id=30475.Google Scholar
- Bug 14287 -- ext4: fixpoint divide exception at <code>ext4_fill_super,</code> 2009. https://bugzilla.kernel.org/show_bug.cgi?id=14287.Google Scholar
- Bug 49820 -- explicit check for integer negative after <code>abs</code> optimized away, 2011. http://gcc.gnu.org/bugzilla/show_bug.cgi?id=49820.Google Scholar
- Bug 53265 -- warn when undefined behavior implies smaller iteration count, 2013. http://gcc.gnu.org/bugzilla/show_bug.cgi?id=53265.Google Scholar
- Cadar, C., Dunbar, D., Engler, D. 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
- Canet, G., Cuoq, P., Monate, B. A value analysis for C programs. In Proceedings of the 9th IEEE International Working Conference on Source Code Analysis and Manipulation (Edmonton, Canada, Sept. 2009), 123--124. Google ScholarDigital Library
- Chen, H., Mao, Y., Wang, X., Zhou, D., Zeldovich, N., Kaashoek, M.F. Linux kernel vulnerabilities: State-of-the-art defenses and open problems. In Proceedings of the 2nd Asia-Pacific Workshop on Systems (Shanghai, China, Jul. 2011). Google ScholarDigital Library
- Clang Compiler User's Manual: Controlling Code Generation, 2014. http://clang.llvm.org/docs/UsersManual.html#controlling-code-generation.Google Scholar
- Corbet, J. Fun with NULL pointers, part 1, July 2009. http://lwn.net/Articles/342330/.Google Scholar
- Cuoq, P., Flatt, M., Regehr, J. Proposal for a friendly dialect of C, Aug. 2014. http://blog.regehr.org/archives/1180.Google Scholar
- Dietz, W., Li, P., Regehr, J., Adve, V. Understanding integer overflow in C/C++. In Proceedings of the 34th International Conference on Software Engineering (ICSE) (Zurich, Switzerland, Jun. 2012), 760--770. Google ScholarDigital Library
- Dillig, I., Dillig, T., Aiken, A. Static error detection using semantic inconsistency inference. In Proceedings of the 2007 ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI) (San Diego, CA, Jun. 2007), 435--445. Google ScholarDigital Library
- Dougherty, C.R., Seacord, R.C. C compilers may silently discard some wraparound checks. Vulnerability note VU#162289, US-CERT, 2008. http://www.kb.cert.org/vuls/id/162289, original version: http://www.isspcs.org/render.html?it=9100, also known as CVE-2008-1685.Google Scholar
- Ellison, C., Roşu, G. Defining the Undefinedness of C. Technical report, University of Illinois, Apr. 2012. http://hdl.handle.net/2142/30780.Google Scholar
- Ellison, C., Roşu, G. An executable formal semantics of C with applications. In Proceedings of the 39th ACM Symposium on Principles of Programming Languages (POPL) (Philadelphia, PA, Jan. 2012), 533--544. Google ScholarDigital Library
- Engler, D., Chen, D.Y., Hallem, S., Chou, A., Chelf, B. 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) (Chateau Lake Louise, Banff, Canada, Oct. 2001), 57--72. Google ScholarDigital Library
- Hoenicke, J., Leino, K.R.M., Podelski, A., Schäf, M., Wies, T. It's doomed; we can prove it. In Proceedings of the 16th International Symposium on Formal Methods (FM) (Eindhoven, the Netherlands, Nov. 2009), 338--353. Google ScholarDigital Library
- Intel 64 and IA-32 Architectures Software Developer's Manual, Volume 2: Instruction Set Reference, A--Z, Jan. 2013.Google Scholar
- ISO/IEC 9899:2011, Programming languages -- C, Dec. 2011.Google Scholar
- Jack, B. Vector rewrite attack: Exploitable NULL pointer vulnerabilities on ARM and XScale architectures. White paper, Juniper Networks, May 2007.Google Scholar
- Krebbers, R., Wiedijk, F. Subtleties of the ANSI/ISO C standard. Document N1639, ISO/IEC, Sept. 2012.Google Scholar
- Lane, T. Anyone for adding <code>--fwrapv</code> to our standard CFLAGS? Dec. 2005. http://www.postgresql.org/message-id/[email protected].Google Scholar
- Lattner, C. 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
- Lattner, C., Adve, V. LLVM: A compilation framework for lifelong program analysis & transformation. In Proceedings of the 2004 International Symposium on Code Generation and Optimization (CGO) (Palo Alto, CA, Mar. 2004), 75--86. Google ScholarDigital Library
- Miller, W.M. 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
- Power ISA Version 2.06 Revision B, Book I: Power ISA User Instruction Set Architecture, Jul. 2010.Google Scholar
- Ranise, S., Tinelli, C., Barrett, C. QF_BV logic, Jun. 2013. http://smtlib.cs.uiowa.edu/logics/QF_BV.smt2.Google Scholar
- Rationale for International Standard -- Programming Languages -- C, Apr. 2003.Google Scholar
- Regehr, J. A guide to undefined behavior in C and C++, Jul. 2010. http://blog.regehr.org/archives/213.Google Scholar
- Regehr, J. Undefined behavior consequences contest winners, Jul. 2012. http://blog.regehr.org/archives/767.Google Scholar
- Seacord, R.C. Dangerous optimizations and the loss of causality, Feb. 2010. https://www.securecoding.cert.org/confluence/download/attachments/40402999/Dangerous+Optimizations.pdf.Google Scholar
- Stallman, R.M., the GCC Developer Community. Using the GNU Compiler Collection for GCC 4.8.0. GNU Press, Free Software Foundation, Boston, MA, 2013.Google Scholar
- Teo, E. {PATCH} add <code>-fno-delete-null-pointer-checks</code> to gcc <code>CFLAGS</code>, Jul. 2009. https://lists.ubuntu.com/archives/kernel-team/2009-July/006609.html.Google Scholar
- Tinnes, J. Bypassing Linux NULL pointer dereference exploit prevention (<code>mmap_min_addr</code>), Jun. 2009. http://blog.cr0.org/2009/06/bypassing-linux-null-pointer.html.Google Scholar
- Tomb, A., Flanagan, C. Detecting inconsistencies via universal reachability analysis. In Proceedings of the 2012 International Symposium on Software Testing and Analysis (Minneapolis, MN, Jul. 2012), 287--297. Google ScholarDigital Library
- Torvalds, L. Re: {patch} CFS scheduler, -v8, May 2007. https://lkml.org/lkml/2007/5/7/213.Google Scholar
- Tourrilhes, J. Invalid compilation without <code>-fno-strict-aliasing</code>, Feb. 2003. https://lkml.org/lkml/2003/2/25/270.Google Scholar
- Wang, X., Chen, H., Cheung, A., Jia, Z., Zeldovich, N., Kaashoek, M.F. Undefined behavior: What happened to my code? In Proceedings of the 3rd Asia-Pacific Workshop on Systems (Seoul, South Korea, Jul. 2012). Google ScholarDigital Library
- Wang, X., Chen, H., Jia, Z., Zeldovich, N., Kaashoek, M.F. Improving integer security for systems with KINT. In Proceedings of the 10th Symposium on Operating Systems Design and Implementation (OSDI) (Hollywood, CA, Oct. 2012), 163--177. Google ScholarDigital Library
- Wang, X., Zeldovich, N., Kaashoek, M.F., Solar-Lezama, A. Towards optimization-safe systems: Analyzing the impact of undefined behavior. In Proceedings of the 24th ACM Symposium on Operating Systems Principles (SOSP) (Farmington, PA, Nov. 2013), 260--275. Google ScholarDigital Library
- Woods, J.F. Re: Why is this legal? Feb. 1992. http://groups.google.com/group/comp.std.c/msg/dfe1ef367547684b.Google Scholar
Index Terms
- A differential approach to undefined behavior detection
Recommendations
A Differential Approach to Undefined Behavior Detection
This article studies undefined behavior arising in systems programming languages such as C/C++. Undefined behavior bugs lead to unpredictable and subtle systems behavior, and their effects can be further amplified by compiler optimizations. Undefined ...
LOCATE: Locally Anomalous Behavior Change Detection in Behavior Information Sequence
Web and Big DataAbstractWith the availability of diverse data reflecting people’s behavior, behavior analysis has been studied extensively. Detecting anom-alies can improve the monitoring and understanding of the objects’ (e.g., people’s) behavior. This work considers ...
Influence of crossover on the behavior of Differential Evolution Algorithms
In Differential Evolution Algorithms the crossover operator allows the construction of a new trial element starting from the current and mutant elements. Thus it controls which and how many components are mutated in each element of the current ...
Comments