Self-composition by Symbolic Execution
View/ Open
Series
OASIcs: OpenAccess Series in Informatics
Volume
35
Pagination
95 - 102 (7)
Publisher
Publisher URL
ISBN-13
978-3-939897-63-7
DOI
10.4230/OASIcs.ICCSW.2013.95
ISSN
2190-6807
Metadata
Show full item recordAbstract
Self-composition is a logical formulation of non-interference, a high-level security property that guarantees the absence of illicit information leakages through executing programs. In order to capture program executions, self-composition has been expressed in Hoare or modal logic, and has been proved (or refuted) by using theorem provers. These approaches require considerable user interaction, and verification expertise. This paper presents an automated technique to prove self-composition. We reformulate the idea of self-composition into comparing pairs of symbolic paths of the same program; the symbolic paths are given by Symbolic Execution. The result of our analysis is a logical formula expressing self-composition in first-order theories, which can be solved by off-the-shelf Satisfiability Modulo Theories solvers