Efficient SAT-Based Pre-image Enumeration for Quantitative Information Flow in Programs

Autor:	Alexander Weigl
Rok vydání:	2016
Předmět:	Propositional formula Normalization property Theoretical computer science Computer science Enumeration Information flow (information theory) Software system Conjunctive normal form Conjunctive normal form formula Image (mathematics)
Zdroj:	Data Privacy Management and Security Assurance ISBN: 9783319470719 DPM/QASA@ESORICS
DOI:	10.1007/978-3-319-47072-6_4
Popis:	Quantitative Information Flow Analysis (QIF) measures the loss of an attacker’s uncertainty about the confidential information (pre-image) inside a software system after observing the system outputs (image). In this paper, we supplement the SAT-based QIF analysis for deterministic and terminating C programs, by introducing three algorithms for counting the pre-images and images, which utilizes advantages of incremental SAT solvers. Our tool sharpPI is competitive to mql, quail and chimp. An implementation is provided under http://formal.iti.kit.edu/sharpPI.
Databáze:	OpenAIRE
Externí odkaz:	https://explore.openaire.eu/search/publication?articleId=doi_________::cbfe93ad7367cfa11c7fcb90e93844c5 https://doi.org/10.1007/978-3-319-47072-6_4 Zobrazit plný text záznamu