{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,8,22]],"date-time":"2025-08-22T04:58:07Z","timestamp":1755838687591},"publisher-location":"Cham","reference-count":51,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319897219"},{"type":"electronic","value":"9783319897226"}],"license":[{"start":{"date-parts":[[2018,1,1]],"date-time":"2018-01-01T00:00:00Z","timestamp":1514764800000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2018]]},"DOI":"10.1007\/978-3-319-89722-6_3","type":"book-chapter","created":{"date-parts":[[2018,4,13]],"date-time":"2018-04-13T14:53:50Z","timestamp":1523631230000},"page":"53-78","update-policy":"http:\/\/dx.doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":7,"title":["Compositional Non-interference for Concurrent Programs via Separation and Framing"],"prefix":"10.1007","author":[{"given":"Aleksandr","family":"Karbyshev","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Kasper","family":"Svendsen","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Aslan","family":"Askarov","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Lars","family":"Birkedal","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2018,4,14]]},"reference":[{"key":"3_CR1","doi-asserted-by":"crossref","unstructured":"Agat, J.: Transforming out timing leaks. In: POPL (2000)","DOI":"10.1145\/325694.325702"},{"key":"3_CR2","doi-asserted-by":"crossref","unstructured":"Askarov, A., Sabelfeld, A.: Tight enforcement of information-release policies for dynamic languages. In: CSF (2009)","DOI":"10.1109\/CSF.2009.22"},{"key":"3_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"333","DOI":"10.1007\/978-3-540-88313-5_22","volume-title":"Computer Security - ESORICS 2008","author":"A Askarov","year":"2008","unstructured":"Askarov, A., Hunt, S., Sabelfeld, A., Sands, D.: Termination-insensitive noninterference leaks more than just a bit. In: Jajodia, S., Lopez, J. (eds.) ESORICS 2008. LNCS, vol. 5283, pp. 333\u2013348. Springer, Heidelberg (2008). https:\/\/doi.org\/10.1007\/978-3-540-88313-5_22"},{"key":"3_CR4","doi-asserted-by":"crossref","unstructured":"Askarov, A., Chong, S., Mantel, H.: Hybrid monitors for concurrent noninterference. In: CSF (2015)","DOI":"10.1109\/CSF.2015.17"},{"key":"3_CR5","doi-asserted-by":"crossref","unstructured":"Barthe, G., Nieto, L.P.: Formally verifying information flow type systems for concurrent and thread systems. In: FMSE (2004)","DOI":"10.1145\/1029133.1029136"},{"issue":"2","key":"3_CR6","doi-asserted-by":"publisher","first-page":"33","DOI":"10.1016\/j.entcs.2005.10.031","volume":"153","author":"G Barthe","year":"2006","unstructured":"Barthe, G., Rezk, T., Warnier, M.: Preventing timing leaks through transactional branching instructions. Electron. Notes Theor. Comput. Sci. 153(2), 33\u201355 (2006)","journal-title":"Electron. Notes Theor. Comput. Sci."},{"issue":"3","key":"3_CR7","doi-asserted-by":"publisher","first-page":"21","DOI":"10.1145\/1805974.1805977","volume":"13","author":"G Barthe","year":"2010","unstructured":"Barthe, G., Rezk, T., Russo, A., Sabelfeld, A.: Security of multithreaded programs by compilation. ACM Trans. Inf. Syst. Secur. 13(3), 21 (2010)","journal-title":"ACM Trans. Inf. Syst. Secur."},{"issue":"6","key":"3_CR8","doi-asserted-by":"publisher","first-page":"1207","DOI":"10.1017\/S0960129511000193","volume":"21","author":"G Barthe","year":"2011","unstructured":"Barthe, G., D\u2019Argenio, P.R., Rezk, T.: Secure information flow by self-composition. Math. Struct. Comput. Sci. 21(6), 1207\u20131252 (2011)","journal-title":"Math. Struct. Comput. Sci."},{"issue":"1\u20132","key":"3_CR9","doi-asserted-by":"publisher","first-page":"109","DOI":"10.1016\/S0304-3975(02)00010-5","volume":"281","author":"G Boudol","year":"2002","unstructured":"Boudol, G., Castellani, I.: Noninterference for concurrent programs and thread systems. Theor. Comput. Sci. 281(1\u20132), 109\u2013130 (2002)","journal-title":"Theor. Comput. Sci."},{"key":"3_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"68","DOI":"10.1007\/978-3-662-49635-0_4","volume-title":"Principles of Security and Trust","author":"J Breitner","year":"2016","unstructured":"Breitner, J., Graf, J., Hecker, M., Mohr, M., Snelting, G.: On improvements of low-deterministic security. In: Piessens, F., Vigan\u00f2, L. (eds.) POST 2016. LNCS, vol. 9635, pp. 68\u201388. Springer, Heidelberg (2016). https:\/\/doi.org\/10.1007\/978-3-662-49635-0_4"},{"key":"3_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"116","DOI":"10.1007\/978-3-642-41488-6_8","volume-title":"Secure IT Systems","author":"P Buiras","year":"2013","unstructured":"Buiras, P., Russo, A.: Lazy programs leak secrets. In: Riis Nielson, H., Gollmann, D. (eds.) NordSec 2013. LNCS, vol. 8208, pp. 116\u2013122. Springer, Heidelberg (2013). https:\/\/doi.org\/10.1007\/978-3-642-41488-6_8"},{"key":"3_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"420","DOI":"10.1007\/978-3-662-54434-1_16","volume-title":"Programming Languages and Systems","author":"T Dinsdale-Young","year":"2017","unstructured":"Dinsdale-Young, T., da Rocha Pinto, P., Andersen, K.J., Birkedal, L.: Caper: automatic verification for fine-grained concurrency. In: Yang, H. (ed.) ESOP 2017. LNCS, vol. 10201, pp. 420\u2013447. Springer, Heidelberg (2017). https:\/\/doi.org\/10.1007\/978-3-662-54434-1_16"},{"key":"3_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"299","DOI":"10.1007\/978-3-540-31982-5_19","volume-title":"Foundations of Software Science and Computational Structures","author":"R Focardi","year":"2005","unstructured":"Focardi, R., Rossi, S., Sabelfeld, A.: Bridging language-based and process calculi security. In: Sassone, V. (ed.) FoSSaCS 2005. LNCS, vol. 3441, pp. 299\u2013315. Springer, Heidelberg (2005). https:\/\/doi.org\/10.1007\/978-3-540-31982-5_19"},{"issue":"3","key":"3_CR14","doi-asserted-by":"publisher","first-page":"263","DOI":"10.1007\/s10207-014-0257-6","volume":"14","author":"D Giffhorn","year":"2015","unstructured":"Giffhorn, D., Snelting, G.: A new algorithm for low-deterministic security. Int. J. Inf. Secur. 14(3), 263\u2013287 (2015)","journal-title":"Int. J. Inf. Secur."},{"key":"3_CR15","doi-asserted-by":"crossref","unstructured":"Goguen, J.A., Meseguer, J.: Security policies and security models: In: Security and Privacy (1982)","DOI":"10.1109\/SP.1982.10014"},{"key":"3_CR16","unstructured":"Huisman, M., Worah, P., Sunesen, K.: A temporal logic characterisation of observational determinism. In: CSFW (2006)"},{"key":"3_CR17","doi-asserted-by":"crossref","unstructured":"Hunt, S., Sands, D.: On flow-sensitive security types. In: POPL (2006)","DOI":"10.1145\/1111037.1111045"},{"key":"3_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"327","DOI":"10.1007\/978-3-642-11957-6_18","volume-title":"Programming Languages and Systems","author":"D King","year":"2010","unstructured":"King, D., Jha, S., Muthukumaran, D., Jaeger, T., Jha, S., Seshia, S.A.: Automating security mediation placement. In: Gordon, A.D. (ed.) ESOP 2010. LNCS, vol. 6012, pp. 327\u2013344. Springer, Heidelberg (2010). https:\/\/doi.org\/10.1007\/978-3-642-11957-6_18"},{"issue":"2\u20133","key":"3_CR19","doi-asserted-by":"publisher","first-page":"107","DOI":"10.1007\/s10207-007-0016-z","volume":"6","author":"B K\u00f6pf","year":"2007","unstructured":"K\u00f6pf, B., Mantel, H.: Transformational typing and unification for automatically correcting insecure programs. Int. J. Inf. Secur. 6(2\u20133), 107\u2013131 (2007)","journal-title":"Int. J. Inf. Secur."},{"key":"3_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"45","DOI":"10.1007\/978-3-319-71237-6_3","volume-title":"Programming Languages and Systems","author":"X Li","year":"2017","unstructured":"Li, X., Mantel, H., Tasch, M.: Taming message-passing communication in compositional reasoning about confidentiality. In: Chang, B.-Y.E. (ed.) APLAS 2017. LNCS, vol. 10695, pp. 45\u201366. Springer, Cham (2017). https:\/\/doi.org\/10.1007\/978-3-319-71237-6_3"},{"key":"3_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"141","DOI":"10.1007\/978-3-540-71316-6_11","volume-title":"Programming Languages and Systems","author":"H Mantel","year":"2007","unstructured":"Mantel, H., Reinhard, A.: Controlling the what and where of declassification in language-based security. In: De Nicola, R. (ed.) ESOP 2007. LNCS, vol. 4421, pp. 141\u2013156. Springer, Heidelberg (2007). https:\/\/doi.org\/10.1007\/978-3-540-71316-6_11"},{"issue":"4","key":"3_CR22","doi-asserted-by":"publisher","first-page":"615","DOI":"10.3233\/JCS-2003-11406","volume":"11","author":"H Mantel","year":"2003","unstructured":"Mantel, H., Sabelfeld, A.: A unifying approach to the security of distributed and multi-threaded programs. J. Comput. Secur. 11(4), 615\u2013676 (2003)","journal-title":"J. Comput. Secur."},{"key":"3_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"447","DOI":"10.1007\/978-3-319-24174-6_23","volume-title":"Computer Security \u2013 ESORICS 2015","author":"H Mantel","year":"2015","unstructured":"Mantel, H., Starostin, A.: Transforming out timing leaks, more or less. In: Pernul, G., Ryan, P.Y.A., Weippl, E. (eds.) ESORICS 2015. LNCS, vol. 9326, pp. 447\u2013467. Springer, Cham (2015). https:\/\/doi.org\/10.1007\/978-3-319-24174-6_23"},{"key":"3_CR24","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"116","DOI":"10.1007\/978-3-642-15497-3_8","volume-title":"Computer Security \u2013 ESORICS 2010","author":"H Mantel","year":"2010","unstructured":"Mantel, H., Sudbrock, H.: Flexible scheduler-independent security. In: Gritzalis, D., Preneel, B., Theoharidou, M. (eds.) ESORICS 2010. LNCS, vol. 6345, pp. 116\u2013133. Springer, Heidelberg (2010). https:\/\/doi.org\/10.1007\/978-3-642-15497-3_8"},{"key":"3_CR25","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"94","DOI":"10.1007\/978-3-540-71410-1_8","volume-title":"Logic-Based Program Synthesis and Transformation","author":"H Mantel","year":"2007","unstructured":"Mantel, H., Sudbrock, H., Krau\u00dfer, T.: Combining different proof techniques for verifying information flow security. In: Puebla, G. (ed.) LOPSTR 2006. LNCS, vol. 4407, pp. 94\u2013110. Springer, Heidelberg (2007). https:\/\/doi.org\/10.1007\/978-3-540-71410-1_8"},{"key":"3_CR26","doi-asserted-by":"crossref","unstructured":"Mantel, H., Sands, D., Sudbrock, H.: Assumptions and guarantees for compositional noninterference. In: CSF (2011)","DOI":"10.1109\/CSF.2011.22"},{"issue":"1","key":"3_CR27","doi-asserted-by":"publisher","first-page":"37","DOI":"10.3233\/JCS-1992-1103","volume":"1","author":"J McLean","year":"1992","unstructured":"McLean, J.: Proving noninterference and functional correctness using traces. J. Comput. Secur. 1(1), 37\u201357 (1992)","journal-title":"J. Comput. Secur."},{"key":"3_CR28","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"156","DOI":"10.1007\/11734727_14","volume-title":"Information Security and Cryptology - ICISC 2005","author":"D Molnar","year":"2006","unstructured":"Molnar, D., Piotrowski, M., Schultz, D., Wagner, D.: The program counter security model: automatic detection and removal of control-flow side channel attacks. In: Won, D.H., Kim, S. (eds.) ICISC 2005. LNCS, vol. 3935, pp. 156\u2013168. Springer, Heidelberg (2006). https:\/\/doi.org\/10.1007\/11734727_14"},{"key":"3_CR29","doi-asserted-by":"crossref","unstructured":"Moore, S., Askarov, A., Chong, S.: Precise enforcement of progress-sensitive security. In: CCS (2012)","DOI":"10.1145\/2382196.2382289"},{"key":"3_CR30","doi-asserted-by":"crossref","unstructured":"Muller, S., Chong, S.: Towards a practical secure concurrent language. In: OOPSLA (2012)","DOI":"10.1145\/2384616.2384621"},{"key":"3_CR31","doi-asserted-by":"crossref","unstructured":"Murray, T.C., Sison, R., Pierzchalski, E., Rizkallah, C.: Compositional verification and refinement of concurrent value-dependent noninterference. In: CSF (2016)","DOI":"10.1109\/CSF.2016.36"},{"key":"3_CR32","doi-asserted-by":"crossref","unstructured":"Myers, A.C.: JFlow: practical mostly-static information flow control. In: POPL (1999)","DOI":"10.1145\/292540.292561"},{"key":"3_CR33","unstructured":"O\u2019Neill, K.R., Clarkson, M.R., Chong, S.: Information-flow security for interactive programs. In: CSFW (2006)"},{"key":"3_CR34","doi-asserted-by":"crossref","unstructured":"Parkinson, M.J., Bierman, G.M.: Separation logic and abstraction. In: POPL (2005)","DOI":"10.1145\/1040305.1040326"},{"key":"3_CR35","doi-asserted-by":"crossref","unstructured":"Pedersen, M.V., Askarov, A.: From trash to treasure: timing-sensitive garbage collection. In: Security and Privacy (2017)","DOI":"10.1109\/SP.2017.64"},{"key":"3_CR36","unstructured":"Reynolds, J.C.: Separation logic: a logic for shared mutable data structures. In: LICS (2002)"},{"key":"3_CR37","doi-asserted-by":"crossref","unstructured":"Roscoe, A.W.: CSP and determinism in security modelling. In: Security and Privacy (1995)","DOI":"10.1109\/SECPRI.1995.398927"},{"key":"3_CR38","doi-asserted-by":"crossref","unstructured":"Russo, A., Sabelfeld, A.: Securing interaction between threads and the scheduler. In: CSFW (2006)","DOI":"10.1109\/CSFW.2006.29"},{"key":"3_CR39","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"120","DOI":"10.1007\/978-3-540-77505-8_10","volume-title":"Advances in Computer Science - ASIAN 2006. Secure Software and Related Issues","author":"A Russo","year":"2007","unstructured":"Russo, A., Hughes, J., Naumann, D., Sabelfeld, A.: Closing internal timing channels by transformation. In: Okada, M., Satoh, I. (eds.) ASIAN 2006. LNCS, vol. 4435, pp. 120\u2013135. Springer, Heidelberg (2007). https:\/\/doi.org\/10.1007\/978-3-540-77505-8_10"},{"key":"3_CR40","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"225","DOI":"10.1007\/3-540-45575-2_22","volume-title":"Perspectives of System Informatics","author":"A Sabelfeld","year":"2001","unstructured":"Sabelfeld, A.: The impact of synchronisation on secure information flow in concurrent programs. In: Bj\u00f8rner, D., Broy, M., Zamulin, A.V. (eds.) PSI 2001. LNCS, vol. 2244, pp. 225\u2013239. Springer, Heidelberg (2001). https:\/\/doi.org\/10.1007\/3-540-45575-2_22"},{"key":"3_CR41","doi-asserted-by":"crossref","unstructured":"Sabelfeld, A., Sands, D.: Probabilistic noninterference for multi-threaded programs. In: CSFW (2000)","DOI":"10.1109\/CSFW.2000.856937"},{"key":"3_CR42","unstructured":"Saraswat, V., Bloom, B., Peshansky, I., Tardieu, O., Grove, D.: X10 language specification. Technical report, IBM, January 2012"},{"key":"3_CR43","doi-asserted-by":"crossref","unstructured":"Smith, G.: Probabilistic noninterference through weak probabilistic bisimulation. In: CSFW (2003)","DOI":"10.1109\/CSFW.2003.1212701"},{"key":"3_CR44","doi-asserted-by":"crossref","unstructured":"Smith, G., Volpano, D.M.: Secure information flow in a multi-threaded imperative language. In: POPL (1998)","DOI":"10.1145\/268946.268975"},{"key":"3_CR45","doi-asserted-by":"crossref","unstructured":"Stefan, D., Russo, A., Buiras, P., Levy, A., Mitchell, J.C., Mazi\u00e8res, D.: Addressing covert termination and timing channels in concurrent information flow systems. In: ICFP (2012)","DOI":"10.1145\/2364527.2364557"},{"key":"3_CR46","doi-asserted-by":"crossref","unstructured":"Terauchi, T.: A type system for observational determinism. In: CSF (2008)","DOI":"10.1109\/CSF.2008.9"},{"issue":"1","key":"3_CR47","doi-asserted-by":"publisher","first-page":"231","DOI":"10.3233\/JCS-1999-72-305","volume":"7","author":"DM Volpano","year":"1999","unstructured":"Volpano, D.M., Smith, G.: Probabilistic noninterference in a concurrent language. J. Comput. Secur. 7(1), 231\u2013253 (1999)","journal-title":"J. Comput. Secur."},{"key":"3_CR48","doi-asserted-by":"crossref","unstructured":"Volpano, D.M., Smith, G.: Verifying secrets and relative secrecy, In: POPL (2000)","DOI":"10.1145\/325694.325729"},{"key":"3_CR49","doi-asserted-by":"crossref","unstructured":"Zdancewic, S., Myers, A.C.: Observational determinism for concurrent program security. In: CSFW (2003)","DOI":"10.1109\/CSFW.2003.1212703"},{"key":"3_CR50","doi-asserted-by":"crossref","unstructured":"Zhang, D., Askarov, A., Myers, A.C.: Language-based control and mitigation of timing channels. In: PLDI (2012)","DOI":"10.1145\/2254064.2254078"},{"key":"3_CR51","series-title":"IFIP International Federation for Information Processing","doi-asserted-by":"publisher","first-page":"27","DOI":"10.1007\/0-387-24098-5_3","volume-title":"Formal Aspects in Security and Trust","author":"L Zheng","year":"2005","unstructured":"Zheng, L., Myers, A.C.: Dynamic security labels and noninterference (extended abstract). In: Dimitrakos, T., Martinelli, F. (eds.) Formal Aspects in Security and Trust. IIFIP, vol. 173, pp. 27\u201340. Springer, Boston, MA (2005). https:\/\/doi.org\/10.1007\/0-387-24098-5_3"}],"container-title":["Lecture Notes in Computer Science","Principles of Security and Trust"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-89722-6_3","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,10,31]],"date-time":"2020-10-31T18:55:17Z","timestamp":1604170517000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-89722-6_3"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2018]]},"ISBN":["9783319897219","9783319897226"],"references-count":51,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-89722-6_3","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2018]]}}}