{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,5,30]],"date-time":"2025-05-30T23:40:01Z","timestamp":1748648401321,"version":"3.41.0"},"publisher-location":"Cham","reference-count":26,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319255262"},{"type":"electronic","value":"9783319255279"}],"license":[{"start":{"date-parts":[[2015,1,1]],"date-time":"2015-01-01T00:00:00Z","timestamp":1420070400000},"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":[[2015]]},"DOI":"10.1007\/978-3-319-25527-9_6","type":"book-chapter","created":{"date-parts":[[2015,10,7]],"date-time":"2015-10-07T11:08:43Z","timestamp":1444216123000},"page":"47-65","source":"Crossref","is-referenced-by-count":3,"title":["Hoare Logic for Disjunctive Information Flow"],"prefix":"10.1007","author":[{"given":"Hanne Riis","family":"Nielson","sequence":"first","affiliation":[]},{"given":"Flemming","family":"Nielson","sequence":"additional","affiliation":[]},{"given":"Ximeng","family":"Li","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2015,11,20]]},"reference":[{"key":"6_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"369","DOI":"10.1007\/978-3-642-28641-4_20","volume-title":"Principles of Security and Trust","author":"T Amtoft","year":"2012","unstructured":"Amtoft, T., Dodds, J., Zhang, Z., Appel, A., Beringer, L., Hatcliff, J., Ou, X., Cousino, A.: A certificate infrastructure for machine-checked proofs of conditional information flow. In: Degano, P., Guttman, J.D. (eds.) Principles of Security and Trust. LNCS, vol. 7215, pp. 369\u2013389. Springer, Heidelberg (2012)"},{"issue":"1","key":"6_CR2","doi-asserted-by":"publisher","first-page":"56","DOI":"10.1145\/357084.357088","volume":"2","author":"GR Andrews","year":"1980","unstructured":"Andrews, G.R., Reitman, R.P.: An axiomatic approach to information flow in programs. ACM Trans. Program. Lang. Syst. 2(1), 56\u201376 (1980)","journal-title":"ACM Trans. Program. Lang. Syst."},{"issue":"4","key":"6_CR3","doi-asserted-by":"publisher","first-page":"431","DOI":"10.1145\/357146.357150","volume":"3","author":"KR Apt","year":"1981","unstructured":"Apt, K.R.: Ten years of Hoare\u2019s logic: A survey - part I. ACM Trans. Program. Lang. Syst. 3(4), 431\u2013483 (1981)","journal-title":"ACM Trans. Program. Lang. Syst."},{"key":"6_CR4","doi-asserted-by":"publisher","first-page":"83","DOI":"10.1016\/0304-3975(83)90066-X","volume":"28","author":"KR Apt","year":"1984","unstructured":"Apt, K.R.: Ten years of Hoare\u2019s logic: a survey part II: nondeterminism. Theoret. Comput. Sci. 28, 83\u2013109 (1984)","journal-title":"Theoret. Comput. Sci."},{"unstructured":"Bell, D.E., LaPadula, L.J.: Secure computer systems: a mathematical model. Technical report, MITRE Corporation (1973)","key":"6_CR5"},{"unstructured":"Biba, K.J.: Integrity considerations for secure computer systems. Technical report, MITRE Corporation (1977)","key":"6_CR6"},{"key":"6_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"20","DOI":"10.1007\/978-3-642-01465-9_2","volume-title":"Formal Aspects in Security and Trust","author":"G Boudol","year":"2009","unstructured":"Boudol, G.: Secure information flow as a safety property. In: Guttman, J., Degano, P., Martinelli, F. (eds.) FAST 2008. LNCS, vol. 5491, pp. 20\u201334. Springer, Heidelberg (2009)"},{"doi-asserted-by":"crossref","unstructured":"Broberg, N., Sands, D.: Paralocks: role-based information flow control and beyond. In: 37 th POPL, pp. 431\u2013444. ACM (2010)","key":"6_CR8","DOI":"10.1145\/1706299.1706349"},{"doi-asserted-by":"crossref","unstructured":"Chong, S., Myers, A.C.: Decentralized robustness. In: 19\u2019th CSFW, pp. 242\u2013256. IEEE Computer Society (2006)","key":"6_CR9","DOI":"10.1109\/CSFW.2006.11"},{"unstructured":"Airlines Electronic Engineering Committee. ARINC 811: Commercial aircraft information security concepts of operation and process framework. Technical report (2005)","key":"6_CR10"},{"key":"6_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":"\u00c1 Darvas","year":"2005","unstructured":"Darvas, \u00c1., 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)"},{"issue":"7","key":"6_CR12","doi-asserted-by":"publisher","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. CACM 20(7), 504\u2013513 (1977)","journal-title":"CACM"},{"unstructured":"Greve, D.: Data flow logic: Analyzing Information Flow Properties of C Programs. Rockwell Collins (2011)","key":"6_CR13"},{"unstructured":"Hedin, D., Sabelfeld, A.: A Perspective on Information-Flow Control. Marktoberdorf Summerschool (2011)","key":"6_CR14"},{"doi-asserted-by":"crossref","unstructured":"Montagu, B., Pierce, B.C., Pollack, R.: A theory of information-flow labels. In: 26th CSF, pp. 3\u201317. IEEE Computer Society (2013)","key":"6_CR15","DOI":"10.1109\/CSF.2013.8"},{"doi-asserted-by":"crossref","unstructured":"M\u00fcller, K., Paulitsch, M., Tverdyshev, S., Blasum, H.: MILS-related information flow control in the avionic domain: a view on security-enhancing software architectures. In: IEEE\/IFIP International Conference on Dependable Systems and Networks Workshops, DSN 2012, pp. 1\u20136. IEEE (2012)","key":"6_CR16","DOI":"10.1109\/DSNW.2012.6264665"},{"doi-asserted-by":"crossref","unstructured":"Myers, A.C., Liskov, B.: A decentralized model for information flow control. In: 16th ACM Symposium on Operating Systems Principles, pp. 129\u2013142 (1997)","key":"6_CR17","DOI":"10.1145\/269005.266669"},{"issue":"4","key":"6_CR18","doi-asserted-by":"publisher","first-page":"410","DOI":"10.1145\/363516.363526","volume":"9","author":"AC Myers","year":"2000","unstructured":"Myers, A.C., Liskov, B.: Protecting privacy using the decentralized label model. ACM Trans. Softw. Eng. Methodol. 9(4), 410\u2013442 (2000)","journal-title":"ACM Trans. Softw. Eng. Methodol."},{"issue":"3","key":"6_CR19","doi-asserted-by":"publisher","first-page":"359","DOI":"10.1145\/3916.3917","volume":"7","author":"F Nielson","year":"1985","unstructured":"Nielson, F.: Program transformations in a denotational setting. ACM Trans. Program. Lang. Syst. 7(3), 359\u2013379 (1985)","journal-title":"ACM Trans. Program. Lang. Syst."},{"key":"6_CR20","first-page":"17","volume":"60\u201361","author":"GD Plotkin","year":"2004","unstructured":"Plotkin, G.D.: A structural approach to operational semantics. J. Logic Algebraic Program. 60\u201361, 17\u2013139 (2004)","journal-title":"J. Logic Algebraic Program."},{"unstructured":"Rushby, J.: Separation and Integration in MILS (The MILS Constitution). Technical report SRI-CSL-08-XX, SRI International, February 2008","key":"6_CR21"},{"key":"6_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"352","DOI":"10.1007\/978-3-642-11486-1_30","volume-title":"Perspectives of Systems Informatics","author":"A Sabelfeld","year":"2010","unstructured":"Sabelfeld, A., Russo, A.: From dynamic to static and back: riding the roller coaster of information-flow control research. In: Virbitskaite, I., Voronkov, A., Pnueli, A. (eds.) PSI 2009. LNCS, vol. 5947, pp. 352\u2013365. Springer, Heidelberg (2010)"},{"key":"6_CR23","doi-asserted-by":"publisher","first-page":"347","DOI":"10.1016\/0304-3975(88)90033-3","volume":"58","author":"C Stirling","year":"1988","unstructured":"Stirling, C.: A generalization of Owicki-Gries\u2019s Hoare logic for a concurrent while language. Theoret. Comput. Sci. 58, 347\u2013359 (1988)","journal-title":"Theoret. Comput. Sci."},{"issue":"2\/3","key":"6_CR24","doi-asserted-by":"publisher","first-page":"167","DOI":"10.3233\/JCS-1996-42-304","volume":"4","author":"DM Volpano","year":"1996","unstructured":"Volpano, D.M., Irvine, C.E., Smith, G.: A sound type system for secure flow analysis. J. Comput. Secur. 4(2\/3), 167\u2013188 (1996)","journal-title":"J. Comput. Secur."},{"key":"6_CR25","doi-asserted-by":"publisher","first-page":"381","DOI":"10.1007\/978-1-4419-1539-9_13","volume-title":"Design and Verification of Microprocessor Systems for High-Assurance Applications","author":"MW Whalen","year":"2010","unstructured":"Whalen, M.W., Greve, D.A., Wagner, L.G.: Model checking information flow. In: Hardin, D.S. (ed.) Design and Verification of Microprocessor Systems for High-Assurance Applications, pp. 381\u2013428. Springer, New York (2010)"},{"unstructured":"Zheng, L., Myers, A.C.: End-to-end availability policies and noninterference. In: 18\u2019th CSFW, pp. 272\u2013286. IEEE Computer Society (2005)","key":"6_CR26"}],"container-title":["Lecture Notes in Computer Science","Programming Languages with Applications to Biology and Security"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-25527-9_6","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,5,30]],"date-time":"2025-05-30T22:59:00Z","timestamp":1748645940000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-25527-9_6"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2015]]},"ISBN":["9783319255262","9783319255279"],"references-count":26,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-25527-9_6","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2015]]}}}