{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2023,5,31]],"date-time":"2023-05-31T18:10:38Z","timestamp":1685556638233},"reference-count":37,"publisher":"Springer Science and Business Media LLC","issue":"3","license":[{"start":{"date-parts":[[2010,4,1]],"date-time":"2010-04-01T00:00:00Z","timestamp":1270080000000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Innovations Syst Softw Eng"],"published-print":{"date-parts":[[2010,9]]},"DOI":"10.1007\/s11334-010-0127-y","type":"journal-article","created":{"date-parts":[[2010,3,31]],"date-time":"2010-03-31T09:35:35Z","timestamp":1270028135000},"page":"203-218","source":"Crossref","is-referenced-by-count":0,"title":["Deductive verification of cryptographic software"],"prefix":"10.1007","volume":"6","author":[{"given":"Jos\u00e9 Bacelar","family":"Almeida","sequence":"first","affiliation":[]},{"given":"Manuel","family":"Barbosa","sequence":"additional","affiliation":[]},{"given":"Jorge Sousa","family":"Pinto","sequence":"additional","affiliation":[]},{"given":"B\u00e1rbara","family":"Vieira","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2010,4,1]]},"reference":[{"key":"127_CR1","unstructured":"Almeida JB, Barbosa M, Pinto JS, Vieira B (2009) Deductive verification of cryptographic software. Technical Report DI-CCTC-09-03, CCTC, Univ. Minho, Available from http:\/\/cctc.uminho.pt\/publications?year=2009"},{"key":"127_CR2","doi-asserted-by":"crossref","unstructured":"Ball T, Rajamani SK (2002) The SLAM project: debugging system software via static analysis. In: POPL \u201902: Proceedings of the 29th ACM SIGPLAN-SIGACT symposium on principles of programming languages. ACM, New York, pp 1\u20133","DOI":"10.1145\/503272.503274"},{"issue":"2","key":"127_CR3","doi-asserted-by":"crossref","first-page":"131","DOI":"10.1017\/S0956796804005453","volume":"15","author":"A Banerjee","year":"2005","unstructured":"Banerjee A, Naumann DA (2005) Stack-based access control and secure information flow. J Funct Program 15(2): 131\u2013177","journal-title":"J Funct Program"},{"key":"127_CR4","unstructured":"Barnett M, Rustan K, Leino M, Schulte W (2004) The Spec# programming system: an overview. In: Construction and analysis of safe, secure, and interoperable smart devices. Springer, Berlin, pp 49\u201369"},{"key":"127_CR5","doi-asserted-by":"crossref","unstructured":"Barthe G, D\u2019Argenio PR, Rezk T (2004) Secure information flow by self-composition. In: CSFW. IEEE Computer Society, USA, pp 100\u2013114","DOI":"10.1109\/CSFW.2004.1310735"},{"key":"127_CR6","unstructured":"Baudin P, Filli\u00e2tre J-C, March\u00e9 C, Monate B, Moy Y, Prevosto V (2008) ACSL: ANSI\/ISO C Specfication Language. CEA LIST and INRIA, Preliminary design (version 1.4, December 12, 2008)"},{"key":"127_CR7","doi-asserted-by":"crossref","first-page":"14","DOI":"10.1145\/964001.964003","volume-title":"POPL","author":"N Benton","year":"2004","unstructured":"Benton N (2004) Simple relational correctness proofs for static analyses and program transformations. In: Jones ND, Leroy X (eds) POPL. ACM, New York, pp 14\u201325"},{"key":"127_CR8","unstructured":"Computer Aided Cryptography Engineering. EU FP7. http:\/\/www.cace-project.eu\/"},{"key":"127_CR9","unstructured":"Chrzaszcz J (2003) Implementation of modules in the Coq system. In: Basin D, Wolff B (eds) Proceedings of the theorem proving in higher order logics 16th international conference. LNCS, vol 2758. Rome, Italy, September 2003. Springer, Berlin, pp 270\u2013286"},{"key":"127_CR10","doi-asserted-by":"crossref","unstructured":"Clarkson MR, Schneider FB (2008) Hyperproperties. In: CSF. IEEE Computer Society, USA, pp 51\u201365","DOI":"10.1109\/CSF.2008.7"},{"key":"127_CR11","unstructured":"Conchon S, Contejean E, Kanig J (2006) Ergo : a theorem prover for polymorphic first-order logic modulo theories. Available from http:\/\/alt-ergo.lri.fr\/"},{"issue":"1","key":"127_CR12","doi-asserted-by":"crossref","first-page":"70","DOI":"10.1137\/0207005","volume":"7","author":"SA Cook","year":"1978","unstructured":"Cook SA (1978) Soundness and completeness of an axiom system for program verification. SIAM J Comput 7(1): 70\u201390","journal-title":"SIAM J Comput"},{"key":"127_CR13","doi-asserted-by":"crossref","unstructured":"de Moura L, Bj\u00f8rner N (2008) Z3: an efficient SMT solver. Lecture Notes in Computer Science, vol 4963\/2008. Springer, Berlin, pp 337\u2013340","DOI":"10.1007\/978-3-540-78800-3_24"},{"issue":"7","key":"127_CR14","doi-asserted-by":"crossref","first-page":"504","DOI":"10.1145\/359636.359712","volume":"20","author":"DE Denning","year":"1977","unstructured":"Denning DE, Denning PJ (1977) Certification of programs for secure information flow. Commun ACM 20(7): 504\u2013513","journal-title":"Commun ACM"},{"issue":"3","key":"127_CR15","doi-asserted-by":"crossref","first-page":"365","DOI":"10.1145\/1066100.1066102","volume":"52","author":"D Detlefs","year":"2005","unstructured":"Detlefs D, Nelson G, Saxe JB (2005) Simplify: a theorem prover for program checking. J ACM 52(3): 365\u2013473","journal-title":"J ACM"},{"key":"127_CR16","doi-asserted-by":"crossref","unstructured":"Dufay G, Felty A, Matwin S (2005) Privacy-sensitive information flow with JML. In: Automated deduction\u2014CADE-20. Springer, Berlin, pp 116\u2013130","DOI":"10.1007\/11532231_9"},{"key":"127_CR17","doi-asserted-by":"crossref","unstructured":"Filli\u00e2tre J-C, March\u00e9 C (2007) The Why\/Krakatoa\/Caduceus platform for deductive program verification. In: Damm W, Hermanns H (eds) CAV. Lecture notes in computer science, vol 4590. Springer, Berlin, pp 173\u2013177","DOI":"10.1007\/978-3-540-73368-3_21"},{"key":"127_CR18","doi-asserted-by":"crossref","unstructured":"Henzinger TA, Jhala R, Majumdar R, Sutre G (2002) Lazy abstraction. In: POPL \u201902: Proceedings of the 29th ACM SIGPLAN-SIGACT symposium on principles of programming languages. ACM, New York, pp 58\u201370","DOI":"10.1145\/503272.503279"},{"key":"127_CR19","doi-asserted-by":"crossref","first-page":"576","DOI":"10.1145\/363235.363259","volume":"12","author":"CAR Hoare","year":"1969","unstructured":"Hoare CAR (1969) An axiomatic basis for computer programming. Commun ACM 12: 576\u2013580","journal-title":"Commun ACM"},{"key":"127_CR20","doi-asserted-by":"crossref","unstructured":"Jacobs BPF, Kiniry JR, Warnier ME, Jacobs B, Kiniry J, Warnier M (2003) Java program verification challenges. In: Proceedings of the formal methods for component objects, FMCO 2002. Lecture notes in computer science, vol 2852. Springer, Berlin, pp 202\u2013219","DOI":"10.1007\/978-3-540-39656-7_8"},{"issue":"4","key":"127_CR21","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1145\/1592434.1592438","volume":"41","author":"R Jhala","year":"2009","unstructured":"Jhala R, Majumdar R (2009) Software model checking. ACM Comput Surv 41(4): 1\u201354","journal-title":"ACM Comput Surv"},{"key":"127_CR22","doi-asserted-by":"crossref","unstructured":"Leavens GT, Ruby C, Leino KRM, Poll E, Jacobs B (2000) JML (poster session): notations and tools supporting detailed design in Java. In OOPSLA \u201900: Addendum to the 2000 proceedings of the conference on Object-oriented programming, systems, languages, and applications (Addendum). ACM, New York, pp 105\u2013106","DOI":"10.1145\/367845.367996"},{"key":"127_CR23","doi-asserted-by":"crossref","first-page":"254","DOI":"10.1007\/BFb0054294","volume":"1422","author":"KRM Leino","year":"1998","unstructured":"Leino KRM, Joshi R (1998) A semantic approach to secure information flow. Lect Notes Comput Sci 1422: 254\u2013271","journal-title":"Lect Notes Comput Sci"},{"key":"127_CR24","doi-asserted-by":"crossref","unstructured":"Leivant D (1985) Logical and mathematical reasoning about imperative programs. In: POPL, pp 132\u2013140","DOI":"10.1145\/318593.318625"},{"key":"127_CR25","doi-asserted-by":"crossref","unstructured":"Myers AC (1999) Jflow: Practical mostly-static information flow control. In: POPL, pp 228\u2013241","DOI":"10.1145\/292540.292561"},{"issue":"2","key":"127_CR26","doi-asserted-by":"crossref","first-page":"157","DOI":"10.3233\/JCS-2006-14203","volume":"14","author":"AC Myers","year":"2006","unstructured":"Myers AC, Sabelfeld A, Zdancewic S (2006) Enforcing robust declassification and qualified robustness. J Comput Secur 14(2): 157\u2013196","journal-title":"J Comput Secur"},{"key":"127_CR27","doi-asserted-by":"crossref","unstructured":"Naumann DA (2006) From coupling relations to mated invariants for checking information flow. In: Computer Security\u2014ESORICS 2006. LNCS, vol 4189, pp 279\u2013296","DOI":"10.1007\/11863908_18"},{"key":"127_CR28","unstructured":"Page D (ed) (2009) CACE Deliverable D1.1: Complete CAO and qhasm specifications. Available from http:\/\/www.cace-project.eu"},{"issue":"1","key":"127_CR29","doi-asserted-by":"crossref","first-page":"5","DOI":"10.1109\/JSAC.2002.806121","volume":"21","author":"A Sabelfeld","year":"2003","unstructured":"Sabelfeld A, Myers A (2003) Language-based information-flow security. IEEE J Selected Areas Commun 21(1): 5\u201319","journal-title":"IEEE J Selected Areas Commun"},{"key":"127_CR30","volume-title":"Applied cryptography: protocols, algorithms, and source code in C","author":"B Schneier","year":"1996","unstructured":"Schneier B (1996) Applied cryptography: protocols, algorithms, and source code in C, 2nd edn. Wiley, New York","edition":"2"},{"key":"127_CR31","doi-asserted-by":"crossref","unstructured":"Terauchi T, Aiken A (2005) Secure information flow as a safety problem. In: Hankin C, Siveroni I (eds) SAS. Lecture notes in computer science, vol 3672. Springer, Berlin, pp 352\u2013367","DOI":"10.1007\/11547662_24"},{"key":"127_CR32","unstructured":"The Coq Development Team. The Coq Proof Assistant Reference Manual\u2014Version V8.2, 2008. http:\/\/coq.inria.fr"},{"key":"127_CR33","unstructured":"The OpenSSL Project. http:\/\/www.openssl.org"},{"key":"127_CR34","doi-asserted-by":"crossref","unstructured":"Tse S, Zdancewic S (2005) A design for a security-typed language with certificate-based declassification. In: Sagiv S (ed) ESOP. Lecture notes in computer science, vol 3444. Springer, Berlin, pp 279\u2013294","DOI":"10.1007\/978-3-540-31987-0_20"},{"key":"127_CR35","doi-asserted-by":"crossref","unstructured":"Vaughan JA, Zdancewic S (2007) A cryptographic decentralized label model. In: IEEE symposium on security and privacy. IEEE Computer Society, USA, pp 192\u2013206","DOI":"10.1109\/SP.2007.5"},{"key":"127_CR36","doi-asserted-by":"crossref","unstructured":"Volpano DM, Smith G (1997) A type-based approach to program security. In: Bidoit M, Dauchet M (eds) TAPSOFT. Lecture notes in computer science, vol 1214. Springer, Berlin, pp 607\u2013621","DOI":"10.21236\/ADA486429"},{"key":"127_CR37","unstructured":"Warnier M, Oostdijk M (2005) Non-interference in JML. Technical Report ICIS-R05034, Nijmegen Institute for Computing and Information Sciences"}],"container-title":["Innovations in Systems and Software Engineering"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s11334-010-0127-y.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s11334-010-0127-y\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s11334-010-0127-y","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,5,31]],"date-time":"2023-05-31T17:38:06Z","timestamp":1685554686000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s11334-010-0127-y"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2010,4,1]]},"references-count":37,"journal-issue":{"issue":"3","published-print":{"date-parts":[[2010,9]]}},"alternative-id":["127"],"URL":"https:\/\/doi.org\/10.1007\/s11334-010-0127-y","relation":{},"ISSN":["1614-5046","1614-5054"],"issn-type":[{"value":"1614-5046","type":"print"},{"value":"1614-5054","type":"electronic"}],"subject":[],"published":{"date-parts":[[2010,4,1]]}}}