{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,5]],"date-time":"2026-02-05T09:55:55Z","timestamp":1770285355638,"version":"3.49.0"},"reference-count":37,"publisher":"Association for Computing Machinery (ACM)","issue":"PLDI","license":[{"start":{"date-parts":[[2023,6,6]],"date-time":"2023-06-06T00:00:00Z","timestamp":1686009600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by-nc\/4.0\/"}],"funder":[{"DOI":"10.13039\/100000001","name":"NSF","doi-asserted-by":"publisher","award":["CF-2008660, CCF-1901098, CCF-1817242"],"award-info":[{"award-number":["CF-2008660, CCF-1901098, CCF-1817242"]}],"id":[{"id":"10.13039\/100000001","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["Proc. ACM Program. Lang."],"published-print":{"date-parts":[[2023,6,6]]},"abstract":"<jats:p>Information leaks are a significant problem in modern software systems. In recent years, information theoretic concepts, such as Shannon entropy, have been applied to quantifying information leaks in programs. One recent approach is to use symbolic execution together with model counting constraints solvers in order to quantify information leakage. There are at least two reasons for unsoundness in quantifying information leakage using this approach: 1) Symbolic execution may not be able to explore all execution paths, 2) Model counting constraints solvers may not be able to provide an exact count. We present a sound symbolic quantitative information flow analysis that bounds the information leakage both for the cases where the program behavior is not fully explored and the model counting constraint solver is unable to provide a precise model count but provides an upper and a lower bound. We implemented our approach as an extension to KLEE for computing sound bounds for information leakage in C programs.<\/jats:p>","DOI":"10.1145\/3591281","type":"journal-article","created":{"date-parts":[[2023,6,6]],"date-time":"2023-06-06T20:06:24Z","timestamp":1686081984000},"page":"1488-1509","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":9,"title":["Obtaining Information Leakage Bounds via Approximate Model Counting"],"prefix":"10.1145","volume":"7","author":[{"ORCID":"https:\/\/orcid.org\/0009-0005-6427-9068","authenticated-orcid":false,"given":"Seemanta","family":"Saha","sequence":"first","affiliation":[{"name":"University of California at Santa Barbara, USA"}]},{"ORCID":"https:\/\/orcid.org\/0009-0007-6968-4059","authenticated-orcid":false,"given":"Surendra","family":"Ghentiyala","sequence":"additional","affiliation":[{"name":"University of California at Santa Barbara, USA"}]},{"ORCID":"https:\/\/orcid.org\/0009-0004-0003-243X","authenticated-orcid":false,"given":"Shihua","family":"Lu","sequence":"additional","affiliation":[{"name":"University of California at Santa Barbara, USA"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-2711-5548","authenticated-orcid":false,"given":"Lucas","family":"Bang","sequence":"additional","affiliation":[{"name":"Harvey Mudd College, USA"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-2993-1215","authenticated-orcid":false,"given":"Tevfik","family":"Bultan","sequence":"additional","affiliation":[{"name":"University of California at Santa Barbara, USA"}]}],"member":"320","published-online":{"date-parts":[[2023,6,6]]},"reference":[{"key":"e_1_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.3390\/e19080427"},{"key":"e_1_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1145\/3140587.3062378"},{"key":"e_1_2_1_3_1","volume-title":"Proceedings of the 27th International Conference on Computer Aided Verification (CAV). 255\u2013272","author":"Aydin Abdulbaki","year":"2015","unstructured":"Abdulbaki Aydin , Lucas Bang , and Tevfik Bultan . 2015 . Automata-Based Model Counting for String Constraints . In Proceedings of the 27th International Conference on Computer Aided Verification (CAV). 255\u2013272 . Abdulbaki Aydin, Lucas Bang, and Tevfik Bultan. 2015. Automata-Based Model Counting for String Constraints. In Proceedings of the 27th International Conference on Computer Aided Verification (CAV). 255\u2013272."},{"key":"e_1_2_1_4_1","volume-title":"Automatic Discovery and Quantification of Information Leaks. In 30th IEEE Symposium on Security and Privacy (S&P 2009)","author":"Backes Michael","year":"2009","unstructured":"Michael Backes , Boris K\u00f6pf , and Andrey Rybalchenko . 2009 . Automatic Discovery and Quantification of Information Leaks. In 30th IEEE Symposium on Security and Privacy (S&P 2009) , 17-20 May 2009, Oakland, California, USA. 141\u2013153. Michael Backes, Boris K\u00f6pf, and Andrey Rybalchenko. 2009. Automatic Discovery and Quantification of Information Leaks. In 30th IEEE Symposium on Security and Privacy (S&P 2009), 17-20 May 2009, Oakland, California, USA. 141\u2013153."},{"key":"e_1_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.scico.2007.08.001"},{"key":"e_1_2_1_6_1","unstructured":"V. Baldoni N. Berline J.A. De Loera B. Dutra M. K\u00f6ppe S. Moreinis G. Pinto M. Vergne and J. Wu. 2014. LattE integrale v1.7.2. http:\/\/www.math.ucdavis.edu\/ latte\/. \t\t\t\t  V. Baldoni N. Berline J.A. De Loera B. Dutra M. K\u00f6ppe S. Moreinis G. Pinto M. Vergne and J. Wu. 2014. LattE integrale v1.7.2. http:\/\/www.math.ucdavis.edu\/ latte\/."},{"key":"e_1_2_1_7_1","volume-title":"Proceedings of the 24th ACM SIGSOFT International Symposium on Foundations of Software Engineering (FSE","author":"Bang Lucas","year":"2016","unstructured":"Lucas Bang , Abdulbaki Aydin , Quoc-Sang Phan , Corina S. P\u0103s\u0103reanu , and Tevfik Bultan . 2016 . String Analysis for Side Channels with Segmented Oracles . In Proceedings of the 24th ACM SIGSOFT International Symposium on Foundations of Software Engineering (FSE 2016). ACM, New York, NY, USA. Lucas Bang, Abdulbaki Aydin, Quoc-Sang Phan, Corina S. P\u0103s\u0103reanu, and Tevfik Bultan. 2016. String Analysis for Side Channels with Segmented Oracles. In Proceedings of the 24th ACM SIGSOFT International Symposium on Foundations of Software Engineering (FSE 2016). ACM, New York, NY, USA."},{"key":"e_1_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1109\/EuroSP.2018.00029"},{"key":"e_1_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1287\/moor.19.4.769"},{"key":"e_1_2_1_10_1","volume-title":"VSTTE 2019","author":"Bultan Tevfik","year":"2019","unstructured":"Tevfik Bultan . 2019 . Quantifying Information Leakage Using Model Counting Constraint Solvers. In Verified Software. Theories, Tools, and Experiments - 11th International Conference , VSTTE 2019 , New York City, NY, USA , July 13-14, 2019, Revised Selected Papers. 30\u201335. Tevfik Bultan. 2019. Quantifying Information Leakage Using Model Counting Constraint Solvers. In Verified Software. Theories, Tools, and Experiments - 11th International Conference, VSTTE 2019, New York City, NY, USA, July 13-14, 2019, Revised Selected Papers. 30\u201335."},{"key":"e_1_2_1_11_1","first-page":"209","article-title":"KLEE: Unassisted and Automatic Generation of High-Coverage Tests for Complex Systems Programs","volume":"8","author":"Cadar Cristian","year":"2008","unstructured":"Cristian Cadar , Daniel Dunbar , and Dawson R Engler . 2008 . KLEE: Unassisted and Automatic Generation of High-Coverage Tests for Complex Systems Programs .. In OSDI. 8 , 209 \u2013 224 . Cristian Cadar, Daniel Dunbar, and Dawson R Engler. 2008. KLEE: Unassisted and Automatic Generation of High-Coverage Tests for Complex Systems Programs.. In OSDI. 8, 209\u2013224.","journal-title":"OSDI."},{"key":"e_1_2_1_12_1","volume-title":"International Conference on Principles and Practice of Constraint Programming. 200\u2013216","author":"Chakraborty Supratik","year":"2013","unstructured":"Supratik Chakraborty , Kuldeep S Meel , and Moshe Y Vardi . 2013 . A scalable approximate model counter . In International Conference on Principles and Practice of Constraint Programming. 200\u2013216 . Supratik Chakraborty, Kuldeep S Meel, and Moshe Y Vardi. 2013. A scalable approximate model counter. In International Conference on Principles and Practice of Constraint Programming. 200\u2013216."},{"key":"e_1_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-11212-1_13"},{"key":"e_1_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.5555\/1370628.1370629"},{"key":"e_1_2_1_15_1","volume-title":"Thomas","author":"Cover Thomas M.","year":"2006","unstructured":"Thomas M. Cover and Joy A . Thomas . 2006 . Elements of Information Theory (Wiley Series in Telecommunications and Signal Processing). Wiley-Interscience . isbn:0471241954 Thomas M. Cover and Joy A. Thomas. 2006. Elements of Information Theory (Wiley Series in Telecommunications and Signal Processing). Wiley-Interscience. isbn:0471241954"},{"key":"e_1_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1145\/2338965.2336773"},{"key":"e_1_2_1_17_1","volume-title":"The principle of maximum entropy. The mathematical intelligencer, 7, 1","author":"Guiasu Silviu","year":"1985","unstructured":"Silviu Guiasu and Abe Shenitzer . 1985. The principle of maximum entropy. The mathematical intelligencer, 7, 1 ( 1985 ), 42\u201348. Silviu Guiasu and Abe Shenitzer. 1985. The principle of maximum entropy. The mathematical intelligencer, 7, 1 (1985), 42\u201348."},{"key":"e_1_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1007\/BF01589330"},{"key":"e_1_2_1_19_1","volume-title":"International Conference on Tests and Proofs. 41\u201354","author":"Kapus Timotej","year":"2019","unstructured":"Timotej Kapus , Martin Nowack , and Cristian Cadar . 2019 . Constraints in Dynamic Symbolic Execution: Bitvectors or Integers? In International Conference on Tests and Proofs. 41\u201354 . Timotej Kapus, Martin Nowack, and Cristian Cadar. 2019. Constraints in Dynamic Symbolic Execution: Bitvectors or Integers? In International Conference on Tests and Proofs. 41\u201354."},{"key":"e_1_2_1_20_1","unstructured":"Seonmo Kim. 2018. SearchMC. https:\/\/github.com\/seonmokim\/SearchMC \t\t\t\t  Seonmo Kim. 2018. SearchMC. https:\/\/github.com\/seonmokim\/SearchMC"},{"key":"e_1_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-40196-1_16"},{"key":"e_1_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1145\/1315245.1315282"},{"key":"e_1_2_1_23_1","volume-title":"2018 IEEE 31st Computer Security Foundations Symposium (CSF). 313\u2013327","author":"Malacaria Pasquale","year":"2018","unstructured":"Pasquale Malacaria , MHR Khouzani , Corina S Pasareanu , Quoc-Sang Phan , and Kasper Luckow . 2018 . Symbolic side-channel analysis for probabilistic programs . In 2018 IEEE 31st Computer Security Foundations Symposium (CSF). 313\u2013327 . Pasquale Malacaria, MHR Khouzani, Corina S Pasareanu, Quoc-Sang Phan, and Kasper Luckow. 2018. Symbolic side-channel analysis for probabilistic programs. In 2018 IEEE 31st Computer Security Foundations Symposium (CSF). 313\u2013327."},{"key":"e_1_2_1_24_1","first-page":"1987","article-title":"Ibm ilog cplex optimization studio","volume":"12","author":"User\u2019s Manual CPLEX","year":"1987","unstructured":"CPLEX User\u2019s Manual . 1987 . Ibm ilog cplex optimization studio . Version , 12 , 1987 - 2018 (1987), 1. CPLEX User\u2019s Manual. 1987. Ibm ilog cplex optimization studio. Version, 12, 1987-2018 (1987), 1.","journal-title":"Version"},{"key":"e_1_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1145\/1375581.1375606"},{"key":"e_1_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.1145\/1554339.1554349"},{"key":"e_1_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.1145\/2632362.2632367"},{"key":"e_1_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.1145\/2382756.2382791"},{"key":"e_1_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.1109\/CSF.2017.8"},{"key":"e_1_2_1_30_1","doi-asserted-by":"publisher","DOI":"10.1145\/2590296.2590328"},{"key":"e_1_2_1_31_1","doi-asserted-by":"publisher","DOI":"10.1109\/CSF.2016.34"},{"key":"e_1_2_1_32_1","unstructured":"PyParma. 2015. PyParma. https:\/\/github.com\/haudren\/pyparma \t\t\t\t  PyParma. 2015. PyParma. https:\/\/github.com\/haudren\/pyparma"},{"key":"e_1_2_1_33_1","doi-asserted-by":"publisher","DOI":"10.1145\/3364452.336445759"},{"key":"e_1_2_1_34_1","volume-title":"William Eiers, Lucas Bang, and Tevfik Bultan.","author":"Saha Seemanta","year":"2019","unstructured":"Seemanta Saha , Ismet Burak Kadron , William Eiers, Lucas Bang, and Tevfik Bultan. 2019 . Attack Synthesis for Strings using Meta-Heuristics. CoRR , abs\/1907.11710 (2019), arXiv:1907.11710. arxiv:1907.11710 Seemanta Saha, Ismet Burak Kadron, William Eiers, Lucas Bang, and Tevfik Bultan. 2019. Attack Synthesis for Strings using Meta-Heuristics. CoRR, abs\/1907.11710 (2019), arXiv:1907.11710. arxiv:1907.11710"},{"key":"e_1_2_1_35_1","doi-asserted-by":"publisher","DOI":"10.3390\/e21090885"},{"key":"e_1_2_1_36_1","volume-title":"12th International Conference, FOSSACS 2009, York, UK, March 22-29, 2009. Proceedings. 288\u2013302","author":"Smith Geoffrey","year":"2009","unstructured":"Geoffrey Smith . 2009 . On the Foundations of Quantitative Information Flow. In Foundations of Software Science and Computational Structures , 12th International Conference, FOSSACS 2009, York, UK, March 22-29, 2009. Proceedings. 288\u2013302 . Geoffrey Smith. 2009. On the Foundations of Quantitative Information Flow. In Foundations of Software Science and Computational Structures, 12th International Conference, FOSSACS 2009, York, UK, March 22-29, 2009. Proceedings. 288\u2013302."},{"key":"e_1_2_1_37_1","volume-title":"2016 IEEE European Symposium on Security and Privacy (EuroS&P). 31\u201346","author":"Val Celina G","year":"2016","unstructured":"Celina G Val , Michael A Enescu , Sam Bayless , William Aiello , and Alan J Hu . 2016 . Precisely measuring quantitative information flow: 10k lines of code and beyond . In 2016 IEEE European Symposium on Security and Privacy (EuroS&P). 31\u201346 . Celina G Val, Michael A Enescu, Sam Bayless, William Aiello, and Alan J Hu. 2016. Precisely measuring quantitative information flow: 10k lines of code and beyond. In 2016 IEEE European Symposium on Security and Privacy (EuroS&P). 31\u201346."}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3591281","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3591281","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T16:47:20Z","timestamp":1750178840000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3591281"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2023,6,6]]},"references-count":37,"journal-issue":{"issue":"PLDI","published-print":{"date-parts":[[2023,6,6]]}},"alternative-id":["10.1145\/3591281"],"URL":"https:\/\/doi.org\/10.1145\/3591281","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2023,6,6]]},"assertion":[{"value":"2023-06-06","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}