{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,27]],"date-time":"2025-03-27T11:42:18Z","timestamp":1743075738304,"version":"3.40.3"},"publisher-location":"Cham","reference-count":34,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319661964"},{"type":"electronic","value":"9783319661971"}],"license":[{"start":{"date-parts":[[2017,1,1]],"date-time":"2017-01-01T00:00:00Z","timestamp":1483228800000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2017]]},"DOI":"10.1007\/978-3-319-66197-1_19","type":"book-chapter","created":{"date-parts":[[2017,8,11]],"date-time":"2017-08-11T21:02:30Z","timestamp":1502485350000},"page":"300-315","source":"Crossref","is-referenced-by-count":7,"title":["Modular Verification of Information Flow Security in Component-Based Systems"],"prefix":"10.1007","author":[{"given":"Simon","family":"Greiner","sequence":"first","affiliation":[]},{"given":"Martin","family":"Mohr","sequence":"additional","affiliation":[]},{"given":"Bernhard","family":"Beckert","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2017,8,13]]},"reference":[{"volume-title":"Deductive Software Verification - The KeY Book: From Theory to Practice","year":"2016","key":"19_CR1","unstructured":"Ahrendt, W., Beckert, B., Bubel, R., H\u00e4hnle, R., Schmitt, P.H., Ulbrich, M. (eds.): Deductive Software Verification - The KeY Book: From Theory to Practice. Springer, Heidelberg (2016)"},{"key":"19_CR2","doi-asserted-by":"crossref","unstructured":"Askarov, A., Chong, S., Mantel, H.: Hybrid monitors for concurrent noninterference. In: IEEE 28th Computer Security Foundations Symposium, CSF 2015, Verona, Italy, 13\u201317 July 2015","DOI":"10.1109\/CSF.2015.17"},{"key":"19_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"125","DOI":"10.1007\/978-3-540-71316-6_10","volume-title":"Programming Languages and Systems","author":"G Barthe","year":"2007","unstructured":"Barthe, G., Pichardie, D., Rezk, T.: A certified lightweight non-interference Java bytecode verifier. In: Nicola, R. (ed.) ESOP 2007. LNCS, vol. 4421, pp. 125\u2013140. Springer, Heidelberg (2007). doi: 10.1007\/978-3-540-71316-6_10"},{"key":"19_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"19","DOI":"10.1007\/978-3-319-14125-1_2","volume-title":"Logic-Based Program Synthesis and Transformation","author":"B Beckert","year":"2013","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, vol. 8901, pp. 19\u201337. Springer, Heidelberg (2013). doi: 10.1007\/978-3-319-14125-1_2"},{"key":"19_CR5","unstructured":"Chong, S., Vikram, K., Myers, A.C., et al.: SIF: Enforcing confidentiality and integrity in web applications. In: USENIX Security, vol. 7 (2007)"},{"key":"19_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"50","DOI":"10.1007\/978-3-642-01465-9_4","volume-title":"Formal Aspects in Security and Trust","author":"D Clark","year":"2009","unstructured":"Clark, D., Hunt, S.: Non-interference for deterministic interactive programs. In: Degano, P., Guttman, J., Martinelli, F. (eds.) FAST 2008. LNCS, vol. 5491, pp. 50\u201366. Springer, Heidelberg (2009). doi: 10.1007\/978-3-642-01465-9_4"},{"key":"19_CR7","doi-asserted-by":"publisher","first-page":"133","DOI":"10.1145\/1067625.806556","volume":"11","author":"E Cohen","year":"1977","unstructured":"Cohen, E.: Information transmission in computational systems. SIGOPS Oper. Syst. Rev. 11, 133\u2013139 (1977)","journal-title":"SIGOPS Oper. Syst. Rev."},{"key":"19_CR8","unstructured":"EJB 3.1 Expert Group: JSR 318: Enterprise JavaBeans, Version 3.1. Sun Microsystems (2009). https:\/\/jcp.org\/en\/jsr\/detail?id=366 . Accessed 31 Aug 2016"},{"key":"19_CR9","unstructured":"Ereth, S., Mantel, H., Perner, M.: Towards a common specification language for information-flow security in RS3 and beyond: RIFL 1.0 - the language. Technical Report TUD-CS-2014-0115, TU Darmstadt (2014)"},{"key":"19_CR10","doi-asserted-by":"crossref","unstructured":"Goguen, J.A., Meseguer, J.: Security policies and security models. In: IEEE Security and Privacy (1982)","DOI":"10.1109\/SP.1982.10014"},{"key":"19_CR11","unstructured":"Graf, J., Hecker, M., Mohr, M.: Using Joana for information flow control in Java programs - a practical guide. In: ATPS, February 2013"},{"key":"19_CR12","doi-asserted-by":"crossref","unstructured":"Greiner, S., Grahl, D.: Non-interference with what-declassification in component-based systems. In: CSF (2016)","DOI":"10.1109\/CSF.2016.25"},{"key":"19_CR13","doi-asserted-by":"publisher","first-page":"300","DOI":"10.1007\/978-3-319-66197-1_19","volume-title":"Software Engineering and Formal Methods","author":"Simon Greiner","year":"2017","unstructured":"Greiner, S., Mohr, M., Beckert, B.: Modular verification of information flow security in component-based systems - proofs and proof of concept (2017)"},{"key":"19_CR14","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. Int. J. Inf. Secur. 8, 399\u2013422 (2009)","journal-title":"Int. J. Inf. Secur."},{"key":"19_CR15","unstructured":"IBM Research: T.J. Watson Library for Analysis (WALA). http:\/\/wala.sf.net"},{"key":"19_CR16","doi-asserted-by":"crossref","unstructured":"Johnson, A., Waye, L., Moore, S., Chong, S.: Exploring and enforcing security guarantees via program dependence graphs. In: PLDI, June 2015","DOI":"10.1145\/2737924.2737957"},{"key":"19_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"268","DOI":"10.1007\/11813040_19","volume-title":"FM 2006: Formal Methods","author":"IT Kassios","year":"2006","unstructured":"Kassios, I.T.: Dynamic frames: support for framing, dependencies and sharing without restrictions. In: Misra, J., Nipkow, T., Sekerinski, E. (eds.) FM 2006. LNCS, vol. 4085, pp. 268\u2013283. Springer, Heidelberg (2006). doi: 10.1007\/11813040_19"},{"key":"19_CR18","doi-asserted-by":"crossref","unstructured":"K\u00fcsters, R., Truderung, T., Beckert, B., Bruns, D., Kirsten, M., Mohr, M.: A hybrid approach for proving noninterference of Java programs. In: CSF, July 2015","DOI":"10.1109\/CSF.2015.28"},{"key":"19_CR19","series-title":"IFIP Advances in Information and Communication Technology","doi-asserted-by":"publisher","first-page":"371","DOI":"10.1007\/978-3-319-18467-8_25","volume-title":"ICT Systems Security and Privacy Protection","author":"E Lovat","year":"2015","unstructured":"Lovat, E., Fromm, A., Mohr, M., Pretschner, A.: SHRIFT system-wide hybrid information flow tracking. In: Federrath, H., Gollmann, D. (eds.) SEC 2015. IAICT, vol. 455, pp. 371\u2013385. Springer, Cham (2015). doi: 10.1007\/978-3-319-18467-8_25"},{"key":"19_CR20","doi-asserted-by":"crossref","unstructured":"Mantel, H.: Possibilistic definitions of security \u2013 an assembly kit. In: CSFW (2000)","DOI":"10.1109\/CSFW.2000.856936"},{"key":"19_CR21","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"},{"key":"19_CR22","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":"19_CR23","doi-asserted-by":"crossref","unstructured":"Myers, A.C.: JFlow: Practical mostly-static information flow control. In: Proceedings of the 26th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (1999)","DOI":"10.1145\/292540.292561"},{"key":"19_CR24","doi-asserted-by":"crossref","unstructured":"Nanevski, A., Banerjee, A., Garg, D.: Verification of information flow and access control policies with dependent types. In: IEEE Security and Privacy, May 2011","DOI":"10.1109\/SP.2011.12"},{"key":"19_CR25","unstructured":"O\u2019Neill, K.R., Clarkson, M.R., Chong, S.: Information-flow security for interactive programs. In: CSFW, Jul 2006"},{"key":"19_CR26","doi-asserted-by":"crossref","unstructured":"Rafnsson, W., Hedin, D., Sabelfeld, A.: Securing interactive programs. In: CSF (2012)","DOI":"10.1109\/CSF.2012.15"},{"key":"19_CR27","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"376","DOI":"10.1007\/3-540-45789-5_27","volume-title":"Static Analysis","author":"A Sabelfeld","year":"2002","unstructured":"Sabelfeld, A., Mantel, H.: Static confidentiality enforcement for distributed programs. In: Hermenegildo, M.V., Puebla, G. (eds.) SAS 2002. LNCS, vol. 2477, pp. 376\u2013394. Springer, Heidelberg (2002). doi: 10.1007\/3-540-45789-5_27"},{"key":"19_CR28","doi-asserted-by":"publisher","first-page":"59","DOI":"10.1023\/A:1011553200337","volume":"14","author":"A Sabelfeld","year":"2001","unstructured":"Sabelfeld, A., Sands, D.: A PER model of secure information flow in sequential programs. Higher-Order Symbolic Comput. 14, 59\u201391 (2001)","journal-title":"Higher-Order Symbolic Comput."},{"key":"19_CR29","doi-asserted-by":"publisher","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. J. Comput. Secur. 17, 517\u2013548 (2009)","journal-title":"J. Comput. Secur."},{"key":"19_CR30","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). doi: 10.1007\/978-3-642-31762-0_15"},{"key":"19_CR31","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"579","DOI":"10.1007\/978-3-319-06410-9_39","volume-title":"FM 2014: Formal Methods","author":"C Scheben","year":"2014","unstructured":"Scheben, C., Schmitt, P.H.: Efficient self-composition for weakest precondition calculi. In: Jones, C., Pihlajasaari, P., Sun, J. (eds.) FM 2014. LNCS, vol. 8442, pp. 579\u2013594. Springer, Cham (2014). doi: 10.1007\/978-3-319-06410-9_39"},{"key":"19_CR32","doi-asserted-by":"crossref","unstructured":"Sheldon, M.A., Gifford, D.K.: Static dependent types for first class modules. In: Proceedings of the 1990 ACM Conference on LISP and Functional Programming. ACM (1990)","DOI":"10.1145\/91556.91577"},{"key":"19_CR33","unstructured":"Ranganath, V.-P., et al.: Indus. http:\/\/indus.projects.cs.ksu.edu\/ . Last visited on 01 Feb 2017"},{"key":"19_CR34","unstructured":"Wasserrab, D., Lohner, D.: Proving information flow noninterference by reusing a machine-checked correctness proof for slicing. In: VERIFY (2010)"}],"container-title":["Lecture Notes in Computer Science","Software Engineering and Formal Methods"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-66197-1_19","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,10,2]],"date-time":"2019-10-02T06:03:27Z","timestamp":1569996207000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-66197-1_19"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017]]},"ISBN":["9783319661964","9783319661971"],"references-count":34,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-66197-1_19","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2017]]}}}