| dc.contributor.author | Phan, Q-S | en_US |
| dc.contributor.author | Malacaria, P | en_US |
| dc.contributor.author | ASIA CCS '14 Proceedings of the 9th ACM symposium on Information, computer and communications security | en_US |
| dc.date.accessioned | 2014-09-16T08:57:50Z | |
| dc.date.issued | 2014 | en_US |
| dc.identifier.isbn | 978-1-4503-2800-5 | en_US |
| dc.identifier.uri | http://qmro.qmul.ac.uk/xmlui/handle/123456789/6120 | |
| dc.description | acmid: 2590328 keywords: model checking, quantitative information flow, satisfiability modulo theories, symbolic execution location: Kyoto, Japan numpages: 10 | |
| dc.description | acmid: 2590328 keywords: model checking, quantitative information flow, satisfiability modulo theories, symbolic execution location: Kyoto, Japan numpages: 10 | en_US |
| dc.description | acmid: 2590328 keywords: model checking, quantitative information flow, satisfiability modulo theories, symbolic execution location: Kyoto, Japan numpages: 10 | en_US |
| dc.description.abstract | We present a novel method for Quantitative Information Flow analysis. We show how the problem of computing information leakage can be viewed as an extension of the Satisfiability Modulo Theories (SMT) problem. This view enables us to develop a framework for QIF analysis based on the framework DPLL(T) used in SMT solvers. We then show that the methodology of Symbolic Execution (SE) also fits our framework. Based on these ideas, we build two QIF analysis tools: the first one employs CBMC, a bounded model checker for ANSI C, and the second one is built on top of Symbolic PathFinder, a Symbolic Executor for Java. We use these tools to quantify leaks in industrial code such as C programs from the Linux kernel, a Java tax program from the European project HATS, and anonymity protocols | en_US |
| dc.format.extent | 283 - 292 (9) | en_US |
| dc.publisher | ACM | en_US |
| dc.subject | model checking | en_US |
| dc.subject | quantitative information flow | en_US |
| dc.subject | satisfiability modulo theories | en_US |
| dc.subject | symbolic execution | en_US |
| dc.title | Abstract Model Counting: A Novel Approach for Quantification of Information Leaks | en_US |
| dc.type | Conference Proceeding | |
| dc.identifier.doi | 10.1145/2590296.2590328 | en_US |
| pubs.notes | Not known | en_US |
| pubs.publication-status | Published | en_US |
| pubs.publisher-url | http://doi.acm.org/10.1145/2590296.2590328 | en_US |
