{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,11,18]],"date-time":"2025-11-18T12:14:29Z","timestamp":1763468069829,"version":"3.40.2"},"publisher-location":"Berlin, Heidelberg","reference-count":31,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642286407"},{"type":"electronic","value":"9783642286414"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2012]]},"DOI":"10.1007\/978-3-642-28641-4_20","type":"book-chapter","created":{"date-parts":[[2012,3,22]],"date-time":"2012-03-22T21:10:46Z","timestamp":1332450646000},"page":"369-389","source":"Crossref","is-referenced-by-count":18,"title":["A Certificate Infrastructure for Machine-Checked Proofs of Conditional Information Flow"],"prefix":"10.1007","author":[{"given":"Torben","family":"Amtoft","sequence":"first","affiliation":[]},{"given":"Josiah","family":"Dodds","sequence":"additional","affiliation":[]},{"given":"Zhi","family":"Zhang","sequence":"additional","affiliation":[]},{"given":"Andrew","family":"Appel","sequence":"additional","affiliation":[]},{"given":"Lennart","family":"Beringer","sequence":"additional","affiliation":[]},{"given":"John","family":"Hatcliff","sequence":"additional","affiliation":[]},{"given":"Xinming","family":"Ou","sequence":"additional","affiliation":[]},{"given":"Andrew","family":"Cousino","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"20_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"229","DOI":"10.1007\/978-3-540-68237-0_17","volume-title":"FM 2008: Formal Methods","author":"T. Amtoft","year":"2008","unstructured":"Amtoft, T., Hatcliff, J., Rodr\u00edguez, E., Robby, Hoag, J., Greve, D.A.: Specification and Checking of Software Contracts for Conditional Information Flow. In: Cuellar, J., Sere, K. (eds.) FM 2008. LNCS, vol.\u00a05014, pp. 229\u2013245. Springer, Heidelberg (2008)"},{"key":"20_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"43","DOI":"10.1007\/978-3-642-11957-6_4","volume-title":"Programming Languages and Systems","author":"T. Amtoft","year":"2010","unstructured":"Amtoft, T., Hatcliff, J., Rodr\u00edguez, E.: Precise and Automated Contract-Based Reasoning for Verification and Certification of Information Flow Properties of Programs with Arrays. In: Gordon, A.D. (ed.) ESOP 2010. LNCS, vol.\u00a06012, pp. 43\u201363. Springer, Heidelberg (2010)"},{"key":"20_CR3","unstructured":"Barnes, J., Chapman, R., Johnson, R., Widmaier, J., Cooper, D., Everett, B.: Engineering the Tokeneer enclave protection software. In: Proceedings of the IEEE International Symposium on Secure Software Engineering (ISSSE 2006). IEEE Press (2006)"},{"key":"20_CR4","doi-asserted-by":"crossref","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 (2012), http:\/\/santos.cis.ksu.edu\/papers\/Amtoft-al-POST12\/","DOI":"10.1007\/978-3-642-28641-4_20"},{"key":"20_CR5","doi-asserted-by":"crossref","unstructured":"Amtoft, T., Banerjee, A.: Verification condition generation for conditional information flow. In: 5th ACM Workshop on Formal Methods in Security Engineering (FMSE 2007), pp. 2\u201311. George Mason University, ACM (2007)","DOI":"10.1145\/1314436.1314438"},{"key":"20_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"135","DOI":"10.1007\/978-3-642-25379-9_12","volume-title":"Certified Programs and Proofs","author":"M. Armand","year":"2011","unstructured":"Armand, M., Faure, G., Gr\u00e9goire, B., Keller, C., Th\u00e9ry, L., Werner, B.: A Modular Integration of SAT\/SMT Solvers to Coq through Proof Witnesses. In: Jouannaud, J.-P., Shao, Z. (eds.) CPP 2011. LNCS, vol.\u00a07086, pp. 135\u2013150. Springer, Heidelberg (2011)"},{"key":"20_CR7","doi-asserted-by":"crossref","unstructured":"Heitmeyer, C.L., Archer, M., Leonard, E.I., McLean, J.: Formal specification and verification of data separation in a separation kernel for an embedded system. In: 13th ACM Conference on Computer and Communications Security (CCS 2006), pp. 346\u2013355 (2006)","DOI":"10.1145\/1180405.1180448"},{"key":"20_CR8","doi-asserted-by":"publisher","first-page":"37","DOI":"10.1145\/2363.2366","volume":"7","author":"J.F. Bergeretti","year":"1985","unstructured":"Bergeretti, J.F., Carr\u00e9, B.A.: Information-flow and data-flow analysis of while-programs. ACM Transactions on Programming Languages and Systems\u00a07, 37\u201361 (1985)","journal-title":"ACM Transactions on Programming Languages and Systems"},{"key":"20_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"607","DOI":"10.1007\/BFb0030629","volume-title":"TAPSOFT\u201997: Theory and Practice of Software Development","author":"D.M. Volpano","year":"1997","unstructured":"Volpano, D.M., Smith, G.: A Type-Based Approach to Program Security. In: Bidoit, M., Dauchet, M. (eds.) CAAP 1997, FASE 1997, and TAPSOFT 1997. LNCS, vol.\u00a01214, pp. 607\u2013621. Springer, Heidelberg (1997)"},{"key":"20_CR10","doi-asserted-by":"crossref","unstructured":"Chapman, R., Hilton, A.: Enforcing security and safety models with an information flow analysis tool. ACM SIGAda Ada Letters XXIV, 39\u201346 (2004)","DOI":"10.1145\/1046191.1032305"},{"key":"20_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"100","DOI":"10.1007\/978-3-540-27864-1_10","volume-title":"Static Analysis","author":"T. Amtoft","year":"2004","unstructured":"Amtoft, T., Banerjee, A.: Information Flow Analysis in Logical Form. In: Giacobazzi, R. (ed.) SAS 2004. LNCS, vol.\u00a03148, pp. 100\u2013115. Springer, Heidelberg (2004)"},{"key":"20_CR12","doi-asserted-by":"crossref","unstructured":"Necula, G.C.: Proof-carrying code. In: POPL 1997, pp. 106\u2013119. ACM Press (1997)","DOI":"10.1145\/263699.263712"},{"key":"20_CR13","unstructured":"Appel, A.W.: Foundational proof-carrying code. In: LICS 2001. IEEE Computer Society (2001)"},{"key":"20_CR14","unstructured":"Sannella, D., Hofmann, M., Aspinall, D., Gilmore, S., Stark, I., Beringer, L., Loidl, H.W., MacKenzie, K., Momigliano, A., Shkaravska, O.: Mobile resource guarantees. In: van Eekelen, M.C.J.D. (ed.) Revised Selected Papers from the Sixth Symposium on Trends in Functional Programming (TFP 2005), Intellect, pp. 211\u2013226 (2007)"},{"key":"20_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/978-3-540-92188-2_1","volume-title":"Formal Methods for Components and Objects","author":"G. Barthe","year":"2008","unstructured":"Barthe, G., Cr\u00e9gut, P., Gr\u00e9goire, B., Jensen, T., Pichardie, D.: The MOBIUS Proof Carrying Code Infrastructure. In: de Boer, F.S., Bonsangue, M.M., Graf, S., de Roever, W.-P. (eds.) FMCO 2007. LNCS, vol.\u00a05382, pp. 1\u201324. Springer, Heidelberg (2008)"},{"key":"20_CR16","series-title":"LNAI","doi-asserted-by":"publisher","first-page":"347","DOI":"10.1007\/978-3-540-32275-7_23","volume-title":"Logic for Programming, Artificial Intelligence, and Reasoning","author":"L. Beringer","year":"2005","unstructured":"Beringer, L., Hofmann, M., Momigliano, A., Shkaravska, O.: Automatic Certification of Heap Consumption. In: Baader, F., Voronkov, A. (eds.) LPAR 2004. LNCS (LNAI), vol.\u00a03452, pp. 347\u2013362. Springer, Heidelberg (2005)"},{"key":"20_CR17","series-title":"LNAI","doi-asserted-by":"publisher","first-page":"380","DOI":"10.1007\/978-3-540-32275-7_25","volume-title":"Logic for Programming, Artificial Intelligence, and Reasoning","author":"E. Albert","year":"2005","unstructured":"Albert, E., Puebla, G., Hermenegildo, M.V.: Abstraction-Carrying Code. In: Baader, F., Voronkov, A. (eds.) LPAR 2004. LNCS (LNAI), vol.\u00a03452, pp. 380\u2013397. Springer, Heidelberg (2005)"},{"key":"20_CR18","series-title":"LNCS","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: De Nicola, R. (ed.) ESOP 2007. LNCS, vol.\u00a04421, pp. 125\u2013140. Springer, Heidelberg (2007)"},{"key":"20_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"326","DOI":"10.1007\/978-3-540-31987-0_23","volume-title":"Programming Languages and Systems","author":"M. Wildmoser","year":"2005","unstructured":"Wildmoser, M., Nipkow, T.: Asserting Bytecode Safety. In: Sagiv, M. (ed.) ESOP 2005. LNCS, vol.\u00a03444, pp. 326\u2013341. Springer, Heidelberg (2005)"},{"key":"20_CR20","doi-asserted-by":"publisher","first-page":"273","DOI":"10.1016\/j.tcs.2006.08.012","volume":"364","author":"F. Besson","year":"2006","unstructured":"Besson, F., Jensen, T.P., Pichardie, D.: Proof-carrying code from certified abstract interpretation and fixpoint compression. Theor. Comput. Sci.\u00a0364, 273\u2013291 (2006)","journal-title":"Theor. Comput. Sci."},{"key":"20_CR21","doi-asserted-by":"crossref","unstructured":"Necula, G.C., Rahul, S.P.: Oracle-based checking of untrusted software. In: POPL 2001, pp. 142\u2013154 (2001)","DOI":"10.1145\/373243.360216"},{"key":"20_CR22","doi-asserted-by":"crossref","unstructured":"Wu, D., Appel, A.W., Stump, A.: Foundational proof checkers with small witnesses. In: Proceedings of the 5th International ACM SIGPLAN Conference on Principles and Practice of Declarative Programming (PPDP 2003), pp. 264\u2013274. ACM (2003)","DOI":"10.1145\/888251.888276"},{"key":"20_CR23","doi-asserted-by":"crossref","unstructured":"Benton, N.: Simple relational correctness proofs for static analyses and program transformations. In: Jones, N.D., Leroy, X. (eds.) POPL 2004, pp. 14\u201325. ACM (2004)","DOI":"10.1145\/982962.964003"},{"key":"20_CR24","doi-asserted-by":"crossref","unstructured":"Beringer, L., Hofmann, M.: Secure information flow and program logics. In: CSF 2007, pp. 233\u2013248. IEEE Computer Society (2007)","DOI":"10.1109\/CSF.2007.30"},{"key":"20_CR25","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"39","DOI":"10.1007\/978-3-642-22863-6_6","volume-title":"Interactive Theorem Proving","author":"L. Beringer","year":"2011","unstructured":"Beringer, L.: Relational Decomposition. In: van Eekelen, M., Geuvers, H., Schmaltz, J., Wiedijk, F. (eds.) ITP 2011. LNCS, vol.\u00a06898, pp. 39\u201354. Springer, Heidelberg (2011)"},{"key":"20_CR26","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.\u00a03450, pp. 193\u2013209. Springer, Heidelberg (2005)"},{"key":"20_CR27","doi-asserted-by":"crossref","unstructured":"Barthe, G., D\u2019Argenio, P.R., Rezk, T.: Secure information flow by self-composition. In: 17th IEEE Computer Security Foundations Workshop (CSFW-17 2004), pp. 100\u2013114. IEEE Computer Society (2004)","DOI":"10.1109\/CSFW.2004.1310735"},{"key":"20_CR28","series-title":"LNAI","doi-asserted-by":"publisher","first-page":"116","DOI":"10.1007\/11532231_9","volume-title":"Automated Deduction \u2013 CADE-20","author":"G. Dufay","year":"2005","unstructured":"Dufay, G., Felty, A.P., Matwin, S.: Privacy-Sensitive Information Flow with JML. In: Nieuwenhuis, R. (ed.) CADE 2005. LNCS (LNAI), vol.\u00a03632, pp. 116\u2013130. Springer, Heidelberg (2005)"},{"key":"20_CR29","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"352","DOI":"10.1007\/11547662_24","volume-title":"Static Analysis","author":"T. Terauchi","year":"2005","unstructured":"Terauchi, T., Aiken, A.: Secure Information Flow as a Safety Problem. In: Hankin, C., Siveroni, I. (eds.) SAS 2005. LNCS, vol.\u00a03672, pp. 352\u2013367. Springer, Heidelberg (2005)"},{"key":"20_CR30","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/978-3-642-19718-5_1","volume-title":"Programming Languages and Systems","author":"A.W. Appel","year":"2011","unstructured":"Appel, A.W.: Verified Software Toolchain. In: Barthe, G. (ed.) ESOP 2011. LNCS, vol.\u00a06602, pp. 1\u201317. Springer, Heidelberg (2011)"},{"key":"20_CR31","doi-asserted-by":"crossref","unstructured":"Leroy, X.: Formal certification of a compiler back-end or: programming a compiler with a proof assistant. In: POPL 2006, pp. 42\u201354 (2006)","DOI":"10.1145\/1111320.1111042"}],"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-642-28641-4_20.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,3,23]],"date-time":"2025-03-23T18:58:45Z","timestamp":1742756325000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-28641-4_20"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2012]]},"ISBN":["9783642286407","9783642286414"],"references-count":31,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-28641-4_20","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2012]]}}}