Skip to main content

Seminar:  Narrowing the gap between verification and systematic testing

Date:September 29, 2014 
Talk Title:Narrowing the gap between verification and systematic testing
Speaker:Maria Christakis, Doctoral Student at ETH Zurich
Time & Location:12:00pm - 1:00pm
CIC Building, Pittsburgh

Abstract

The first part of the talk focuses on combining static program checking with systematic testing. Many mainstream static checkers make a number of compromises to improve automation, performance, and accuracy. These compromises include not checking certain program properties as well as making implicit, unsound assumptions. Consequently, the results of such static checkers do not provide definite guarantees about program correctness, which makes it unclear which properties remain to be tested. We propose a technique for collaborative verification and testing that makes compromises of static checkers explicit such that they can be compensated for by complementary checkers or testing.

In the second part of the talk, I will present how to use systematic testing to achieve verification. In particular, I will describe how we proved memory safety of a complex Windows image parser written in low-level C in only three months of work and using only three core techniques, namely (1) symbolic execution at the x86 binary level, (2) exhaustive program path enumeration and testing, and (3) user-guided program decomposition and summarization. As a result of this work, we are able to prove, for the first time, that a Windows image parser is memory safe, that is, free of any buffer-overflow security vulnerabilities.

Speaker Bio

Maria Christakis is in her fourth year as a Ph.D. student under Peter Müller's supervision in the Department of Computer Science of ETH Zurich, Switzerland. In the summer of 2015, she will be joining CMU as a postdoctoral researcher in David Brumley's group.

Maria's work focuses on narrowing the gap between verification and systematic testing both by combining them and by using systematic testing to achieve verification. Part of this work has been done while visiting Patrice Godefroid at Microsoft Research Redmond.

Maria received her Bachelor's and Master's degrees from the National Technical University of Athens, Greece, where she also worked on static and dynamic concurrency error detection in Erlang.