{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,11,18]],"date-time":"2025-11-18T12:15:04Z","timestamp":1763468104700,"version":"3.41.0"},"reference-count":15,"publisher":"Association for Computing Machinery (ACM)","issue":"6","license":[{"start":{"date-parts":[[2012,11,27]],"date-time":"2012-11-27T00:00:00Z","timestamp":1353974400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["SIGSOFT Softw. Eng. Notes"],"published-print":{"date-parts":[[2012,11,27]]},"abstract":"<jats:p>Quantitative Information Flow (QIF) is a powerful approach to quantify leaks of confidential information in a software system. Here we present a novel method that precisely quanties information leaks. In order to mitigate the state-space explosion problem, we propose a symbolic representation of data, and a general SMT-based framework to explore systematically the state space. Symbolic Execution fits well with our framework, so we implement a method of QIF analysis employing Symbolic Execution. We develop our method as a prototype tool that can perform QIF analysis for a software system developed in Java. The tool is built on top of Java Pathfinder, an open source model checking platform, and it is the first tool in the field to support information-theoretic QIF analysis.<\/jats:p>","DOI":"10.1145\/2382756.2382791","type":"journal-article","created":{"date-parts":[[2012,11,29]],"date-time":"2012-11-29T15:02:27Z","timestamp":1354201347000},"page":"1-5","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":45,"title":["Symbolic quantitative information flow"],"prefix":"10.1145","volume":"37","author":[{"given":"Quoc-Sang","family":"Phan","sequence":"first","affiliation":[{"name":"Queen Mary University of London"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Pasquale","family":"Malacaria","sequence":"additional","affiliation":[{"name":"Queen Mary University of London"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Oksana","family":"Tkachuk","sequence":"additional","affiliation":[{"name":"NASA Ames Research Center"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Corina S.","family":"P\u0103s\u0103reanu","sequence":"additional","affiliation":[{"name":"NASA Ames Research Center"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2012,11,27]]},"reference":[{"key":"e_1_2_1_1_1","unstructured":"http:\/\/babelsh.arc.nasa.gov\/trac\/jpf\/.  http:\/\/babelsh.arc.nasa.gov\/trac\/jpf\/."},{"key":"e_1_2_1_2_1","unstructured":"http:\/\/code.google.com\/p\/relsat\/.  http:\/\/code.google.com\/p\/relsat\/."},{"key":"e_1_2_1_3_1","unstructured":"http:\/\/sites.google.com\/site\/stpfastprover\/.  http:\/\/sites.google.com\/site\/stpfastprover\/."},{"key":"e_1_2_1_4_1","unstructured":"http:\/\/www.wolfram.com\/mathematica\/.  http:\/\/www.wolfram.com\/mathematica\/."},{"key":"e_1_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1109\/SP.2009.18"},{"key":"e_1_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1287\/moor.19.4.769"},{"key":"e_1_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.5555\/1370628.1370629"},{"key":"e_1_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1145\/1190216.1190251"},{"key":"e_1_2_1_9_1","volume-title":"Algebraic foundations for information theoretical, probabilistic and guessability measures of information ow. CoRR abs\/1101.3453","author":"Malacaria P.","year":"2011","unstructured":"Malacaria , P. Algebraic foundations for information theoretical, probabilistic and guessability measures of information ow. CoRR abs\/1101.3453 ( 2011 ). Malacaria, P. Algebraic foundations for information theoretical, probabilistic and guessability measures of information ow. CoRR abs\/1101.3453 (2011)."},{"key":"e_1_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1145\/1375696.1375713"},{"key":"e_1_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1109\/ISIT.1994.394764"},{"key":"e_1_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1145\/2166956.2166957"},{"key":"e_1_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1145\/1858996.1859035"},{"key":"e_1_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1109\/JSAC.2002.806121"},{"key":"e_1_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.5555\/3266641.3266673"}],"container-title":["ACM SIGSOFT Software Engineering Notes"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2382756.2382791","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/2382756.2382791","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T09:34:54Z","timestamp":1750239294000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2382756.2382791"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2012,11,27]]},"references-count":15,"journal-issue":{"issue":"6","published-print":{"date-parts":[[2012,11,27]]}},"alternative-id":["10.1145\/2382756.2382791"],"URL":"https:\/\/doi.org\/10.1145\/2382756.2382791","relation":{},"ISSN":["0163-5948"],"issn-type":[{"type":"print","value":"0163-5948"}],"subject":[],"published":{"date-parts":[[2012,11,27]]},"assertion":[{"value":"2012-11-27","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}