Patrice Godefroid
Abstract
Most ACM Queue readers might think of "program verification research" as mostly theoretical with little impact on the world at large. Think again. If you are reading these lines on a PC running some form of Windows (like 93-plus percent of PC users--that is, more than a billion people), then you have been affected by this line of work--without knowing it, which is precisely the way we want it to be.
- Bhansali, S., Chen, W., De Jong, S., Edwards, A., Drinic, M. 2006. Framework for instruction-leveltracing and analysis of programs. In Second International Conference on Virtual ExecutionEnvironments. Google Scholar
Digital Library
- de Moura, L., Bjorner, N. 2008. Z3: an efficient SMT solver. In Proceedings of TACAS (Tools andAlgorithms for the Construction and Analysis of Systems), volume 4963 of Lecture Notes in ComputerScience: 337-340. Springer-Verlag. Google ScholarDigital Library
- Forrester, J. E., Miller, B. P. 2000. An empirical study of the robustness of Windows NT applicationsusing random testing. In Proceedings of the 4th Usenix Windows System Symposium, Seattle (August). Google ScholarDigital Library
- Godefroid, P., Klarlund, N., Sen, K. 2005. DART: Directed Automated Random Testing. InProceedings of PLDI (Programming Language Design and Implementation): 213-223. Google ScholarDigital Library
- Godefroid, P., Levin, M. Y., Molnar, D. 2008. Automated whitebox fuzz testing. In Proceedings ofNDSS (Network and Distributed Systems Security): 151-166.Google Scholar
- Howard, M. 2007. Lessons learned from the animated cursor security bug; http://blogs.msdn.com/sdl/archive/2007/04/26/lessons-learned-fromthe-animated-cursor-security-bug.aspx.Google Scholar
- Howard, M., Lipner, S. 2006. The Security Development Lifecycle. Microsoft Press. Google ScholarDigital Library
- Narayanasamy, S.,Wang, Z., Tigani, J., Edwards, A., Calder, B. 2007. Automatically classifyingbenign and harmful data races using replay analysis. In Programming Languages Design andImplementation (PLDI). Google ScholarDigital Library
- Sotirov, A. 2007. Windows animated cursor stack overflow vulnerability; http://www.determina.com/security.research/vulnerabilities/ani-header.html.Google Scholar
Index Terms
- SAGE: Whitebox Fuzzing for Security Testing: SAGE has had a remarkable impact at Microsoft.
Recommendations
Grammar-based whitebox fuzzing
PLDI '08: Proceedings of the 29th ACM SIGPLAN Conference on Programming Language Design and ImplementationWhitebox fuzzing is a form of automatic dynamic test generation, based on symbolic execution and constraint solving, designed for security testing of large applications. Unfortunately, the current effectiveness of whitebox fuzzing is limited when ...
Grammar-based whitebox fuzzing
PLDI '08Whitebox fuzzing is a form of automatic dynamic test generation, based on symbolic execution and constraint solving, designed for security testing of large applications. Unfortunately, the current effectiveness of whitebox fuzzing is limited when ...
KLUZZER: Whitebox Fuzzing on Top of LLVM
Automated Technology for Verification and AnalysisAbstractWhitebox fuzzing (a.k.a. concolic testing) has been shown to be an effective bug finding technique on its own as well as in combination with coverage-guided greybox fuzzing. However, there is currently a lack of whitebox fuzzers operating above ...
Comments