{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2023,9,13]],"date-time":"2023-09-13T18:45:05Z","timestamp":1694630705432},"reference-count":45,"publisher":"Association for Computing Machinery (ACM)","issue":"3","license":[{"start":{"date-parts":[[2008,5,1]],"date-time":"2008-05-01T00:00:00Z","timestamp":1209600000000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Form. Asp. Comput."],"published-print":{"date-parts":[[2008,5]]},"abstract":"<jats:title>Abstract<\/jats:title>\n          <jats:p>In this paper, we describe the application of the interactive theorem prover Coq to the security analysis of bytecode as used in Java. We provide a generic specification and proof of non-interference for bytecode languages using the Coq module system. We illustrate the use of this formalization by applying it to a small subset of Java bytecode. The emphasis of the paper is on modularity of a language formalization and its analysis in a machine proof.<\/jats:p>","DOI":"10.1007\/s00165-007-0055-2","type":"journal-article","created":{"date-parts":[[2007,12,3]],"date-time":"2007-12-03T13:22:51Z","timestamp":1196688171000},"page":"259-275","source":"Crossref","is-referenced-by-count":4,"title":["Formalizing non-interference for a simple bytecode language in Coq"],"prefix":"10.1145","volume":"20","author":[{"given":"Florian","family":"Kamm\u00fcller","sequence":"first","affiliation":[{"name":"Technische Universit\u00e4t Berlin, Institut f\u00fcr Softwaretechnik und Theoretische Informatik, TU Berlin, FR 5-6, Franklinstr. 28\/29, 10587, Berlin, Germany"}]}],"member":"320","reference":[{"key":"e_1_2_1_2_1_2","doi-asserted-by":"crossref","unstructured":"Andronick J Chetali B Ly O (2003) Using Coq to verify Java Card Applet Isolation Properties. Theorem proving in higher order logics TPHOLs\u201903. LNCS vol 2758. Springer Heidelberg","DOI":"10.1007\/10930755_22"},{"key":"e_1_2_1_2_2_2","unstructured":"Bicolano and MOBIUS base logic. http:\/\/mobius.inria.fr\/twiki\/bin\/view\/Bicolano 2007"},{"key":"e_1_2_1_2_3_2","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796804005453"},{"key":"e_1_2_1_2_4_2","doi-asserted-by":"crossref","unstructured":"Barthe G Basu A Rezk T (2004) Security types preserving compilation. Verification model checking and abstract interpretation VMCAI\u201904. LNCS vol 2934. Springer Heidelberg","DOI":"10.1007\/978-3-540-24622-0_2"},{"key":"e_1_2_1_2_5_2","doi-asserted-by":"crossref","unstructured":"Barthe G Dufay G (2004) A Tool-assisted framework for certified bytecode verification. Fundamental approaches to software engineering FASE 2004. LNCS vol 2984. Springer Heidelberg","DOI":"10.1007\/978-3-540-24721-0_7"},{"key":"e_1_2_1_2_6_2","unstructured":"Barthe G Kamm\u00fcller F (2005) Certified bytecode verifier for non-interference. Technical Report INRIA Sophia-Antipolis"},{"key":"#cr-split#-e_1_2_1_2_7_2.1","unstructured":"Bell DE LaPadula LJ (1996) Secure Computer systems: a mathematical model. Technical Report MTR-2547"},{"key":"#cr-split#-e_1_2_1_2_7_2.2","unstructured":"(2) MITRE Corp. Bedford 1973. Reprinted in J Comput Secur 4(2-3):239-263. IOS Press"},{"key":"e_1_2_1_2_8_2","doi-asserted-by":"crossref","DOI":"10.1007\/978-3-662-07964-5","volume-title":"Interactive theorem proving and program development\u2014Coq\u2019art: the calculus of inductive constructions","author":"Bertot Y","year":"2004"},{"key":"e_1_2_1_2_9_2","doi-asserted-by":"publisher","DOI":"10.5555\/518247"},{"key":"e_1_2_1_2_10_2","unstructured":"National Institute of Standards and Technology (2005) Common criteria for information technology security evaluation. US Department of Commerce National Bureau of Standards and Technology. http:\/\/csrc.nist.gov\/cc"},{"key":"e_1_2_1_2_11_2","doi-asserted-by":"crossref","unstructured":"Chrzaszcz J (2003) Implementing modules in the Coq system. In: Theorem proving in higher order logics TPHOLs 2003. LNCS vol 2758. Springer Heidelberg pp 270\u2013286","DOI":"10.1007\/10930755_18"},{"key":"e_1_2_1_2_12_2","doi-asserted-by":"publisher","DOI":"10.2307\/2266170"},{"key":"e_1_2_1_2_13_2","doi-asserted-by":"crossref","unstructured":"Coquand T Paulin-Mohring C (1990) Inductively defined types. In: Martin-L\u00f6f P Mints G (eds) International conference in computer logic Colog\u201988. LNCS vol 417. Springer Heidelberg","DOI":"10.1007\/3-540-52335-9_47"},{"key":"e_1_2_1_2_14_2","unstructured":"Coq Development Team (2004) The Coq proof assistant user\u2019s guide. Version 8.0"},{"key":"e_1_2_1_2_15_2","doi-asserted-by":"publisher","DOI":"10.1145\/359636.359712"},{"key":"e_1_2_1_2_16_2","unstructured":"Dufay G (2003) V\u00e9rification Formelle de la Plate-Forme Java Card. Th\u00e8se de Doctorat. Universit\u00e9 de Nice Sophia-Antipolis"},{"key":"e_1_2_1_2_17_2","unstructured":"Fenton JS (1973) Information protection systems. PhD Thesis University of Cambridge"},{"key":"e_1_2_1_2_18_2","doi-asserted-by":"crossref","unstructured":"Goguen J Meseguer J (1982) Security policies and security models. In: Proceedings of symposium on operating system principles SOSP\u201982. IEEE Computer Society Press New York pp 11\u201322","DOI":"10.1109\/SP.1982.10014"},{"key":"e_1_2_1_2_19_2","doi-asserted-by":"publisher","DOI":"10.1145\/503112.503115"},{"key":"e_1_2_1_2_20_2","unstructured":"Howard WA (1980) The formulae-as-types notion of construction. In: Seldin JP Hindley JR (eds) To H.B. Curry: Essays on combinatory logic lambda\u2013calculus and formalism. Academic NY pp 479\u2013490"},{"key":"e_1_2_1_2_21_2","doi-asserted-by":"publisher","DOI":"10.1016\/S0167-6423(99)00024-6"},{"key":"e_1_2_1_2_22_2","unstructured":"Kamm\u00fcller F (1999) Modular reasoning in isabelle. PhD thesis Computer Laboratory University of Cambridge Technical Report 470"},{"key":"e_1_2_1_2_23_2","unstructured":"Kamm\u00fcller F. http:\/\/www.swt.cs.tu-berlin.de\/~flokam\/coq\/index.html"},{"key":"e_1_2_1_2_24_2","doi-asserted-by":"publisher","DOI":"10.1023\/A:1006269330992"},{"key":"e_1_2_1_2_25_2","doi-asserted-by":"publisher","DOI":"10.1016\/S0304-3975(02)00869-1"},{"key":"e_1_2_1_2_26_2","doi-asserted-by":"publisher","DOI":"10.1023\/A:1025055424017"},{"key":"e_1_2_1_2_27_2","doi-asserted-by":"crossref","unstructured":"MacQueen DB (1986) Using dependent types to express modular structures. In: Proceedings of 13th ACM symposium on principles of programming languages POPL\u201996. Association for Computing Machinery","DOI":"10.1145\/512644.512670"},{"key":"e_1_2_1_2_28_2","unstructured":"Mobius: Mobility Ubiquity and Security (2007). http:\/\/mobius.inria.fr\/twiki\/bin\/view\/Mobius"},{"key":"e_1_2_1_2_29_2","doi-asserted-by":"crossref","unstructured":"Mosses PD (1999) Foundations of modular SOS. In: Mathematical Foundations of Computer Science MFCS\u201999. LNCS vol 1672. Springer Heidelberg","DOI":"10.1007\/3-540-48340-3_7"},{"key":"e_1_2_1_2_30_2","doi-asserted-by":"crossref","unstructured":"Naumann DA (2005) Verifying a secure information flow analyzer. Theorem proving in higher order logics TPHOLs\u201905 Oxford 2005. LNCS vol 3603. Springer Heidelberg","DOI":"10.1007\/11541868_14"},{"key":"e_1_2_1_2_31_2","doi-asserted-by":"crossref","unstructured":"Necula GC Lee P (1996) Safe Kernel extensions without run-time checking. In: Proceedings of 2nd USENIX symposium on operating systems design and implementation (OSDI). October 1996. Operating systems review Special Issue ACM 1996 and USENIX Association New York pp 229\u2013243","DOI":"10.1145\/248155.238781"},{"key":"e_1_2_1_2_32_2","doi-asserted-by":"publisher","DOI":"10.1145\/872732.806971"},{"key":"e_1_2_1_2_33_2","unstructured":"Oheimb Dv (2001) Analyzing Java in Isabelle\/HOL: formalization type safety and hoare logic. PhD Thesis Technische Universit\u00e4t M\u00fcnchen"},{"key":"e_1_2_1_2_34_2","unstructured":"Oheimb Dv (2004) Information flow control revisited: Noninfluence = Noninterference + Nonleakage. In: 9th European symposium on research in computer security ESORICS\u201904. LNCS vol 3193. Springer Heidelberg"},{"key":"e_1_2_1_2_35_2","doi-asserted-by":"crossref","unstructured":"Oheimb Dv Nipkow T (1999) Machine-checking the Java language specification: proving type-safety. In: Alves-Foss J (ed) Formal syntax and semantics of Java. LNCS vol 1523. Springer Heidelberg pp 119\u2013156","DOI":"10.1007\/3-540-48737-9_4"},{"key":"e_1_2_1_2_36_2","doi-asserted-by":"publisher","DOI":"10.5555\/509043"},{"key":"e_1_2_1_2_37_2","unstructured":"Rushby J (1992) Noninterference transitivity and channel-control security policies. Technical Report csl-92-2 SRI Palo Alto"},{"key":"e_1_2_1_2_38_2","doi-asserted-by":"publisher","DOI":"10.1109\/JSAC.2002.806121"},{"key":"e_1_2_1_2_39_2","volume-title":"To H. B. Curry: essays on combinatory logic","author":"Seldin JP","year":"1980"},{"key":"e_1_2_1_2_40_2","doi-asserted-by":"crossref","DOI":"10.1007\/978-3-642-59495-3","volume-title":"Java and the Java virtual machine: definition, verification, validation","author":"St\u00e4rk R","year":"2001"},{"key":"e_1_2_1_2_41_2","unstructured":"Strecker M (2003) Formal analysis of an information flow type system for MicroJava (extended version). Technical Report Technische Universit\u00e4t M\u00fcnchen"},{"key":"e_1_2_1_2_42_2","doi-asserted-by":"publisher","DOI":"10.5555\/130367"},{"key":"e_1_2_1_2_43_2","doi-asserted-by":"crossref","unstructured":"Tuch H Klein G Norrish M (2007) Types bytes and separation logic. In: Principles of programming languages POPL\u201907. ACM SIGPLAN 42(1) Association for Computing Machinery","DOI":"10.1145\/1190215.1190234"},{"key":"e_1_2_1_2_44_2","volume-title":"Algorithms + Datastructures = Programs","author":"Wirth N","year":"1976"}],"container-title":["Formal Aspects of Computing"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s00165-007-0055-2.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s00165-007-0055-2\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1007\/s00165-007-0055-2","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,1,6]],"date-time":"2022-01-06T15:45:15Z","timestamp":1641483915000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1007\/s00165-007-0055-2"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2008,5]]},"references-count":45,"journal-issue":{"issue":"3","published-print":{"date-parts":[[2008,5]]}},"alternative-id":["10.1007\/s00165-007-0055-2"],"URL":"https:\/\/doi.org\/10.1007\/s00165-007-0055-2","relation":{},"ISSN":["0934-5043","1433-299X"],"issn-type":[{"value":"0934-5043","type":"print"},{"value":"1433-299X","type":"electronic"}],"subject":[],"published":{"date-parts":[[2008,5]]}}}