{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,5,28]],"date-time":"2025-05-28T04:21:21Z","timestamp":1748406081573,"version":"3.41.0"},"publisher-location":"Cham","reference-count":27,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319184661"},{"type":"electronic","value":"9783319184678"}],"license":[{"start":{"date-parts":[[2015,1,1]],"date-time":"2015-01-01T00:00:00Z","timestamp":1420070400000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2015]]},"DOI":"10.1007\/978-3-319-18467-8_27","type":"book-chapter","created":{"date-parts":[[2015,5,8]],"date-time":"2015-05-08T12:12:03Z","timestamp":1431087123000},"page":"401-415","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":11,"title":["Exploit Generation for Information Flow Leaks in Object-Oriented Programs"],"prefix":"10.1007","author":[{"given":"Quoc Huy","family":"Do","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Richard","family":"Bubel","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Reiner","family":"H\u00e4hnle","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2015,5,9]]},"reference":[{"key":"27_CR1","doi-asserted-by":"crossref","unstructured":"Backes, M., Kopf, B., Rybalchenko, A.: Automatic discovery and quantification of information leaks. In: Proc. of the 30th IEEE Symp. on Security and Privacy, pp. 141\u2013153. SP 2009, IEEE CS (2009)","DOI":"10.1109\/SP.2009.18"},{"key":"27_CR2","doi-asserted-by":"crossref","unstructured":"Balliu, M., Dam, M., Le Guernic, G.: ENCoVer: symbolic exploration for information flow security. In: 25th IEEE Computer Security Foundations Symposium, pp. 30\u201344. IEEE CS (2012)","DOI":"10.1109\/CSF.2012.24"},{"key":"27_CR3","first-page":"47","volume":"173","author":"A Banerjee","year":"2007","unstructured":"Banerjee, A., Giacobazzi, R., Mastroeni, I.: What you lose is what you leak: Information leakage in declassification policies. ENTCS 173, 47\u201366 (2007)","journal-title":"ENTCS"},{"issue":"2","key":"27_CR4","doi-asserted-by":"publisher","first-page":"131","DOI":"10.1017\/S0956796804005453","volume":"15","author":"A Banerjee","year":"2005","unstructured":"Banerjee, A., Naumann, D.A.: Stack-based Access Control and Secure Information Flow. J. Funct. Program. 15(2), 131\u2013177 (2005)","journal-title":"J. Funct. Program."},{"key":"27_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"200","DOI":"10.1007\/978-3-642-21437-0_17","volume-title":"FM 2011: Formal Methods","author":"G Barthe","year":"2011","unstructured":"Barthe, G., Crespo, J.M., Kunz, C.: Relational verification using product programs. In: Butler, M., Schulte, W. (eds.) FM 2011. LNCS, vol. 6664, pp. 200\u2013214. Springer, Heidelberg (2011)"},{"key":"27_CR6","doi-asserted-by":"crossref","unstructured":"Barthe, G., D\u2019Argenio, P.R., Rezk, T.: Secure information flow by self-composition. In: Proc. of the 17th IEEE Workshop on Computer Security Foundations, pp. 100\u2013114. CSFW 2004, IEEE CS (2004)","DOI":"10.1109\/CSFW.2004.1310735"},{"key":"27_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"19","DOI":"10.1007\/978-3-319-14125-1_2","volume-title":"Logic-Based Program Synthesis and Transformation","author":"B Beckert","year":"2014","unstructured":"Beckert, B., Bruns, D., Klebanov, V., Scheben, C., Schmitt, P.H., Ulbrich, M.: Information flow in object-oriented software. In: Gupta, G., Pe\u00f1a, R. (eds.) LOPSTR 2013, LNCS 8901. LNCS, vol. 8901, pp. 19\u201337. Springer, Heidelberg (2014)"},{"key":"27_CR8","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","volume-title":"Verification of Object-Oriented Software: The KeY Approach","year":"2007","unstructured":"Beckert, B., H\u00e4hnle, R., Schmitt, P.H. (eds.): Verification of Object-Oriented Software: The KeY Approach. LNCS (LNAI), vol. 4334. Springer, Heidelberg (2007)"},{"key":"27_CR9","unstructured":"Cohen, E.S.: Information Transmission in Sequential Programs. Foundations of Secure Computation, pp. 297\u2013335 (1978)"},{"key":"27_CR10","unstructured":"Darvas, A., H\u00e4hnle, R., Sands, D.: A theorem proving approach to analysis of secure information flow. In: Gorrieri, R. (ed.) Workshop on Issues in the Theory of Security. IFIP WG 1.7, ACM SIGPLAN and GI FoMSESS (2003)"},{"key":"27_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"193","DOI":"10.1007\/978-3-540-32004-3_20","volume-title":"Security in Pervasive Computing","author":"A Darvas","year":"2005","unstructured":"Darvas, A., H\u00e4hnle, R., Sands, D.: A theorem proving approach to analysis of secure information flow. In: Hutter, D., Ullmann, M. (eds.) SPC 2005. LNCS, vol. 3450, pp. 193\u2013209. Springer, Heidelberg (2005)"},{"key":"27_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"169","DOI":"10.1007\/978-3-540-73770-4_10","volume-title":"Tests and Proofs","author":"C Engel","year":"2007","unstructured":"Engel, C., H\u00e4hnle, R.: Generating unit tests from formal proofs. In: Gurevich, Y., Meyer, B. (eds.) TAP 2007. LNCS, vol. 4454, pp. 169\u2013188. Springer, Heidelberg (2007)"},{"key":"27_CR13","unstructured":"Graf, J., Hecker, M., Mohr, M.: Using JOANA for information flow control in java programs - a practical guide. In: Proc. of the 6th Working Conf. on Programming Languages, pp. 123\u2013138. LNI 215, Springer (February 2013)"},{"key":"27_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"82","DOI":"10.1007\/978-3-319-09099-3_7","volume-title":"Tests and Proofs","author":"M Hentschel","year":"2014","unstructured":"Hentschel, M., H\u00e4hnle, R., Bubel, R.: Visualizing unbounded symbolic execution. In: Seidl, M., Tillmann, N. (eds.) TAP 2014. LNCS, vol. 8570, pp. 82\u201398. Springer, Heidelberg (2014)"},{"key":"27_CR15","doi-asserted-by":"crossref","unstructured":"Hunt, S., Sands, D.: On flow-sensitive security types. In: ACM SIGPLAN Notices, vol. 41, pp. 79\u201390. ACM (2006)","DOI":"10.1145\/1111320.1111045"},{"issue":"7","key":"27_CR16","doi-asserted-by":"publisher","first-page":"385","DOI":"10.1145\/360248.360252","volume":"19","author":"JC King","year":"1976","unstructured":"King, J.C.: Symbolic Execution and Program Testing. Commun. ACM 19(7), 385\u2013394 (1976)","journal-title":"Commun. ACM"},{"key":"27_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"152","DOI":"10.1007\/978-3-642-30793-5_10","volume-title":"Formal Techniques for Distributed Systems","author":"D Milushev","year":"2012","unstructured":"Milushev, D., Beck, W., Clarke, D.: Noninterference via symbolic execution. In: Giese, H., Rosu, G. (eds.) FORTE 2012 and FMOODS 2012. LNCS, vol. 7273, pp. 152\u2013168. Springer, Heidelberg (2012)"},{"key":"27_CR18","doi-asserted-by":"crossref","unstructured":"Myers, A.C.: JFlow: practical mostly-static information flow control. In: Proc. of 26th ACM Symp. on Principles of Programming Languages, pp. 228\u2013241 (1999)","DOI":"10.1145\/292540.292561"},{"key":"27_CR19","doi-asserted-by":"crossref","unstructured":"Nanevski, A., Banerjee, A., Garg, D.: Verification of information flow and access control policies with dependent types. In: Proc. of the 2011 IEEE Symp. on Security and Privacy, pp. 165\u2013179. SP 2011, IEEE CS (2011)","DOI":"10.1109\/SP.2011.12"},{"key":"27_CR20","unstructured":"Phan, Q.S.: Self-composition by symbolic execution. In: Jones, A.V., Ng, N. (eds.) Imperial College Computing Student Workshop. OASIcs, vol. 35, pp. 95\u2013102. Schloss Dagstuhl (2013)"},{"key":"27_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"174","DOI":"10.1007\/978-3-540-37621-7_9","volume-title":"Software Security - Theories and Systems","author":"A Sabelfeld","year":"2004","unstructured":"Sabelfeld, A., Myers, A.C.: A model for delimited information release. In: Futatsugi, K., Mizoguchi, F., Yonezaki, N. (eds.) ISSS 2003. LNCS, vol. 3233, pp. 174\u2013191. Springer, Heidelberg (2004)"},{"issue":"5","key":"27_CR22","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 17(5), 517\u2013548 (2009)","journal-title":"Journal of Computer Security"},{"key":"27_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"232","DOI":"10.1007\/978-3-642-31762-0_15","volume-title":"Formal Verification of Object-Oriented Software","author":"C Scheben","year":"2012","unstructured":"Scheben, C., Schmitt, P.H.: Verification of information flow properties of Java programs without approximations. In: Beckert, B., Damiani, F., Gurov, D. (eds.) FoVeOOS 2011. LNCS, vol. 7421, pp. 232\u2013249. Springer, Heidelberg (2012)"},{"key":"27_CR24","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"352","DOI":"10.1007\/11547662_24","volume-title":"Static Analysis","author":"T Terauchi","year":"2005","unstructured":"Terauchi, T., Aiken, A.: Secure information flow as a safety problem. In: Hankin, C., Siveroni, I. (eds.) SAS 2005. LNCS, vol. 3672, pp. 352\u2013367. Springer, Heidelberg (2005)"},{"key":"27_CR25","doi-asserted-by":"crossref","unstructured":"Vaughan, J.A., Chong, S.: Inference of expressive declassification policies. In: Proc. of the 2011 IEEE Symp. on Security and Privacy, pp. 180\u2013195. IEEE CS (2011)","DOI":"10.1109\/SP.2011.20"},{"issue":"2","key":"27_CR26","doi-asserted-by":"crossref","first-page":"167","DOI":"10.3233\/JCS-1996-42-304","volume":"4","author":"D Volpano","year":"1996","unstructured":"Volpano, D., Irvine, C., Smith, G.: A Sound Type System for Secure Flow Analysis. Journal of Computer Security 4(2), 167\u2013187 (1996)","journal-title":"Journal of Computer Security"},{"key":"27_CR27","unstructured":"Wasser, N., Bubel, R.: A theorem prover backed approach to array abstraction. In: Proc. of VSL 2014 \u2013 WING Workshop (2014)"}],"container-title":["IFIP Advances in Information and Communication Technology","ICT Systems Security and Privacy Protection"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-18467-8_27","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,5,27]],"date-time":"2025-05-27T21:22:16Z","timestamp":1748380936000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-18467-8_27"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2015]]},"ISBN":["9783319184661","9783319184678"],"references-count":27,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-18467-8_27","relation":{},"ISSN":["1868-4238","1868-422X"],"issn-type":[{"type":"print","value":"1868-4238"},{"type":"electronic","value":"1868-422X"}],"subject":[],"published":{"date-parts":[[2015]]},"assertion":[{"value":"9 May 2015","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}