TY - GEN
T1 - Relational abstract interpretation for the verification of 2-hypersafety properties
AU - Kovács, Máté
AU - Seidl, Helmut
AU - Finkbeiner, Bernd
PY - 2013
Y1 - 2013
N2 - 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.
AB - 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.
KW - abstract interpretation
KW - hyperproperties
KW - information flow control
KW - semi-structured data
UR - http://www.scopus.com/inward/record.url?scp=84889037353&partnerID=8YFLogxK
U2 - 10.1145/2508859.2516721
DO - 10.1145/2508859.2516721
M3 - Conference contribution
AN - SCOPUS:84889037353
SN - 9781450324779
T3 - Proceedings of the ACM Conference on Computer and Communications Security
SP - 211
EP - 222
BT - CCS 2013 - Proceedings of the 2013 ACM SIGSAC Conference on Computer and Communications Security
T2 - 2013 ACM SIGSAC Conference on Computer and Communications Security, CCS 2013
Y2 - 4 November 2013 through 8 November 2013
ER -