Paper Info
Title
Relational abstract interpretation for the verification of 2-hypersafety properties
Abstract
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.
Year
DOI
Venue
2013
10.1145/2508859.2516721
ACM Conference on Computer and Communications Security
Keywords
Field
DocType
information flow property,relational abstract interpretation,execution language,abstract syntax tree,constructing self-compositions,tree manipulation,abstract interpretation,intricate information flow property,control flow graph,2-hypersafety property,tree distance measure,semi structured data
Semi-structured data,Information flow (information theory),Graph,Abstract interpretation,Computer science,Control flow,Theoretical computer science,Business Process Execution Language,Abstract syntax
Conference
Citations 
PageRank 
References 
10
0.47
29
Authors
3
Name
Order
Citations
PageRank
Máté Kovács1794.97
Helmut Seidl21468103.61
Bernd Finkbeiner366669.95