Reactive Systems Group

Relational Abstract Interpretation for the Verification of 2-Hypersafety Properties

Máté Kovács, Helmut Seidl and Bernd Finkbeiner

PDF BIB

@inproceedings{CCS13,
  author    = {M{\'a}t{\'e} Kov{\'a}cs and
               Helmut Seidl and
               Bernd Finkbeiner},
  title     = {Relational abstract interpretation for the verification
               of 2-hypersafety properties},
  booktitle = {20th ACM Conference on Computer and Communications Security (CCS 2013)},
  year      = {2013},
  pages     = {211-222},
  ee        = {http://doi.acm.org/10.1145/2508859.2516721},
  crossref  = {DBLP:conf/ccs/2013},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}

@proceedings{DBLP:conf/ccs/2013,
  editor    = {Ahmad-Reza Sadeghi and
               Virgil D. Gligor and
               Moti Yung},
  title     = {2013 ACM SIGSAC Conference on Computer and Communications
               Security, CCS'13, Berlin, Germany, November 4-8, 2013},
  publisher = {ACM},
  year      = {2013},
  isbn      = {978-1-4503-2477-9},
  ee        = {http://dl.acm.org/citation.cfm?id=2508859, http://dl.acm.org/citation.cfm?id=2541806},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}

Information flow properties of programs can be formalized as hyperproperties specifying the relation of multiple executions. In this paper, we therefore introduce a framework for proving 2-hypersafety properties by means of abstract interpretation. The main idea is to apply abstract interpretation on the self-compositions of the control flow graphs of programs. As a result, our method is inherently capable of analyzing relational properties of even dissimilar programs. Constructing self-compositions of control flow graphs is nontrivial. Therefore, we present an algorithm for constructing quality self-compositions driven by a tree distance measure between the abstract syntax trees of subprograms. Finally, we demonstrate the applicability of the approach by proving intricate information flow properties of programs written in a simple language for tree manipulation motivated by the Web Services Business Process Execution Language.

20th ACM Conference on Computer and Communications Security