{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,23]],"date-time":"2026-04-23T06:26:54Z","timestamp":1776925614622,"version":"3.51.2"},"publisher-location":"Berlin, Heidelberg","reference-count":42,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783662460801","type":"print"},{"value":"9783662460818","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2015]]},"DOI":"10.1007\/978-3-662-46081-8_4","type":"book-chapter","created":{"date-parts":[[2014,12,11]],"date-time":"2014-12-11T04:25:44Z","timestamp":1418271944000},"page":"61-79","source":"Crossref","is-referenced-by-count":12,"title":["Datacentric Semantics for Verification of Privacy Policy Compliance by Mobile Applications"],"prefix":"10.1007","author":[{"given":"Agostino","family":"Cortesi","sequence":"first","affiliation":[]},{"given":"Pietro","family":"Ferrara","sequence":"additional","affiliation":[]},{"given":"Marco","family":"Pistoia","sequence":"additional","affiliation":[]},{"given":"Omer","family":"Tripp","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"4_CR1","doi-asserted-by":"crossref","unstructured":"Alvim, M.S., Scedrov, A., Schneider, F.B.: When not all bits are equal: Worth-based information flow. In: Abadi, M., Kremer, S. (eds.) POST 2014. LNCS, vol.\u00a08414, pp. 120\u2013139. Springer, Heidelberg (2014)","DOI":"10.1007\/978-3-642-54792-8_7"},{"key":"4_CR2","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1016\/j.scico.2006.03.002","volume":"64","author":"T. Amtoft","year":"2007","unstructured":"Amtoft, T., Banerjee, A.: A logic for information flow analysis with an application to forward slicing of simple imperative programs. Science of Compututer Programming\u00a064, 3\u201328 (2007)","journal-title":"Science of Compututer Programming"},{"key":"4_CR3","unstructured":"AppBrain. Adnetwork stats, \n                  \n                    http:\/\/www.appbrain.com\/stats\/libraries\/ad"},{"key":"4_CR4","doi-asserted-by":"crossref","unstructured":"Arzt, S., Rasthofer, S., et al.: Flowdroid: Precise context, flow, field, object-sensitive and lifecycle-aware taint analysis for android apps. In: PLDI. ACM (2014)","DOI":"10.1145\/2594291.2594299"},{"key":"4_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"64","DOI":"10.1007\/978-3-642-11957-6_5","volume-title":"Programming Languages and Systems","author":"A. Askarov","year":"2010","unstructured":"Askarov, A., Myers, A.: A semantic framework for declassification and endorsement. In: Gordon, A.D. (ed.) ESOP 2010. LNCS, vol.\u00a06012, pp. 64\u201384. Springer, Heidelberg (2010)"},{"key":"4_CR6","doi-asserted-by":"crossref","unstructured":"Cavadini, S.: Secure slices of insecure programs. In: ASIACCS. ACM Press (2008)","DOI":"10.1145\/1368310.1368329"},{"key":"4_CR7","doi-asserted-by":"crossref","unstructured":"Chaudhuri, A.: Language-based security on android. In: PLAS. ACM (2009)","DOI":"10.1145\/1554339.1554341"},{"key":"4_CR8","doi-asserted-by":"publisher","first-page":"325","DOI":"10.4204\/EPTCS.129.19","volume":"129","author":"A. Cortesi","year":"2013","unstructured":"Cortesi, A., Costantini, G., Ferrara, P.: A survey on product operators in abstract interpretation. EPTCS\u00a0129, 325\u2013336 (2013)","journal-title":"EPTCS"},{"key":"4_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"505","DOI":"10.1007\/978-3-642-24559-6_34","volume-title":"Formal Methods and Software Engineering","author":"G. Costantini","year":"2011","unstructured":"Costantini, G., Ferrara, P., Cortesi, A.: Static analysis of string values. In: Qin, S., Qiu, Z. (eds.) ICFEM 2011. LNCS, vol.\u00a06991, pp. 505\u2013521. Springer, Heidelberg (2011)"},{"key":"4_CR10","doi-asserted-by":"crossref","unstructured":"Cousot, P., Cousot, R.: Abstract interpretation: Past, present and future. In: CSL-LICS. ACM (2014)","DOI":"10.1145\/2603088.2603165"},{"key":"4_CR11","doi-asserted-by":"crossref","unstructured":"Cousot, P., Cousot, R., Logozzo, F.: A parametric segmentation functor for fully automatic and scalable array content analysis. In: POPL. ACM (2011)","DOI":"10.1145\/1926385.1926399"},{"key":"4_CR12","doi-asserted-by":"publisher","first-page":"236","DOI":"10.1145\/360051.360056","volume":"19","author":"D.E. Denning","year":"1976","unstructured":"Denning, D.E.: A lattice model of secure information flow. Communications of the ACM\u00a019, 236\u2013243 (1976)","journal-title":"Communications of the ACM"},{"key":"4_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/978-3-540-79228-4_1","volume-title":"Theory and Applications of Models of Computation","author":"C. Dwork","year":"2008","unstructured":"Dwork, C.: Differential privacy: A survey of results. In: Agrawal, M., Du, D.-Z., Duan, Z., Li, A. (eds.) TAMC 2008. LNCS, vol.\u00a04978, pp. 1\u201319. Springer, Heidelberg (2008)"},{"key":"4_CR14","doi-asserted-by":"crossref","unstructured":"Ebadi, H., Sands, D., Schneider, G.: Differential privacy: Now it\u2019s getting personal. In: POPL. ACM (2015)","DOI":"10.1145\/2676726.2677005"},{"issue":"3","key":"4_CR15","doi-asserted-by":"publisher","first-page":"99","DOI":"10.1145\/2494522","volume":"57","author":"W. Enck","year":"2014","unstructured":"Enck, W., Gilbert, P., et al.: Taintdroid: An information flow tracking system for real-time privacy monitoring on smartphones. Comm. of the ACM\u00a057(3), 99\u2013106 (2014)","journal-title":"Comm. of the ACM"},{"key":"4_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"302","DOI":"10.1007\/978-3-642-54013-4_17","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"P. Ferrara","year":"2014","unstructured":"Ferrara, P.: Generic combination of heap and value analyses in abstract interpretation. In: McMillan, K.L., Rival, X. (eds.) VMCAI 2014. LNCS, vol.\u00a08318, pp. 302\u2013321. Springer, Heidelberg (2014)"},{"key":"4_CR17","doi-asserted-by":"crossref","unstructured":"Halder, R., Zanioli, M., Cortesi, A.: Information leakage analysis of database query languages. In: SAC. ACM (2014)","DOI":"10.1145\/2554850.2554862"},{"key":"4_CR18","doi-asserted-by":"publisher","first-page":"399","DOI":"10.1007\/s10207-009-0086-1","volume":"8","author":"C. Hammer","year":"2009","unstructured":"Hammer, C., Snelting, G.: Flow-sensitive, context-sensitive, and object-sensitive information flow control based on program dependence graphs. International Journal of Information Security\u00a08, 399\u2013422 (2009)","journal-title":"International Journal of Information Security"},{"key":"4_CR19","doi-asserted-by":"crossref","unstructured":"Hornyack, P., Han, S., Jung, J., Schechter, S.E., Wetherall, D.: These aren\u2019t the droids you\u2019re looking for: retrofitting android to protect data from imperious applications. In: CCS. ACM (2011)","DOI":"10.1145\/2046707.2046780"},{"key":"4_CR20","doi-asserted-by":"crossref","unstructured":"Krohn, M.N., Tromer, E.: Noninterference for a practical DIFC-based operating system. In: IEEE S&P. IEEE (2009)","DOI":"10.1109\/SP.2009.23"},{"key":"4_CR21","doi-asserted-by":"publisher","first-page":"98","DOI":"10.1145\/571681.571683","volume":"27","author":"B. Li","year":"2002","unstructured":"Li, B.: Analyzing information-flow in java program based on slicing technique. SIGSOFT Softw. Eng. Notes\u00a027, 98\u2013103 (2002)","journal-title":"SIGSOFT Softw. Eng. Notes"},{"key":"4_CR22","doi-asserted-by":"publisher","first-page":"263","DOI":"10.1007\/s10515-009-0050-3","volume":"16","author":"A. Lochbihler","year":"2009","unstructured":"Lochbihler, A., Snelting, G.: On temporal path conditions in dependence graphs. Journal of Automated Software Engineering\u00a016, 263\u2013290 (2009)","journal-title":"Journal of Automated Software Engineering"},{"key":"4_CR23","doi-asserted-by":"publisher","first-page":"100","DOI":"10.1016\/j.cl.2005.01.001","volume":"35","author":"F. Logozzo","year":"2009","unstructured":"Logozzo, F.: Class invariants as abstract interpretation of trace semantics. Computer Languages, Systems & Structures\u00a035, 100\u2013142 (2009)","journal-title":"Computer Languages, Systems & Structures"},{"key":"4_CR24","doi-asserted-by":"crossref","unstructured":"Lu, L., Li, Z., Wu, Z., Lee, W., Jiang, G.: Chex: statically vetting android apps for component hijacking vulnerabilities. In: CCS. ACM (2012)","DOI":"10.1145\/2382196.2382223"},{"key":"4_CR25","doi-asserted-by":"crossref","unstructured":"McCamant, S., Ernst, M.D.: Quantitative information flow as network flow capacity. In: PLDI. ACM (2008)","DOI":"10.1145\/1375581.1375606"},{"issue":"1","key":"4_CR26","doi-asserted-by":"publisher","first-page":"31","DOI":"10.1007\/s10990-006-8609-1","volume":"19","author":"A. Min\u00e9","year":"2006","unstructured":"Min\u00e9, A.: The octagon abstract domain. Higher-Order and Symbolic Computation\u00a019(1), 31\u2013100 (2006)","journal-title":"Higher-Order and Symbolic Computation"},{"key":"4_CR27","doi-asserted-by":"crossref","unstructured":"Myers, A.C., Liskov, B.: A decentralized model for information flow control. In: SOSP. ACM (1997)","DOI":"10.1145\/268998.266669"},{"key":"4_CR28","doi-asserted-by":"crossref","unstructured":"Nanevski, A., Banerjee, A., Garg, D.: Dependent type theory for verification of information flow and access control policies. ACM TOPLAS\u00a035(2), 6:1\u20136:41 (2013)","DOI":"10.1145\/2491522.2491523"},{"key":"4_CR29","doi-asserted-by":"crossref","unstructured":"Omoronyia, I., Cavallaro, L., et al.: Engineering adaptive privacy: on the role of privacy awareness requirements. In: ICSE. IEEE\/ACM (2013)","DOI":"10.1109\/ICSE.2013.6606609"},{"key":"4_CR30","doi-asserted-by":"publisher","first-page":"117","DOI":"10.1145\/596980.596983","volume":"25","author":"F. Pottier","year":"2003","unstructured":"Pottier, F., Simonet, V.: Information flow inference for ml. ACM Transactions on Programming Languages and Systems\u00a025, 117\u2013158 (2003)","journal-title":"ACM Transactions on Programming Languages and Systems"},{"key":"4_CR31","doi-asserted-by":"crossref","unstructured":"Rasthofer, S., Lovat, E., Bodden, E.: Droid force: Enforcing complex, data-centric, system-wide policies in android. In: ARES (2014)","DOI":"10.1109\/ARES.2014.13"},{"key":"4_CR32","doi-asserted-by":"publisher","first-page":"5","DOI":"10.1109\/JSAC.2002.806121","volume":"21","author":"A. Sabelfeld","year":"2003","unstructured":"Sabelfeld, A., Myers, A.C.: Language-based information-flow security. IEEE Journal on Selected Areas in Communications\u00a021, 5\u201319 (2003)","journal-title":"IEEE Journal on Selected Areas in Communications"},{"key":"4_CR33","doi-asserted-by":"crossref","first-page":"517","DOI":"10.3233\/JCS-2009-0352","volume":"17","author":"A. Sabelfeld","year":"2009","unstructured":"Sabelfeld, A., Sands, D.: Declassification: Dimensions and principles. Journal of Computer Security\u00a017, 517\u2013548 (2009)","journal-title":"Journal of Computer Security"},{"key":"4_CR34","doi-asserted-by":"crossref","unstructured":"Smith, G.: Principles of secure information flow analysis. In: Christodorescu, M., et al. (eds.) Malware Detection. Advances in Information Security, vol.\u00a027, pp. 291\u2013307. Springer (2007)","DOI":"10.1007\/978-0-387-44599-1_13"},{"key":"4_CR35","doi-asserted-by":"crossref","unstructured":"Smith, S.F., Thober, M.: Refactoring programs to secure information flows. In: PLAS. ACM (2006)","DOI":"10.1145\/1134744.1134758"},{"issue":"1","key":"4_CR36","doi-asserted-by":"publisher","first-page":"67","DOI":"10.1109\/TSE.2008.88","volume":"35","author":"S. Spiekermann","year":"2009","unstructured":"Spiekermann, S., Cranor, L.F.: Engineering privacy. IEEE Trans. Software Eng.\u00a035(1), 67\u201382 (2009)","journal-title":"IEEE Trans. Software Eng."},{"key":"4_CR37","doi-asserted-by":"crossref","unstructured":"Sridharan, M., Artzi, S., Pistoia, M., Guarnieri, S., Tripp, O., Berg, R.: F4f: Taint analysis of framework-based web applications. In: OOPSLA. ACM (2011)","DOI":"10.1145\/2048066.2048145"},{"key":"4_CR38","doi-asserted-by":"crossref","unstructured":"Tripp, O., Ferrara, P., Pistoia, M.: Hybrid security analysis of web javascript code via dynamic partial evaluation. In: ISSTA. ACM (2014)","DOI":"10.1145\/2610384.2610385"},{"key":"4_CR39","unstructured":"Tripp, O., Pistoia, M., Fink, S.J., Sridharan, M., Weisman, O.: Taj: Effective taint analysis of web applications. In: PLDI. ACM (2009)"},{"key":"4_CR40","unstructured":"Tripp, O., Rubin, J.: A bayesian approach to privacy enforcement in smartphones. In: USENIX Security (2014)"},{"key":"4_CR41","doi-asserted-by":"crossref","unstructured":"Xiao, X., Tillmann, N., F\u00e4hndrich, M., de Halleux, J., Moskal, M.: User-aware privacy control via extended static-information-flow analysis. In: ASE. ACM (2012)","DOI":"10.1145\/2351676.2351689"},{"key":"4_CR42","doi-asserted-by":"crossref","unstructured":"Zanioli, M., Ferrara, P., Cortesi, A.: Sails: Static analysis of information leakage with sample. In: SAC. ACM (2012)","DOI":"10.1145\/2245276.2231983"}],"container-title":["Lecture Notes in Computer Science","Verification, Model Checking, and Abstract Interpretation"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-662-46081-8_4","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,28]],"date-time":"2019-05-28T20:30:41Z","timestamp":1559075441000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-662-46081-8_4"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2015]]},"ISBN":["9783662460801","9783662460818"],"references-count":42,"URL":"https:\/\/doi.org\/10.1007\/978-3-662-46081-8_4","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2015]]}}}