{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,11,18]],"date-time":"2025-11-18T23:14:27Z","timestamp":1763507667467},"publisher-location":"Berlin, Heidelberg","reference-count":24,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642314230"},{"type":"electronic","value":"9783642314247"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2012]]},"DOI":"10.1007\/978-3-642-31424-7_41","type":"book-chapter","created":{"date-parts":[[2012,6,21]],"date-time":"2012-06-21T14:26:49Z","timestamp":1340288809000},"page":"581-598","source":"Crossref","is-referenced-by-count":10,"title":["Secure Programming via Visibly Pushdown Safety Games"],"prefix":"10.1007","author":[{"given":"William R.","family":"Harris","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Somesh","family":"Jha","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Thomas","family":"Reps","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"41_CR1","doi-asserted-by":"crossref","unstructured":"Abadi, M., Budiu, M., Erlingsson, \u00da., Ligatti, J.: Control-flow integrity. In: CCS (2005)","DOI":"10.1145\/1102120.1102165"},{"key":"41_CR2","doi-asserted-by":"crossref","unstructured":"Alur, R., Henzinger, T.A., Kupferman, O.: Alternating-time temporal logic. In: FOCS (1997)","DOI":"10.1007\/3-540-49213-5_2"},{"key":"41_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1102","DOI":"10.1007\/11523468_89","volume-title":"Automata, Languages and Programming","author":"R. Alur","year":"2005","unstructured":"Alur, R., Kumar, V., Madhusudan, P., Viswanathan, M.: Congruences for Visibly Pushdown Languages. In: Caires, L., Italiano, G.F., Monteiro, L., Palamidessi, C., Yung, M. (eds.) ICALP 2005. LNCS, vol.\u00a03580, pp. 1102\u20131114. Springer, Heidelberg (2005)"},{"key":"41_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"363","DOI":"10.1007\/3-540-36577-X_26","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"R. Alur","year":"2003","unstructured":"Alur, R., La Torre, S., Madhusudan, P.: Modular Strategies for Recursive Game Graphs. In: Garavel, H., Hatcliff, J. (eds.) TACAS 2003. LNCS, vol.\u00a02619, pp. 363\u2013378. Springer, Heidelberg (2003)"},{"key":"41_CR5","doi-asserted-by":"crossref","unstructured":"Alur, R., Madhusudan, P.: Visibly pushdown languages. In: STOC (2004)","DOI":"10.1145\/1007352.1007390"},{"key":"41_CR6","unstructured":"Bittau, A., Marchenko, P., Handley, M., Karp, B.: Wedge: Splitting applications into reduced-privilege compartments. In: NSDI (2008)"},{"issue":"7","key":"41_CR7","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":"41_CR8","doi-asserted-by":"crossref","unstructured":"Efstathopoulos, P., Kohler, E.: Manageable fine-grained information flow. In: EuroSys (2008)","DOI":"10.1145\/1352592.1352624"},{"key":"41_CR9","doi-asserted-by":"crossref","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. In: SOSP (2005)","DOI":"10.1145\/1095810.1095813"},{"key":"41_CR10","unstructured":"Erlingsson, \u00da., Schneider, F.B.: IRM enforcement of Java stack inspection. In: IEEE SP (2000)"},{"key":"41_CR11","unstructured":"FreeBSD 9.0-RELEASE announcement (January 2012), \n                    \n                      http:\/\/www.freebsd.org\/releases\/9.0R\/announce.html"},{"key":"41_CR12","doi-asserted-by":"crossref","unstructured":"Harris, W.R., Jha, S., Reps, T.: DIFC programs by automatic instrumentation. In: CCS (2010)","DOI":"10.1145\/1866307.1866340"},{"key":"41_CR13","unstructured":"Harris, W.R., Jha, S., Reps, T.: Programming for a capability system via safety games. Technical Report TR1705, University of Wisconsin-Madison (April 2012)"},{"key":"41_CR14","doi-asserted-by":"crossref","unstructured":"Harris, W.R., Jha, S., Reps, T.W.: Secure programming via visibly pushdown safety games. Technical Report TR1710, University of Wisconsin, Dept. of Computer Sciences (April 2012)","DOI":"10.1007\/978-3-642-31424-7_41"},{"key":"41_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"773","DOI":"10.1007\/978-3-642-05089-3_49","volume-title":"FM 2009: Formal Methods","author":"W.R. Harris","year":"2009","unstructured":"Harris, W.R., Kidd, N.A., Chaki, S., Jha, S., Reps, T.: Verifying Information Flow Control over Unbounded Processes. In: Cavalcanti, A., Dams, D.R. (eds.) FM 2009. LNCS, vol.\u00a05850, pp. 773\u2013789. Springer, Heidelberg (2009)"},{"key":"41_CR16","unstructured":"Izdebski, M.: bzip2 \u2018BZ2_decompress\u2019 function integer overflow vuln. (October 2011)"},{"key":"41_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"226","DOI":"10.1007\/11513988_23","volume-title":"Computer Aided Verification","author":"B. Jobstmann","year":"2005","unstructured":"Jobstmann, B., Griesmayer, A., Bloem, R.: Program Repair as a Game. In: Etessami, K., Rajamani, S.K. (eds.) CAV 2005. LNCS, vol.\u00a03576, pp. 226\u2013238. Springer, Heidelberg (2005)"},{"key":"41_CR18","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":"41_CR19","doi-asserted-by":"crossref","unstructured":"Madhusudan, P., Nam, W., Alur, R.: Symbolic computational techniques for solving games. Electr. Notes Theor. Comput. Sci.\u00a089(4) (2003)","DOI":"10.1016\/S1571-0661(05)82544-7"},{"key":"41_CR20","unstructured":"Naraine, R.: Symantec antivirus worm hole puts millions at risk. eWeek.com (2006)"},{"key":"41_CR21","unstructured":"Ubuntu sec. notice USN-709-1 (2009), \n                    \n                      http:\/\/www.ubuntu.com\/usn\/usn-709-1\/"},{"key":"41_CR22","unstructured":"Vuln. note VU#381508 (July 2011), \n                    \n                      http:\/\/www.kb.cert.org\/vuls\/id\/381508"},{"key":"41_CR23","unstructured":"Watson, R.N.M., Anderson, J., Laurie, B., Kennaway, K.: Capsicum: Practical capabilities for UNIX. In: USENIX Security (2010)"},{"key":"41_CR24","unstructured":"Zeldovich, N., Boyd-Wickizer, S., Kohler, E., Mazi\u00e8res, D.: Making information flow explicit in HiStar. In: OSDI (2006)"}],"container-title":["Lecture Notes in Computer Science","Computer Aided Verification"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-31424-7_41.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,5,4]],"date-time":"2021-05-04T12:00:01Z","timestamp":1620129601000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-31424-7_41"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2012]]},"ISBN":["9783642314230","9783642314247"],"references-count":24,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-31424-7_41","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2012]]}}}