{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,11,1]],"date-time":"2025-11-01T12:59:53Z","timestamp":1762001993599,"version":"build-2065373602"},"publisher-location":"Cham","reference-count":32,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319737201"},{"type":"electronic","value":"9783319737218"}],"license":[{"start":{"date-parts":[[2017,12,29]],"date-time":"2017-12-29T00:00:00Z","timestamp":1514505600000},"content-version":"unspecified","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":[[2018]]},"DOI":"10.1007\/978-3-319-73721-8_20","type":"book-chapter","created":{"date-parts":[[2017,12,28]],"date-time":"2017-12-28T09:13:05Z","timestamp":1514452385000},"page":"430-451","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":2,"title":["A Logical System for Modular Information Flow Verification"],"prefix":"10.1007","author":[{"given":"Adi","family":"Prabawa","sequence":"first","affiliation":[]},{"given":"Mahmudul Faisal","family":"Al Ameen","sequence":"additional","affiliation":[]},{"given":"Benedict","family":"Lee","sequence":"additional","affiliation":[]},{"given":"Wei-Ngan","family":"Chin","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2017,12,29]]},"reference":[{"key":"20_CR1","unstructured":"Al Ameen, M.F., Tatsuta, M.: Completeness for Recursive Procedures in Separation Logic. Theoretical Computer Science (2016)"},{"key":"20_CR2","unstructured":"Al Ameen, M.F.: Completeness of Verification System with Separation Logic for Recursive Procedures. Ph.D. Dissertation. SOKENDAI, Kanagawa, Japan (2016)"},{"key":"20_CR3","doi-asserted-by":"crossref","unstructured":"Barthe, G., D\u2019Argenio, P.R., Rezk, T.: Secure information flow by self-composition. In: Proceedings of the 17th IEEE Workshop on Computer Security Foundations (CSFW 2004), p. 100. IEEE Computer Society, Washington, DC (2004)","DOI":"10.1109\/CSFW.2004.1310735"},{"key":"20_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"100","DOI":"10.1007\/978-3-540-27864-1_10","volume-title":"Static Analysis","author":"T Amtoft","year":"2004","unstructured":"Amtoft, T., Banerjee, A.: Information flow analysis in logical form. In: Giacobazzi, R. (ed.) SAS 2004. LNCS, vol. 3148, pp. 100\u2013115. Springer, Heidelberg (2004). https:\/\/doi.org\/10.1007\/978-3-540-27864-1_10"},{"key":"20_CR5","doi-asserted-by":"crossref","unstructured":"Amtoft, T., Bandhakavi, S., Banerjee, A.: A logic for information flow in object-oriented programs. In: Conference Record of the 33rd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, New York, USA (2006)","DOI":"10.1145\/1111037.1111046"},{"key":"20_CR6","doi-asserted-by":"crossref","unstructured":"Austin, T.H., Flanagan, C.: Permissive dynamic information flow analysis. In: Proceedings of the 5th ACM SIGPLAN Workshop on Programming Languages and Analysis for Security (PLAS 2010). ACM, New York (2010). Article 3, 12 pages","DOI":"10.1145\/1814217.1814220"},{"key":"20_CR7","doi-asserted-by":"crossref","unstructured":"Austin, T.H., Flanagan, C.: Multiple facets for dynamic information flow. In: Proceedings of the 39th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL 2012), pp. 165\u2013178. ACM, New York (2012)","DOI":"10.1145\/2103656.2103677"},{"key":"20_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"55","DOI":"10.1007\/978-3-642-29420-4_4","volume-title":"Formal Aspects of Security and Trust","author":"L Bello","year":"2012","unstructured":"Bello, L., Bonelli, E.: On-the-fly inlining of dynamic dependency monitors for secure information flow. In: Barthe, G., Datta, A., Etalle, S. (eds.) FAST 2011. LNCS, vol. 7140, pp. 55\u201369. Springer, Heidelberg (2012). https:\/\/doi.org\/10.1007\/978-3-642-29420-4_4"},{"issue":"9","key":"20_CR9","doi-asserted-by":"crossref","first-page":"1006","DOI":"10.1016\/j.scico.2010.07.004","volume":"77","author":"WN Chin","year":"2012","unstructured":"Chin, W.N., David, C., Nguyen, H.H., Qin, S.: Automated verification of shape, size and bag properties via user-defined predicates in separation logic. Sci. Comput. Program. 77(9), 1006\u20131036 (2012)","journal-title":"Sci. Comput. Program."},{"key":"20_CR10","doi-asserted-by":"crossref","unstructured":"Chudnov, A., Naumann, D.A.: Information flow monitor inlining. In: 2010 23rd IEEE Computer Security Foundations Symposium, Edinburgh, pp. 200\u2013214 (2010)","DOI":"10.1109\/CSF.2010.21"},{"key":"20_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"179","DOI":"10.1007\/978-3-642-54792-8_10","volume-title":"Principles of Security and Trust","author":"D Costanzo","year":"2014","unstructured":"Costanzo, D., Shao, Z.: A separation logic for enforcing declarative information flow control policies. In: Abadi, M., Kremer, S. (eds.) POST 2014. LNCS, vol. 8414, pp. 179\u2013198. Springer, Heidelberg (2014). https:\/\/doi.org\/10.1007\/978-3-642-54792-8_10"},{"issue":"7","key":"20_CR12","doi-asserted-by":"crossref","first-page":"504","DOI":"10.1145\/359636.359712","volume":"20","author":"DE Denning","year":"1977","unstructured":"Denning, D.E., Denning, P.J.: Certification of programs for secure information flow. Commun. ACM 20(7), 504\u2013513 (1977)","journal-title":"Commun. ACM"},{"key":"20_CR13","doi-asserted-by":"crossref","unstructured":"Goguen, J.A., Meseguer, J.: Security policies and security models. In: IEEE Symposium on Security and Privacy, Oakland, CA, USA (1982)","DOI":"10.1109\/SP.1982.10014"},{"key":"20_CR14","doi-asserted-by":"crossref","unstructured":"Hunt, S., Sands, D.: On flow-sensitive security types. In: POPL, pp. 79\u201390 (2006)","DOI":"10.1145\/1111037.1111045"},{"key":"20_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"321","DOI":"10.1007\/978-3-319-27659-5_23","volume-title":"Information Security","author":"C Kerschbaumer","year":"2015","unstructured":"Kerschbaumer, C., Hennigan, E., Larsen, P., Brunthaler, S., Franz, M.: Crowdflow: efficient information flow security. In: Desmedt, Y. (ed.) ISC 2013. LNCS, vol. 7807, pp. 321\u2013337. Springer, Cham (2015). https:\/\/doi.org\/10.1007\/978-3-319-27659-5_23"},{"issue":"10","key":"20_CR16","doi-asserted-by":"crossref","first-page":"613","DOI":"10.1145\/362375.362389","volume":"16","author":"BW Lampson","year":"1973","unstructured":"Lampson, B.W.: A note on the confinement problem. Commun. ACM 16(10), 613\u2013615 (1973)","journal-title":"Commun. ACM"},{"key":"20_CR17","volume-title":"A Calculus of Communicating Systems","author":"R Milner","year":"1982","unstructured":"Milner, R.: A Calculus of Communicating Systems. Springer-Verlag, New York Inc (1982)"},{"key":"20_CR18","doi-asserted-by":"crossref","unstructured":"Nanevski, A., Banerjee, A., Garg, D.: Verification of information flow and access control policies with dependent types. In: Proceedings of the 2011 IEEE Symposium on Security and Privacy (SP 2011), pp. 165\u2013179. IEEE Computer Society, Washington, DC (2011)","DOI":"10.1109\/SP.2011.12"},{"issue":"6","key":"20_CR19","doi-asserted-by":"crossref","first-page":"557","DOI":"10.1017\/S0956796897002906","volume":"7","author":"P \u00d8rb\u00e6k","year":"1997","unstructured":"\u00d8rb\u00e6k, P., Palsberg, J.: Trust in the $$\\lambda $$ -calculus. J. Funct. Program. 7(6), 557\u2013591 (1997)","journal-title":"J. Funct. Program."},{"key":"20_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"167","DOI":"10.1007\/BFb0017309","volume-title":"Theoretical Computer Science","author":"D Park","year":"1981","unstructured":"Park, D.: Concurrency and automata on infinite sequences. In: Deussen, P. (ed.) GI-TCS 1981. LNCS, vol. 104, pp. 167\u2013183. Springer, Heidelberg (1981). https:\/\/doi.org\/10.1007\/BFb0017309"},{"key":"20_CR21","doi-asserted-by":"crossref","unstructured":"Reynolds, J.C.: Separation logic: a logic for shared mutable data structures. In: Proceedings of the 17th Annual IEEE Symposium on Logic in Computer Science (LICS 2002), pp. 55\u201374. IEEE Computer Society, Washington, DC (2002)","DOI":"10.1109\/LICS.2002.1029817"},{"key":"20_CR22","doi-asserted-by":"crossref","unstructured":"Russo, A., Sabelfeld, A.: Dynamic vs. static flow-sensitive security analysis. In: Proceedings of the 2010 23rd IEEE Computer Security Foundations Symposium (CSF 2010), pp. 186\u2013199. IEEE Computer Society, Washington, DC (2010)","DOI":"10.1109\/CSF.2010.20"},{"key":"20_CR23","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). https:\/\/doi.org\/10.1007\/978-3-540-37621-7_9"},{"issue":"1","key":"20_CR24","doi-asserted-by":"crossref","first-page":"5","DOI":"10.1109\/JSAC.2002.806121","volume":"21","author":"A Sabelfeld","year":"2006","unstructured":"Sabelfeld, A., Myers, A.C.: Language-based information-flow security. IEEE J. Sel. A. Commun. 21(1), 5\u201319 (2006)","journal-title":"IEEE J. Sel. A. Commun."},{"key":"20_CR25","series-title":"IFIP Advances in Information and Communication Technology","doi-asserted-by":"publisher","first-page":"278","DOI":"10.1007\/978-3-642-55415-5_23","volume-title":"ICT Systems Security and Privacy Protection","author":"JF Santos","year":"2014","unstructured":"Santos, J.F., Rezk, T.: An information flow monitor-inlining compiler for securing a core of JavaScript. In: Cuppens-Boulahia, N., Cuppens, F., Jajodia, S., Abou El Kalam, A., Sans, T. (eds.) SEC 2014. IAICT, vol. 428, pp. 278\u2013292. Springer, Heidelberg (2014). https:\/\/doi.org\/10.1007\/978-3-642-55415-5_23"},{"key":"20_CR26","doi-asserted-by":"crossref","unstructured":"Tatsuta, M., Chin, W.N., Al Ameen, M.F.: Completeness of pointer program verification by separation logic. In: Proceeding of 7th IEEE International Conference on Software Engineering and Formal Methods (SEFM 2009), pp. 179\u2013188 (2009)","DOI":"10.1109\/SEFM.2009.33"},{"key":"20_CR27","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). https:\/\/doi.org\/10.1007\/11547662_24"},{"key":"20_CR28","unstructured":"Fennell, L., Thiemann, P.: LJGS: gradual security types for object-oriented languages. In: 30th European Conference on Object-Oriented Programming (ECOOP 2016) (2016)"},{"issue":"2\u20133","key":"20_CR29","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. J. Comput. Secur. 4(2\u20133), 167\u2013187 (1996)","journal-title":"J. Comput. Secur."},{"key":"20_CR30","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"607","DOI":"10.1007\/BFb0030629","volume-title":"TAPSOFT \u201997: Theory and Practice of Software Development","author":"D Volpano","year":"1997","unstructured":"Volpano, D., Smith, G.: A type-based approach to program security. In: Bidoit, M., Dauchet, M. (eds.) CAAP 1997. LNCS, vol. 1214, pp. 607\u2013621. Springer, Heidelberg (1997). https:\/\/doi.org\/10.1007\/BFb0030629"},{"key":"20_CR31","doi-asserted-by":"crossref","DOI":"10.7551\/mitpress\/3054.001.0001","volume-title":"The Formal Semantics of Programming Languages: An Introduction","author":"G Winskel","year":"1993","unstructured":"Winskel, G.: The Formal Semantics of Programming Languages: An Introduction. MIT Press, Cambridge (1993)"},{"key":"20_CR32","unstructured":"Zdancewic, S.A.: Programming Languages for Information Security. Ph.D. Dissertation. Cornell University, Ithaca, NY, USA. AAI3063751 (2002)"}],"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-319-73721-8_20","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,10,8]],"date-time":"2019-10-08T20:01:18Z","timestamp":1570564878000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-73721-8_20"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017,12,29]]},"ISBN":["9783319737201","9783319737218"],"references-count":32,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-73721-8_20","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2017,12,29]]}}}