Show simple item record

dc.contributor.authorPhan, Q-Sen_US
dc.date.accessioned2014-09-16T09:04:45Z
dc.date.issued2013en_US
dc.identifier.isbn978-3-939897-63-7en_US
dc.identifier.issn2190-6807en_US
dc.identifier.urihttp://qmro.qmul.ac.uk/xmlui/handle/123456789/6121
dc.descriptionThis work is licensed under a CC-BY Creative Commons Attribution 3.0 Unported license (http://creativecommons.org/licenses/by/3.0/)
dc.descriptionurn: urn:nbn:de:0030-drops-42770
dc.descriptionurn: urn:nbn:de:0030-drops-42770en_US
dc.description.abstractSelf-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 solversen_US
dc.format.extent95 - 102 (7)en_US
dc.publisherSchloss Dagstuhl–Leibniz-Zentrum fuer Informatiken_US
dc.relation.ispartofseriesOASIcs: OpenAccess Series in Informatics
dc.subjectinformation flowen_US
dc.subjectsymbolic executionen_US
dc.subjectSatisfiability Modulo Theoriesen_US
dc.titleSelf-composition by Symbolic Executionen_US
dc.typeConference Proceeding
dc.rights.holderQuoc-Sang Phan
dc.identifier.doi10.4230/OASIcs.ICCSW.2013.95en_US
pubs.notesNot knownen_US
pubs.organisational-group/Queen Mary University of London
pubs.organisational-group/Queen Mary University of London/Faculty of Science & Engineering
pubs.organisational-group/Queen Mary University of London/Faculty of Science & Engineering/Electronic Engineering and Computer Science - Computer Science - Research Students
pubs.organisational-group/Queen Mary University of London/Faculty Reporting - Research Students
pubs.organisational-group/Queen Mary University of London/Faculty Reporting - Research Students/Faculty of Science & Engineering PGRs
pubs.publication-statusPublisheden_US
pubs.publisher-urlhttp://drops.dagstuhl.de/opus/volltexte/2013/4277en_US
pubs.volume35en_US


Files in this item

Thumbnail

This item appears in the following Collection(s)

Show simple item record