ENCOVER: Symbolic Exploration for Information Flow Security
2012 (English)In: 2012 IEEE 25th Computer Security Foundations Symposium (CSF), IEEE , 2012, 30-44 p.Conference paper (Refereed)
We address the problem of program verification for information flow policies by means of symbolic execution and model checking. Noninterference-like security policies are formalized using epistemic logic. We show how the policies can be accurately verified using a combination of concolic testing and SMT solving. As we demonstrate, many scenarios considered tricky in the literature can be solved precisely using the proposed approach. This is confirmed by experiments performed with ENCOVER, a tool based on Java PathFinder and Z3, which we have developed for epistemic noninterference concolic verification.
Place, publisher, year, edition, pages
IEEE , 2012. 30-44 p.
, Proceedings-Computer Security Foundations Workshop, ISSN 1063-6900
information flow security, noninterference, model checking, epistemic logic, SMT solver, declassification
Computer and Information Science
IdentifiersURN: urn:nbn:se:kth:diva-104390DOI: 10.1109/CSF.2012.24ISI: 000309007800003ScopusID: 2-s2.0-84866898679ISBN: 978-0-7695-4718-3OAI: oai:DiVA.org:kth-104390DiVA: diva2:564473
25th IEEE Computer Security Foundations Symposium (CSF), JUN 25-27, 2012, Cambridge, MA
FunderICT - The Next Generation
QC 201211012012-11-012012-11-012014-09-08Bibliographically approved