Author name cluster

Patrice Godefroid

Possible papers associated with this exact author name in Arrow. This page groups case-insensitive exact name matches and is not a full identity disambiguation profile.

3 papers

2 author rows

Highlights Conference 2013 Conference Abstract

Invited talk: 500 Machine-years of software model checking and SMT solving

Patrice Godefroid

I will report on our experience running SAGE for over 500-machine years in Microsoft's security testing labs. SAGE is a whitebox fuzzing tool for security testing. It performs symbolic execution dynamically at the binary (x86) level, generates constraints on program inputs, and solves those constraints with an SMT solver in order to generate new inputs to exercize previously uncovered program paths or trigger security vulnerabilities (like buffer overflows). This process is repeated using novel state-space exploration techniques that attempt to sweep through all (in practice, many) feasible execution paths of the program while checking simultaneously many properties. This approach thus combines program analysis, testing, model checking and automated theorem proving (constraint solving). Since 2009, SAGE has been running 24/7 on average 100+ machines automatically ``fuzzing'' hundreds of applications. This is the largest computational usage ever for any SMT solver, with over 4 billion constraints processed to date. In the process, SAGE found many new security vulnerabilities (missed by blackbox fuzzing and static program analysis) and was credited to have 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. In this talk, I will present the SAGE project, highlight connections with program verification, and discuss open research challenges. This is joint work with Michael Levin, David Molnar, Ella Bounimova, and other contributors. 09: 50 10: 00 Break

PDF Details

TIME Conference 2005 Invited Paper

Generalized Model Checking

Patrice Godefroid

Three-valued models, in which properties of a system are either true, false or unknown, have recently been advocated as a better representation for reactive program abstractions generated by automatic techniques such as predicate abstraction. Indeed, for the same cost, model checking three-valued abstractions (also called may/must abstractions) can be used to both prove and disprove any temporal-logic property, whereas traditional conservative abstractions can only prove universal properties. Also, verification results can be more precise with generalized model checking, which checks whether there exists a concretization of an abstraction satisfying a temporal-logic formula. Generalized model checking generalizes both model checking (when the model is complete) and satisfiability (when everything in the model is unknown), probably the two most studied problems related to temporal logic and verification. In this talk, the main ideas behind this framework, namely models for three-valued abstractions, completeness preorders (to measure the level of completeness of such models), three-valued temporal logics and generalized model checking was presented. The algorithms and complexity bounds for three-valued model checking and generalized model-checking for various temporal logics, was also discussed. The applications to program verification via automatic abstraction, was then discussed. Examples of programs and properties that can be verified by generalized model checking but not with current abstraction-based verification tools, was shown. Classes of temporal-logic formulas for which model checking is guaranteed to always have the same precision as generalized model checking, was also presented. The final topic is a brief discussion of three-valued abstractions for reasoning about open systems and about games in general, as well as completeness issues (i. e. , given an infinite-state program and a property, is there a finite-state abstraction of that program that satisfies this property?).

Details

AAAI Conference 1991 Conference Paper

An Efficient Reactive Planner for Synthesizing Reactive Plans

Patrice Godefroid

We present a nonlinear forward-search method suitable for planning the reactions of an agent operating in a highly unpredictable environment, . We show that this method is more efficient than existing linear methods. We then introduce the notion of safety and liveness rules. This makes possible a sharper exploitation of the information retrieved when exploring the future of the agent.

PDF Details