{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,25]],"date-time":"2025-03-25T18:22:41Z","timestamp":1742926961947,"version":"3.40.3"},"publisher-location":"Boston, MA","reference-count":33,"publisher":"Springer US","isbn-type":[{"type":"print","value":"9781441915382"},{"type":"electronic","value":"9781441915399"}],"license":[{"start":{"date-parts":[[2010,1,1]],"date-time":"2010-01-01T00:00:00Z","timestamp":1262304000000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2010,1,1]],"date-time":"2010-01-01T00:00:00Z","timestamp":1262304000000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2010]]},"DOI":"10.1007\/978-1-4419-1539-9_12","type":"book-chapter","created":{"date-parts":[[2010,3,2]],"date-time":"2010-03-02T00:26:11Z","timestamp":1267489571000},"page":"341-379","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":3,"title":["Specification and Checking of Software Contracts for Conditional Information Flow"],"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":[]},{"family":"Robby","sequence":"additional","affiliation":[]},{"given":"Jonathan","family":"Hoag","sequence":"additional","affiliation":[]},{"given":"David","family":"Greve","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2010,1,23]]},"reference":[{"key":"12_CR1_12","series-title":"LNCS","doi-asserted-by":"crossref","first-page":"100","DOI":"10.1007\/978-3-540-27864-1_10","volume-title":"11th static analysis symposium (SAS)","author":"T Amtoft","year":"2004","unstructured":"Amtoft T, Banerjee A (2004) Information flow analysis in logical form. In: 11th static analysis symposium (SAS), LNCS, vol 3148. Springer, Berlin, pp 100\u2013115"},{"issue":"1","key":"12_CR2_12","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1016\/j.scico.2006.03.002","volume":"64","author":"T Amtoft","year":"2007","unstructured":"Amtoft T, Banerjee A (2007a) A logic for information flow analysis with an application to forward slicing of simple imperative programs. Sci Comp Prog 64(1):3\u201328","journal-title":"Sci Comp Prog"},{"key":"12_CR3_12","first-page":"2","volume-title":"5th ACM workshop on formal methods in security engineering (FMSE), a long version, with proofs, appears as technical report CIS TR 2007-2","author":"T Amtoft","year":"2007","unstructured":"Amtoft T, Banerjee A (2007b) Verification condition generation for conditional information flow. In: 5th ACM workshop on formal methods in security engineering (FMSE), a long version, with proofs, appears as technical report CIS TR 2007-2, Kansas State University, Manhattan, KS, pp 2\u201311"},{"key":"12_CR4_12","doi-asserted-by":"crossref","unstructured":"Amtoft T, Bandhakavi S, Banerjee A (2006) A logic for information flow in object-oriented programs. In: 33rd Principles of programming languages (POPL), pp 91\u2013102","DOI":"10.1145\/1111037.1111046"},{"key":"12_CR5_12","unstructured":"Amtoft T, Hatcliff J, Rodriguez E, Robby, Hoag J, Greve D (2007) Specification and checking of software contracts for conditional information flow (extended version). Technical report SAnToS-TR2007-5, CIS Department, Kansas State University. Available at http:\/\/www.sireum.org"},{"key":"12_CR6_12","doi-asserted-by":"crossref","unstructured":"Amtoft T, Hatcliff J, Rodr\u00edguez E (2009) Precise and automated contract-based reasoning for verification and certification of information flow properties of programs with arrays. Technical report, Kansas State University. URL http:\/\/www.cis.ksu.edu\/~edwin\/papers\/TR-esop10.pdf, available from http:\/\/www.cis.ksu.edu\/ edwin\/papers\/TR-esop10.pdf","DOI":"10.1007\/978-3-642-11957-6_4"},{"issue":"15","key":"12_CR7_12","doi-asserted-by":"publisher","first-page":"131","DOI":"10.1017\/S0956796804005453","volume":"2","author":"A Banerjee","year":"2005","unstructured":"Banerjee A, Naumann DA (2005) Stack-based access control and secure information flow. J Funct Program 2(15):131\u2013177","journal-title":"J Funct Program"},{"key":"12_CR8_12","volume-title":"High integrity software \u2013 the SPARK approach to safety and security","author":"J Barnes","year":"2003","unstructured":"Barnes J (2003) High integrity software \u2013 the SPARK approach to safety and security. Addison-Wesley, Reading, MA"},{"key":"12_CR9_12","doi-asserted-by":"crossref","unstructured":"Barnett M, Leino KRM, Schulte W (2004) The Spec# programming system: an overview. In: Construction and analysis of safe, secure, and interoperable smart devices (CASSIS), pp 49\u201369","DOI":"10.1007\/978-3-540-30569-9_3"},{"key":"12_CR10_12","first-page":"100","volume-title":"CSFW\u201904","author":"G Barthe","year":"2004","unstructured":"Barthe G, D\u2019Argenio P, Rezk T (2004) Secure information flow by self-composition. In: Foccardi R (ed) CSFW\u201904. IEEE, New York, NY, pp 100\u2013114"},{"key":"12_CR11_12","unstructured":"Bell D, LaPadula L (1973) Secure computer systems: mathematical foundations. Technical report, MTR-2547, MITRE Corp"},{"issue":"1","key":"12_CR12_12","doi-asserted-by":"publisher","first-page":"37","DOI":"10.1145\/2363.2366","volume":"7","author":"JF Bergeretti","year":"1985","unstructured":"Bergeretti JF, Carr\u00e9 BA (1985) Information-flow and data-flow analysis of while-programs. ACM TOPLAS 7(1):37\u201361","journal-title":"ACM TOPLAS"},{"key":"12_CR13_12","first-page":"39","volume-title":"SIGAda\u201904, Atlanta, Georgia","author":"R Chapman","year":"2004","unstructured":"Chapman R, Hilton A (2004) Enforcing security and safety models with an information flow analysis tool. In: SIGAda\u201904, Atlanta, Georgia. ACM, New York, NY, pp 39\u201346"},{"key":"12_CR14_12","first-page":"297","volume-title":"Foundations of secure computation","author":"ES Cohen","year":"1978","unstructured":"Cohen ES (1978) Information transmission in sequential programs. In: Foundations of secure computation. Academic, New York, NY, pp 297\u2013335"},{"key":"12_CR15_12","doi-asserted-by":"crossref","unstructured":"Cok DR, Kiniry J (2004) ESC\/Java2: uniting ESC\/Java and JML. In: Construction and analysis of safe, secure, and interoperable smart devices (CASSIS), pp 108\u2013128","DOI":"10.1007\/978-3-540-30569-9_6"},{"key":"12_CR16_12","first-page":"193","volume-title":"LNCS, vol 3450","author":"Darvas A, H\u00e4hnle R, Sands D (2005) A theorem proving approach to analysis of secure information flow. In: 2nd International conference on security in pervasive computing (SPC","year":"2005","unstructured":"Darvas A, H\u00e4hnle R, Sands D (2005) A theorem proving approach to analysis of secure information flow. In: 2nd International conference on security in pervasive computing (SPC 2005), LNCS, vol 3450. Springer, Berlin, pp 193\u2013209"},{"key":"12_CR17_12","doi-asserted-by":"crossref","unstructured":"Goguen JA, Meseguer J (1982) Security policies and security models. In: IEEE symposium on security and privacy, pp 11\u201320","DOI":"10.1109\/SP.1982.10014"},{"key":"12_CR18_12","unstructured":"Greve D, Wilding M, Vanfleet WM (2003) A separation kernel formal security policy. In: 4th International workshop on the ACL2 prover and its applications (ACL2-2003)"},{"key":"12_CR19_12","doi-asserted-by":"crossref","unstructured":"Heitmeyer CL, Archer M, Leonard EI, McLean J (2006) 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\u201906), pp 346\u2013355","DOI":"10.1145\/1180405.1180448"},{"key":"12_CR20_12","series-title":"LNCS","first-page":"235","volume-title":"10th SPIN workshop","author":"TA Henzinger","year":"2003","unstructured":"Henzinger TA, Jhala R, Majumdar R, Sutre G (2003) Software verification with blast. In: 10th SPIN workshop, LNCS, vol 2648. Springer, Berlin, pp 235\u2013239"},{"volume-title":"Software for dependable systems: sufficient evidence? National Academies Press","year":"2007","key":"12_CR21_12","unstructured":"Jackson D, Thomas M, Millett LI (eds) (2007) Software for dependable systems: sufficient evidence? National Academies Press, Committee on certifiably dependable software systems, National Research Council"},{"key":"12_CR22_12","volume-title":"Computer-aided reasoning: an approach","author":"M Kaufmann","year":"2000","unstructured":"Kaufmann M, Manolios P, Moore JS (2000) Computer-aided reasoning: an approach. Kluwer, Dordrecht"},{"key":"12_CR23_12","first-page":"228","volume-title":"POPL\u201999, San Antonio, Texas","author":"AC Myers","year":"1999","unstructured":"Myers AC (1999) JFlow: practical mostly-static information flow control. In: POPL\u201999, San Antonio, Texas. ACM, New York, NY, pp 228\u2013241"},{"key":"12_CR24_12","first-page":"279","volume-title":"11th European symposium on research in computer security (ESORICS\u201906), LNCS","author":"DA Naumann","year":"2006","unstructured":"Naumann DA (2006) From coupling relations to mated invariants for checking information flow. In: Gollmann D, Meier J, Sabelfeld A (eds) 11th European symposium on research in computer security (ESORICS\u201906), LNCS, vol 4189. Springer, Berlin, pp 279\u2013296"},{"key":"12_CR25_12","doi-asserted-by":"crossref","unstructured":"Owre S, Rushby JM, Shankar N (1992) PVS: a prototype verification system. In: Proceedings of the 11th international conference on automated deduction (Lecture notes in computer science 607)","DOI":"10.1007\/3-540-55602-8_217"},{"key":"12_CR26_12","volume-title":"Using SPARK-Ada to model and verify a MILS message router","author":"B Rossebo","year":"2006","unstructured":"Rossebo B, Oman P, Alves-Foss J, Blue R, Jaszkowiak P (2006) Using SPARK-Ada to model and verify a MILS message router. In: Proceedings of the international symposium on secure software engineering"},{"issue":"5","key":"12_CR27_12","doi-asserted-by":"crossref","first-page":"12","DOI":"10.1145\/1067627.806586","volume":"15","author":"J Rushby","year":"1981","unstructured":"Rushby J (1981) The design and verification of secure systems. In: 8th ACM symposium on operating systems principles, vol 15, Issue 5, pp 12\u201321","journal-title":"8th ACM symposium on operating systems principles"},{"key":"12_CR28_12","unstructured":"Simonet V (2003) Flow Caml in a nutshell. In: Hutton G (ed) First APPSEM-II workshop, pp 152\u2013165"},{"key":"12_CR29_12","unstructured":"Sireum website. http:\/\/www.sireum.org"},{"issue":"4","key":"12_CR30_12","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 (2006) Efficient path conditions in dependence graphs for software safety analysis. ACM Trans Softw Eng Method 15(4):410\u2013457","journal-title":"ACM Trans Softw Eng Method"},{"key":"12_CR31_12","series-title":"LNCS","doi-asserted-by":"crossref","first-page":"352","DOI":"10.1007\/11547662_24","volume-title":"12th Static analysis symposium","author":"T Terauchi","year":"2005","unstructured":"Terauchi T, Aiken A (2005) Secure information flow as a safety problem. In: 12th Static analysis symposium, LNCS, vol 3672. Springer, Berlin, pp 352\u2013367"},{"key":"12_CR32_12","first-page":"12","volume":"18","author":"M Vanfleet","year":"2005","unstructured":"Vanfleet M, Luke J, Beckwith RW, Taylor C, Calloni B, Uchenick G (2005) MILS: architecture for high-assurance embedded computing. CrossTalk: J Defense Softw Eng 18:12\u201316","journal-title":"CrossTalk: J Defense Softw Eng"},{"issue":"3","key":"12_CR33_12","doi-asserted-by":"crossref","first-page":"167","DOI":"10.3233\/JCS-1996-42-304","volume":"4","author":"D Volpano","year":"1996","unstructured":"Volpano D, Smith G, Irvine C (1996) A sound type system for secure flow analysis. J Comput Security 4(3):167\u2013188","journal-title":"J Comput Security"}],"container-title":["Design and Verification of Microprocessor Systems for High-Assurance Applications"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-1-4419-1539-9_12","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,2,18]],"date-time":"2023-02-18T03:22:24Z","timestamp":1676690544000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-1-4419-1539-9_12"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2010]]},"ISBN":["9781441915382","9781441915399"],"references-count":33,"URL":"https:\/\/doi.org\/10.1007\/978-1-4419-1539-9_12","relation":{},"subject":[],"published":{"date-parts":[[2010]]},"assertion":[{"value":"23 January 2010","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}