IC Colloquium: Dynamic Software Model Checking for Security
Event details
| Date | 15.10.2018 |
| Hour | 16:15 › 17:30 |
| Location | |
| Category | Conferences - Seminars |
By: Patrice Godefroid - Microsoft Research
Video of his talk
Abstract:
Dynamic software model checking consists of adapting model checking into a form of systematic testing that is applicable to industrial-size software. Over the last two decades, dozens of tools following this paradigm have been developed for checking concurrent and data-driven software. In this talk, I will discuss dynamic software model checking, its strengths and limitations, and applications. In particular, I will highlight the impact of this approach at Microsoft, including how it inspired the whitebox fuzzer SAGE which found roughly one third of all the bugs discovered by file fuzzing during the development of Microsoft's Windows 7 (saving millions of dollars by avoiding expensive security patches to nearly a billion PCs), why security testing is today the largest application of SMT solvers as measured by computational usage, and how these techniques are powering "Microsoft Security Risk Detection", the first commercial cloud fuzzing service (Fuzzing-as-a-Service). I will conclude with a discussion of future research directions.
Bio:
Patrice Godefroid is a Principal Researcher at Microsoft Research. He received a B.S. degree in Electrical Engineering (Computer Science elective) and a Ph.D. degree in Computer Science from the University of Liege, Belgium, in 1989 and 1994 respectively. From 1994 to 2006, he worked at AT&T/Lucent Bell Laboratories, where he was promoted to "distinguished member of technical staff" in 2001. His research interests include program specification, analysis, testing and verification.
More information
Video of his talk
Abstract:
Dynamic software model checking consists of adapting model checking into a form of systematic testing that is applicable to industrial-size software. Over the last two decades, dozens of tools following this paradigm have been developed for checking concurrent and data-driven software. In this talk, I will discuss dynamic software model checking, its strengths and limitations, and applications. In particular, I will highlight the impact of this approach at Microsoft, including how it inspired the whitebox fuzzer SAGE which found roughly one third of all the bugs discovered by file fuzzing during the development of Microsoft's Windows 7 (saving millions of dollars by avoiding expensive security patches to nearly a billion PCs), why security testing is today the largest application of SMT solvers as measured by computational usage, and how these techniques are powering "Microsoft Security Risk Detection", the first commercial cloud fuzzing service (Fuzzing-as-a-Service). I will conclude with a discussion of future research directions.
Bio:
Patrice Godefroid is a Principal Researcher at Microsoft Research. He received a B.S. degree in Electrical Engineering (Computer Science elective) and a Ph.D. degree in Computer Science from the University of Liege, Belgium, in 1989 and 1994 respectively. From 1994 to 2006, he worked at AT&T/Lucent Bell Laboratories, where he was promoted to "distinguished member of technical staff" in 2001. His research interests include program specification, analysis, testing and verification.
More information
Practical information
- General public
- Free
- This event is internal
Contact
- Host: George Candea