Team for Research in
Ubiquitous Secure Technology

Citation
Patrice Godefroid, Michael Y. Levin, David A Molnar. "Active Property Checking". EMSOFT, Association for Computing Machinery, 2008.

Abstract
Runtime property checking (as implemented in tools like Purify or Valgrind) checks whether a program execution satisfies a property. Active property checking extends runtime checking by checking whether the property is satisfied by all program executions that follow the same program path. This check is performed on a symbolic execution of the given program path using a constraint solver. If the check fails, the constraint solver generates an alternative program input triggering a new program execution that follows the same program path but exhibits a property violation. Combined with systematic dynamic test generation, which attempts to exercise all feasible paths in a program, active property checking defines a new form of dynamic software model checking (program verification). In this paper, we formalize and study active property checking. We show how static and dynamic type checking can be extended with active type checking. Then, we discuss how to implement active property checking efficiently. Finally, we discuss results of experiments with large shipped Windows applications, where active property checking was able to detect several new security-related bugs.

Electronic downloads

• http://research.microsoft.com/pubs/70464/tr-2007-91.pdf

• HTML

  Patrice Godefroid, Michael Y. Levin, David A Molnar. <a
  href="http://www.truststc.org/pubs/501.html"
  >Active Property Checking</a>, EMSOFT, Association
  for Computing Machinery, 2008.

• Plain text

  Patrice Godefroid, Michael Y. Levin, David A Molnar.
  "Active Property Checking". EMSOFT, Association
  for Computing Machinery, 2008.

• BibTeX

  @inproceedings{GodefroidLevinMolnar08_ActivePropertyChecking,
      author = {Patrice Godefroid and Michael Y. Levin and David A
                Molnar},
      title = {Active Property Checking},
      booktitle = {EMSOFT},
      organization = {Association for Computing Machinery},
      year = {2008},
      abstract = {Runtime property checking (as implemented in tools
                like Purify or Valgrind) checks whether a program
                execution satisfies a property. Active property
                checking extends runtime checking by checking
                whether the property is satisfied by all program
                executions that follow the same program path. This
                check is performed on a symbolic execution of the
                given program path using a constraint solver. If
                the check fails, the constraint solver generates
                an alternative program input triggering a new
                program execution that follows the same program
                path but exhibits a property violation. Combined
                with systematic dynamic test generation, which
                attempts to exercise all feasible paths in a
                program, active property checking defines a new
                form of dynamic software model checking (program
                verification). In this paper, we formalize and
                study active property checking. We show how static
                and dynamic type checking can be extended with
                active type checking. Then, we discuss how to
                implement active property checking efficiently.
                Finally, we discuss results of experiments with
                large shipped Windows applications, where active
                property checking was able to detect several new
                security-related bugs.},
      URL = {http://www.truststc.org/pubs/501.html}
  }
  

Posted by David A Molnar on 28 Jan 2009.
Groups: trust
For additional information, see the Publications FAQ or contact webmaster at www truststc org.