{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,5]],"date-time":"2024-09-05T15:12:15Z","timestamp":1725549135622},"publisher-location":"Berlin, Heidelberg","reference-count":31,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642119569"},{"type":"electronic","value":"9783642119576"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2010]]},"DOI":"10.1007\/978-3-642-11957-6_4","type":"book-chapter","created":{"date-parts":[[2010,3,8]],"date-time":"2010-03-08T00:55:38Z","timestamp":1268009738000},"page":"43-63","source":"Crossref","is-referenced-by-count":12,"title":["Precise and Automated Contract-Based Reasoning for Verification and Certification of Information Flow Properties of Programs with Arrays"],"prefix":"10.1007","author":[{"given":"Torben","family":"Amtoft","sequence":"first","affiliation":[]},{"given":"John","family":"Hatcliff","sequence":"additional","affiliation":[]},{"given":"Edwin","family":"Rodr\u00edguez","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"4_CR1","volume-title":"Proceedings of the 33rd ACM SIGPLAN-SIGACT symposium on Principles of programming languages (POPL 2006)","author":"T. Amtoft","year":"2006","unstructured":"Amtoft, T., Bandhakavi, S., Banerjee, A.: A logic for information flow in object-oriented programs. In: Proceedings of the 33rd ACM SIGPLAN-SIGACT symposium on Principles of programming languages (POPL 2006). ACM Press, New York (2006)"},{"key":"4_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","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":"4_CR3","doi-asserted-by":"publisher","first-page":"2","DOI":"10.1145\/1314436.1314438","volume-title":"5th ACM Workshop on Formal Methods in Security Engineering (FMSE 2007)","author":"T. Amtoft","year":"2007","unstructured":"Amtoft, T., Banerjee, A.: Verification condition generation for conditional information flow. In: 5th ACM Workshop on Formal Methods in Security Engineering (FMSE 2007), George Mason University, pp. 2\u201311. ACM, New York (2007); The full paper appears as Technical report 2007-2, Department of Computing and Information Sciences, Kansas State University (August 2007)"},{"key":"4_CR4","doi-asserted-by":"crossref","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. Technical report, Kansas State University (October 2009), http:\/\/www.cis.ksu.edu\/~edwin\/papers\/TR-esop10.pdf","DOI":"10.1007\/978-3-642-11957-6_4"},{"key":"4_CR5","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.: Specification and checking of software contracts for conditional information flow. In: Cuellar, J., Maibaum, T., Sere, K. (eds.) FM 2008. LNCS, vol.\u00a05014, pp. 229\u2013245. Springer, Heidelberg (2008)"},{"key":"4_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"27","DOI":"10.1007\/978-3-540-30569-9_2","volume-title":"Construction and Analysis of Safe, Secure, and Interoperable Smart Devices","author":"A. Banerjee","year":"2005","unstructured":"Banerjee, A., Naumann, D.A.: History-based access control and secure information flow. In: Barthe, G., Burdy, L., Huisman, M., Lanet, J.-L., Muntean, T. (eds.) CASSIS 2004. LNCS, vol.\u00a03362, pp. 27\u201348. Springer, Heidelberg (2005)"},{"key":"4_CR7","volume-title":"Proceedings of the IEEE International Symposium on Secure Software Engineering (ISSSE 2006)","author":"J. Barnes","year":"2006","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, Los Alamitos (2006)"},{"key":"4_CR8","doi-asserted-by":"publisher","first-page":"100","DOI":"10.1109\/CSFW.2004.1310735","volume-title":"Proceedings of the 17th IEEE Computer Security Foundations Workshop","author":"G. Barthe","year":"2004","unstructured":"Barthe, G., D\u2019Argenio, P., Rezk, T.: Secure information flow by self-composition. In: Proceedings of the 17th IEEE Computer Security Foundations Workshop, Pacific Grove, California, USA, June 28 - 30, pp. 100\u2013114. IEEE Computer Society Press, Los Alamitos (2004)"},{"issue":"1","key":"4_CR9","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(1), 37\u201361 (1985)","journal-title":"ACM Transactions on Programming Languages and Systems"},{"key":"4_CR10","volume-title":"27th IEEE\/AIAA Digital Avionics Systems Conference (DASC 2008)","author":"C. Boettcher","year":"2008","unstructured":"Boettcher, C., Delong, R., Rushby, J., Sifre, W.: The MILS component integration approach to secure information sharing. In: 27th IEEE\/AIAA Digital Avionics Systems Conference (DASC 2008). IEEE, Los Alamitos (2008)"},{"issue":"4","key":"4_CR11","doi-asserted-by":"publisher","first-page":"39","DOI":"10.1145\/1046191.1032305","volume":"XXIV","author":"R. Chapman","year":"2004","unstructured":"Chapman, R., Hilton, A.: Enforcing security and safety models with an information flow analysis tool. ACM SIGAda Ada Letters\u00a0XXIV(4), 39\u201346 (2004)","journal-title":"ACM SIGAda Ada Letters"},{"key":"4_CR12","first-page":"297","volume-title":"Foundations of Secure Computation","author":"E.S. Cohen","year":"1978","unstructured":"Cohen, E.S.: Information transmission in sequential programs. In: DeMillo, R.A., Dobkin, D.P., Jones, A.K., Lipton, R.J. (eds.) Foundations of Secure Computation, pp. 297\u2013335. Academic Press, London (1978)"},{"key":"4_CR13","doi-asserted-by":"crossref","unstructured":"Cousot, P., Cousot, R.: Abstract interpretation: A unified lattice model for static analysis of programs by construction or approximation of fixpoints. In: Conference Record of the Fourth Annual ACM Symposium on Principles of Programming Languages, pp. 238\u2013252 (1977)","DOI":"10.1145\/512950.512973"},{"key":"4_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"193","DOI":"10.1007\/978-3-540-32004-3_20","volume-title":"Security in Pervasive Computing","author":"A. Darvas","year":"2005","unstructured":"Darvas, A., 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":"4_CR15","unstructured":"Deng, Z., Smith, G.: Lenient array operations for practical secure information flow. In: 17th IEEE Computer Security Foundations Workshop, Pacific Grove, California, June 2004, pp. 115\u2013124 (2004)"},{"key":"4_CR16","doi-asserted-by":"crossref","first-page":"11","DOI":"10.1109\/SP.1982.10014","volume-title":"Proceedings of the 1982 Symposium on Security and Privacy","author":"J. Goguen","year":"1982","unstructured":"Goguen, J., Meseguer, J.: Security policies and security models. In: Proceedings of the 1982 Symposium on Security and Privacy, pp. 11\u201320. IEEE, Los Alamitos (1982)"},{"key":"4_CR17","unstructured":"Greve, D., Wilding, M., Vanfleet, W.M.: A separation kernel formal security policy. In: 4th International Workshop on the ACL2 Theorem Prover and its Applications (2003)"},{"key":"4_CR18","doi-asserted-by":"crossref","DOI":"10.1007\/978-1-4612-5983-1","volume-title":"The Science of programming","author":"D. Gries","year":"1981","unstructured":"Gries, D.: The Science of programming. Springer, New York (1981)"},{"key":"4_CR19","doi-asserted-by":"publisher","first-page":"346","DOI":"10.1145\/1180405.1180448","volume-title":"Proceedings of the 13th ACM Conference on Computer and Communications Security (CCS 2006)","author":"C.L. Heitmeyer","year":"2006","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: Proceedings of the 13th ACM Conference on Computer and Communications Security (CCS 2006), pp. 346\u2013355. ACM, New York (2006)"},{"key":"4_CR20","volume-title":"Advanced Compiler Design and Implementation","author":"S. Muchnick","year":"1997","unstructured":"Muchnick, S.: Advanced Compiler Design and Implementation. Morgan Kaufmann Publishers, San Francisco (1997)"},{"key":"4_CR21","doi-asserted-by":"publisher","first-page":"228","DOI":"10.1145\/292540.292561","volume-title":"Proceedings of the 26th ACM SIGPLAN-SIGACT symposium on Principles of programming languages (POPL 1999)","author":"A.C. Myers","year":"1999","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 (POPL 1999), pp. 228\u2013241. ACM Press, New York (1999)"},{"key":"4_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"279","DOI":"10.1007\/11863908_18","volume-title":"Computer Security \u2013 ESORICS 2006","author":"D.A. Naumann","year":"2006","unstructured":"Naumann, D.A.: From coupling relations to mated invariants for checking information flow. In: Gollmann, D., Meier, J., Sabelfeld, A. (eds.) ESORICS 2006. LNCS, vol.\u00a04189, pp. 279\u2013296. Springer, Heidelberg (2006)"},{"key":"4_CR23","unstructured":"Praxis High Integrity Systems. Rockwell Collins selects SPARK Ada for high-grade programmable cryptographic engine. Press Release (2006), http:\/\/www.praxis-his.com\/sparkada\/pdfs\/praxis_rockwell_final_pr.pdf"},{"issue":"8","key":"4_CR24","doi-asserted-by":"publisher","first-page":"102","DOI":"10.1145\/135226.135233","volume":"35","author":"W. Pugh","year":"1992","unstructured":"Pugh, W.: A practical algorithm for exact array dependence analysis. Commun. ACM\u00a035(8), 102\u2013114 (1992)","journal-title":"Commun. ACM"},{"key":"4_CR25","first-page":"7","volume-title":"Proceedings of the 2006 IEEE International Symposium on Secure Software Engineering","author":"B. Rossebo","year":"2006","unstructured":"Rossebo, B., Oman, P., Alves-Foss, J., Blue, R., Jaszkowiak, P.: Using Spark-Ada to model and verify a MILS message router. In: Proceedings of the 2006 IEEE International Symposium on Secure Software Engineering, pp. 7\u201314. IEEE, Los Alamitos (2006)"},{"key":"4_CR26","first-page":"12","volume-title":"Proceedings of the 8th ACM Symposium on Operating System Principles (SOSP 1981)","author":"J. Rushby","year":"1981","unstructured":"Rushby, J.: The design and verification of secure systems. In: Proceedings of the 8th ACM Symposium on Operating System Principles (SOSP 1981), Asilomar, CA, pp. 12\u201321. ACM Press, New York (1981); ACM Operating Systems Review 15(5)"},{"issue":"1","key":"4_CR27","doi-asserted-by":"publisher","first-page":"5","DOI":"10.1109\/JSAC.2002.806121","volume":"21","author":"A. Sabelfeld","year":"2003","unstructured":"Sabelfeld, A., Myers, A.C.: Language-based information-flow security. IEEE Journal On Selected Areas in Communications\u00a021(1), 5\u201319 (2003)","journal-title":"IEEE Journal On Selected Areas in Communications"},{"key":"4_CR28","unstructured":"Simonet, V., Rocquencourt, I.: Flow Caml in a nutshell. In: Proceedings of the first APPSEM-II workshop, pp. 152\u2013165 (2003)"},{"issue":"4","key":"4_CR29","doi-asserted-by":"publisher","first-page":"410","DOI":"10.1145\/1178625.1178628","volume":"15","author":"G. Snelting","year":"2006","unstructured":"Snelting, G., Robschink, T., Krinke, J.: Efficient path conditions in dependence graphs for software safety analysis. ACM Transactions on Software Engineering and Methodology\u00a015(4), 410\u2013457 (2006)","journal-title":"ACM Transactions on Software Engineering and Methodology"},{"key":"4_CR30","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":"4_CR31","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)"}],"container-title":["Lecture Notes in Computer Science","Programming Languages and Systems"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-11957-6_4.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,11,24]],"date-time":"2020-11-24T02:45:48Z","timestamp":1606185948000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-11957-6_4"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2010]]},"ISBN":["9783642119569","9783642119576"],"references-count":31,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-11957-6_4","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2010]]}}}