Committee

  • Aarti Gupta (advisor)
  • Zak Kincaid
  • Lennart Beringer

Title

Exploiting Synchrony and Symmetry in Relational Verification

Abstract

Relational safety specifications describe multiple runs of the same program or relate the behaviors of multiple programs. Approaches to automatic relational verification often compose the programs and analyze the composition for safety, but a naively composed program can lead to difficult verification problems. In my talk, I will demonstrate two ways of exploiting relational specifications to simplify verification subtasks generated during relational verification. First, I will describe an algorithm for maximizing opportunities for synchronizing code fragments containing loops, allowing a verification procedure to avoid computing difficult loop invariants. Second, I will show how to compute symmetries in the specifications, allowing a verification procedure to avoid redundant subtasks. These enhancements have been implemented in a prototype for verifying k-safety properties on Java programs, and evaluation confirms that taking advantage of relational specifications as described leads to a consistent performance speedup on a range of benchmarks.

Reading List

Papers / Chapters

  1. Marcelo Sousa and Isil Dillig. Cartesian Hoare Logic for Verifying k-Safety Properties. PLDI'16. 2016.
  2. Gilles Barthe, Juan M. Crespo, and César Kunz. Relational Verification using Product Programs. FM'11. 2011.
  3. Fadi A. Aloul, Karem A. Sakallah, and Igor L. Markov. Efficient Symmetry Breaking for Boolean Satisfiability. IEEE Transactions on Computers 55(5). 2006.
  4. E. Allen Emerson and A. Prasad Sistla. Symmetry and model checking. Formal Methods in System Design. 1996.
  5. Gilles Barthe, Pedro R. D'Argenio, and Tamara Rezk. Secure Information Flow by Self-Composition. CSFW'04. 2004.
  6. Tachio Terauchi and Alex Aiken. Secure Information Flow as a Safety Problem. SAS'05. 2005.
  7. Kenneth L. McMillan. Lazy Annotation Revisited. CAV'14. 2014.
  8. Ranjit Jhala and Rupak Majumdar. Software model checking. CSUR'09. 2009
  9. Clark Barrett, Roberto Sebastiani, Sanjit A. Seshia, and Cesare Tinelli. Satisfiability Modulo Theories. Handbook of Satisfiability. 2009.
  10. David A. Naumann. From coupling relations to mated invariants for checking information flow. European Symposium On Research In Computer Security. 2006.

Textbooks

  1. Aaron Bradley and Zohar Manna. The Calculus of Computation: Decision Procedures with Applications to Verification. 2007.
  2. Benjamin C. Pierce. Types and Programming Languages. 2002.

Slides

They can be found here in Keynote format and here in PDF format.