2026-08-17T00:42:53Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:4277 2024-03-06T10:29:25Z ddc:004 open_access

Self-composition by Symbolic Execution Phan, Quoc-Sang Information Flow Symbolic Execution Satisfiability Modulo Theories 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. Schloss Dagstuhl – Leibniz-Zentrum für Informatik Quoc-Sang Phan 2013 Is Part Of OASIcs, Volume 35, 2013 Imperial College Computing Student Workshop InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/OASIcs.ICCSW.2013.95 urn:nbn:de:0030-drops-42770 https://drops.dagstuhl.de/entities/document/10.4230/OASIcs.ICCSW.2013.95 eng https://creativecommons.org/licenses/by/3.0/legalcode