License: Creative Commons Attribution 3.0 Unported license (CC BY 3.0)
When quoting this document, please refer to the following
DOI: 10.4230/OASIcs.ICCSW.2013.95
URN: urn:nbn:de:0030-drops-42770
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2013/4277/
Go to the corresponding OASIcs Volume Portal

Phan, Quoc-Sang

Self-composition by Symbolic Execution

pdf-format:
16.pdf (0.6 MB)

Abstract

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.

BibTeX - Entry

@InProceedings{phan:OASIcs:2013:4277,
  author =	{Quoc-Sang Phan},
  title =	{{Self-composition by Symbolic Execution}},
  booktitle =	{2013 Imperial College Computing Student Workshop},
  pages =	{95--102},
  series =	{OpenAccess Series in Informatics (OASIcs)},
  ISBN =	{978-3-939897-63-7},
  ISSN =	{2190-6807},
  year =	{2013},
  volume =	{35},
  editor =	{Andrew V. Jones and Nicholas Ng},
  publisher =	{Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{http://drops.dagstuhl.de/opus/volltexte/2013/4277},
  URN =		{urn:nbn:de:0030-drops-42770},
  doi =		{10.4230/OASIcs.ICCSW.2013.95},
  annote =	{Keywords: Information Flow, Symbolic Execution, Satisfiability Modulo Theories}
}

Keywords: Information Flow, Symbolic Execution, Satisfiability Modulo Theories
Collection: 2013 Imperial College Computing Student Workshop
Issue Date: 2013
Date of publication: 14.10.2013

DROPS-Home | Fulltext Search | Imprint | Privacy Published by LZI