{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,10,1]],"date-time":"2026-10-01T12:44:39Z","timestamp":1790858679963,"version":"4.1.0"},"publisher-location":"Berlin, Heidelberg","reference-count":21,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783642050886","type":"print"},{"value":"9783642050893","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2009]]},"DOI":"10.1007\/978-3-642-05089-3_49","type":"book-chapter","created":{"date-parts":[[2009,11,3]],"date-time":"2009-11-03T17:31:40Z","timestamp":1257269500000},"page":"773-789","source":"Crossref","is-referenced-by-count":13,"title":["Verifying Information Flow Control over Unbounded Processes"],"prefix":"10.1007","author":[{"given":"William R.","family":"Harris","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Nicholas A.","family":"Kidd","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Sagar","family":"Chaki","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Somesh","family":"Jha","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Thomas","family":"Reps","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","reference":[{"issue":"5","key":"49_CR1","doi-asserted-by":"publisher","first-page":"17","DOI":"10.1145\/1095809.1095813","volume":"39","author":"P. Efstathopoulos","year":"2005","unstructured":"Efstathopoulos, P., Krohn, M., VanDeBogart, S., Frey, C., Ziegler, D., Kohler, E., Mazi\u00e8res, D., Kaashoek, F., Morris, R.: Labels and event processes in the Asbestos operating system. SIGOPS Oper. Syst. Rev.\u00a039(5), 17\u201330 (2005)","journal-title":"SIGOPS Oper. Syst. Rev."},{"key":"49_CR2","unstructured":"Zeldovich, N., Boyd-Wickizer, S., Kohler, E., Mazi\u00e8res, D.: Making information flow explicit in HiStar. In: OSDI (2006)"},{"key":"49_CR3","doi-asserted-by":"crossref","unstructured":"Krohn, M., Yip, A., Brodsky, M., Cliffer, N., Kaashoek, M.F., Kohler, E., Morris, R.: Information flow control for standard os abstractions. In: SOSP (2007)","DOI":"10.1145\/1294261.1294293"},{"key":"49_CR4","unstructured":"Conover, M.: Analysis of the Windows Vista Security Model. Technical report, Symantec Corporation (2008)"},{"issue":"2-3","key":"49_CR5","doi-asserted-by":"publisher","first-page":"129","DOI":"10.1023\/B:FORM.0000040026.56959.91","volume":"25","author":"S. Chaki","year":"2004","unstructured":"Chaki, S., Clarke, E., Groce, A., Ouaknine, J., Strichman, O., Yorav, K.: Efficient verification of sequential and concurrent C programs. Form. Methods Syst. Des.\u00a025(2-3), 129\u2013166 (2004)","journal-title":"Form. Methods Syst. Des."},{"key":"49_CR6","series-title":"Lecture Notes in Computer Science","first-page":"198","volume-title":"VMCAI 2009","author":"N.A. Kidd","year":"2009","unstructured":"Kidd, N.A., Reps, T.W., Dolby, J., Vaziri, M.: Finding concurrency-related bugs using random isolation. In: Jones, N.D., M\u00fcller-Olm, M. (eds.) VMCAI 2009. LNCS, vol.\u00a05403, pp. 198\u2013213. Springer, Heidelberg (2009)"},{"key":"49_CR7","unstructured":"Apache: Apache, http:\/\/www.apache.org"},{"key":"49_CR8","unstructured":"ClamAV: ClamAV, http:\/\/www.clamav.net"},{"key":"49_CR9","unstructured":"OpenVPN: OpenVPN, http:\/\/www.openvpn.net"},{"key":"49_CR10","doi-asserted-by":"crossref","unstructured":"Chaudhuri, A., Naldurg, P., Rajamani, S.K., Ramalingam, G., Velaga, L.: EON: Modeling and analyzing dynamic access control systems with logic programs. In: CCS (2008)","DOI":"10.1145\/1455770.1455818"},{"key":"49_CR11","doi-asserted-by":"crossref","unstructured":"Krohn, M., Tromer, E.: Non-interference for a practical DIFC-based operating system. In: IEEE Symposium on Security and Privacy (2009)","DOI":"10.1109\/SP.2009.23"},{"issue":"3","key":"49_CR12","doi-asserted-by":"publisher","first-page":"217","DOI":"10.1145\/514188.514190","volume":"24","author":"M. Sagiv","year":"2002","unstructured":"Sagiv, M., Reps, T., Wilhelm, R.: Parametric shape analysis via 3-valued logic. ACM Trans. Program. Lang. Syst.\u00a024(3), 217\u2013298 (2002)","journal-title":"ACM Trans. Program. Lang. Syst."},{"key":"49_CR13","doi-asserted-by":"crossref","unstructured":"Harris, W.R., Kidd, N.A., Chaki, S., Jha, S., Reps, T.: Verifying information flow control over unbounded processes. Technical Report UW-CS-TR-1655, Univ. of Wisc (May 2009)","DOI":"10.1007\/978-3-642-05089-3_49"},{"key":"49_CR14","doi-asserted-by":"crossref","unstructured":"Necula, G., McPeak, S., Rahul, S., Weimer, W.: CIL: Intermediate language and tools for analysis and transformation of C programs (2002)","DOI":"10.1007\/3-540-45937-5_16"},{"key":"49_CR15","unstructured":"MoinMoin: The MoinMoin wiki engine (December 2006), http:\/\/moinmoin.wikiwikiweb.de"},{"issue":"4","key":"49_CR16","doi-asserted-by":"publisher","first-page":"11","DOI":"10.1145\/1314299.1314302","volume":"25","author":"S. Vandebogart","year":"2007","unstructured":"Vandebogart, S., Efstathopoulos, P., Kohler, E., Krohn, M., Frey, C., Ziegler, D., Kaashoek, F., Morris, R., Mazi\u00e8res, D.: Labels and Event Processes in the Asbestos Operating System. ACM Trans. Comput. Syst.\u00a025(4), 11 (2007)","journal-title":"ACM Trans. Comput. Syst."},{"key":"49_CR17","doi-asserted-by":"crossref","unstructured":"Yahav, E.: Verifying safety properties of concurrent java programs using 3-valued logic. In: POPL (2001)","DOI":"10.1145\/360204.360206"},{"issue":"7","key":"49_CR18","doi-asserted-by":"publisher","first-page":"504","DOI":"10.1145\/359636.359712","volume":"20","author":"D.E. Denning","year":"1977","unstructured":"Denning, D.E., Denning, P.J.: Certification of programs for secure information flow. Commun. ACM\u00a020(7), 504\u2013513 (1977)","journal-title":"Commun. ACM"},{"key":"49_CR19","doi-asserted-by":"crossref","unstructured":"Myers, A.C.: JFlow: practical mostly-static information flow control. In: POPL (1999)","DOI":"10.1145\/292540.292561"},{"key":"49_CR20","doi-asserted-by":"crossref","unstructured":"Guttman, J.D., Herzog, A.L., Ramsdell, J.D., Skorupka, C.W.: Verifying Information-Flow Goals in Security-Enhanced Linux. Journal of Computer Security (2005)","DOI":"10.3233\/JCS-2005-13105"},{"key":"49_CR21","unstructured":"Zhang, X., Edwards, A., Jaeger, T.: Using CQUAL for static analysis of authorization hook placement. In: USENIX Security Symposium, pp. 33\u201348 (2002)"}],"container-title":["Lecture Notes in Computer Science","FM 2009: Formal Methods"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-05089-3_49.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,11,23]],"date-time":"2020-11-23T21:47:41Z","timestamp":1606168061000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-05089-3_49"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2009]]},"ISBN":["9783642050886","9783642050893"],"references-count":21,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-05089-3_49","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2009]]}}}