{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,11,24]],"date-time":"2025-11-24T07:08:07Z","timestamp":1763968087707},"reference-count":42,"publisher":"Cambridge University Press (CUP)","issue":"5","license":[{"start":{"date-parts":[[2013,5,17]],"date-time":"2013-05-17T00:00:00Z","timestamp":1368748800000},"content-version":"unspecified","delay-in-days":0,"URL":"https:\/\/www.cambridge.org\/core\/terms"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Math. Struct. Comp. Sci."],"published-print":{"date-parts":[[2013,10]]},"abstract":"<jats:p>Non-interference guarantees the absence of illicit information flow throughout program execution. It can be enforced by appropriate information flow type systems. Much of the previous work on type systems for non-interference has focused on calculi or high-level programming languages, and existing type systems for low-level languages typically omit objects, exceptions and method calls. We define an information flow type system for a sequential JVM-like language that includes all these programming features, and we prove, in the Coq proof assistant, that it guarantees non-interference. An additional benefit of the formalisation is that we have extracted from our proof a certified lightweight bytecode verifier for information flow. Our work provides, to the best of our knowledge, the first sound and certified information flow type system for such an expressive fragment of the JVM.<\/jats:p>","DOI":"10.1017\/s0960129512000850","type":"journal-article","created":{"date-parts":[[2013,5,17]],"date-time":"2013-05-17T11:50:01Z","timestamp":1368791401000},"page":"1032-1081","source":"Crossref","is-referenced-by-count":12,"title":["A certified lightweight non-interference Java bytecode verifier"],"prefix":"10.1017","volume":"23","author":[{"given":"GILLES","family":"BARTHE","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"DAVID","family":"PICHARDIE","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"TAMARA","family":"REZK","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"56","published-online":{"date-parts":[[2013,5,17]]},"reference":[{"key":"S0960129512000850_ref38","doi-asserted-by":"publisher","DOI":"10.1109\/CSFW.2006.29"},{"key":"S0960129512000850_ref36","unstructured":"Rezk T. (2006) Verification of confidentiality policies for mobile code, Ph.D. thesis, Universit\u00e9 de Nice Sophia-Antipolis."},{"key":"S0960129512000850_ref34","doi-asserted-by":"publisher","DOI":"10.1109\/CSFW.2006.16"},{"key":"S0960129512000850_ref29","doi-asserted-by":"publisher","DOI":"10.3233\/JCS-2003-11406"},{"key":"S0960129512000850_ref39","doi-asserted-by":"publisher","DOI":"10.1109\/JSAC.2002.806121"},{"key":"S0960129512000850_ref24","volume-title":"Principles of Program Analysis","author":"Hankin","year":"2005"},{"key":"S0960129512000850_ref23","unstructured":"Hammer C. , Krinke J. and Snelting G. (2006) Information flow control for Java based on path conditions in dependence graphs. In: IEEE International Symposium on Secure Software Engineering (ISSSE 2006) 1\u201310."},{"key":"S0960129512000850_ref19","doi-asserted-by":"crossref","unstructured":"Deng Z. and Smith G. (2004) Lenient array operations for practical secure information flow. In: Proceedings 17th IEEE Computer Security Foundations Workshop, 2004. CSFW 115\u2013124.","DOI":"10.1109\/CSFW.2004.1310736"},{"key":"S0960129512000850_ref18","doi-asserted-by":"publisher","DOI":"10.1007\/11741060_3"},{"key":"S0960129512000850_ref16","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-15640-3_17"},{"key":"S0960129512000850_ref14","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-30065-3_5"},{"key":"S0960129512000850_ref9","doi-asserted-by":"crossref","unstructured":"Barthe G. , Cavadini S. and Rezk T. (2008) Tractable enforcement of declassification policies. In: Proceedings 21st IEEE Computer Security Foundations Symposium, CSF 2008 83\u201397.","DOI":"10.1109\/CSF.2008.11"},{"key":"S0960129512000850_ref8","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-24622-0_2"},{"key":"S0960129512000850_ref5","doi-asserted-by":"publisher","DOI":"10.1007\/11555827_12"},{"key":"S0960129512000850_ref4","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2001.932501"},{"key":"S0960129512000850_ref15","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-47813-2_1"},{"key":"S0960129512000850_ref1","doi-asserted-by":"publisher","DOI":"10.1145\/292540.292555"},{"key":"S0960129512000850_ref42","doi-asserted-by":"publisher","DOI":"10.1007\/11693024_12"},{"key":"S0960129512000850_ref13","doi-asserted-by":"publisher","DOI":"10.1145\/1805974.1805977"},{"key":"S0960129512000850_ref21","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-30579-8_23"},{"key":"S0960129512000850_ref22","volume-title":"Workshop on Smart Card Technology","author":"Girard","year":"1999"},{"key":"S0960129512000850_ref40","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0030629"},{"key":"S0960129512000850_ref25","doi-asserted-by":"publisher","DOI":"10.1109\/CSFW.2006.19"},{"key":"S0960129512000850_ref26","doi-asserted-by":"crossref","unstructured":"Hunt S. and Sands D. (2006) On flow-sensitive security types. In: Proceedings POPL \u201806: Conference record of the 33rd ACM SIGPLAN-SIGACT symposium on Principles of programming languages 79\u201390","DOI":"10.1145\/1111037.1111045"},{"key":"S0960129512000850_ref17","doi-asserted-by":"publisher","DOI":"10.3233\/JCS-2002-10404"},{"key":"S0960129512000850_ref35","doi-asserted-by":"publisher","DOI":"10.1145\/596980.596983"},{"key":"S0960129512000850_ref6","doi-asserted-by":"publisher","DOI":"10.1007\/11541868_4"},{"key":"S0960129512000850_ref32","doi-asserted-by":"publisher","DOI":"10.1145\/319301.319345"},{"key":"S0960129512000850_ref12","doi-asserted-by":"publisher","DOI":"10.1145\/1040294.1040304"},{"key":"S0960129512000850_ref2","unstructured":"Agat J. (2000) Type Based Techniques for Covert Channel Elimination and Register Allocation, Ph.D. thesis, Chalmers University of Technology and Gothenburg University."},{"key":"S0960129512000850_ref31","volume-title":"Workshop on Smart Card Technology","author":"Montgomery","year":"1999"},{"key":"S0960129512000850_ref41","doi-asserted-by":"crossref","unstructured":"Volpano D. and Smith G. (1998) Probabilistic noninterference in a concurrent language. In: Procedings 11th IEEE Computer Security Foundations Workshop 34\u201343.","DOI":"10.1109\/CSFW.1998.683153"},{"key":"S0960129512000850_ref28","doi-asserted-by":"publisher","DOI":"10.1002\/spe.438"},{"key":"S0960129512000850_ref27","unstructured":"Kobayashi N. and Shirane K. (2002) Type-based information analysis for low-level languages. In: Proceedings of the Third Asian Workshop on Programming Languages and Systems, APLAS'02 302\u2013316."},{"key":"S0960129512000850_ref11","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-71316-6_10"},{"key":"S0960129512000850_ref33","doi-asserted-by":"crossref","unstructured":"Myers A. C. (1999) JFlow: Practical mostly-static information flow control. In Proceedings 26th ACM SIGPLAN-SIGACT symposium on Principles of programming languages \u2013 POPL \u201899 228\u2013241. (Ongoing development at http:\/\/www.cs.cornell.edu\/jif\/.)","DOI":"10.1145\/292540.292561"},{"key":"S0960129512000850_ref10","doi-asserted-by":"crossref","unstructured":"Barthe G. , Naumann D. and Rezk T. (2006) Deriving an information flow checker and certifying compiler for Java. In: Proceedings 2006 IEEE Symposium on Security and Privacy 230\u2013242.","DOI":"10.1109\/SP.2006.13"},{"key":"S0960129512000850_ref20","doi-asserted-by":"publisher","DOI":"10.1023\/A:1025011624925"},{"key":"S0960129512000850_ref3","doi-asserted-by":"publisher","DOI":"10.1145\/1111037.1111046"},{"key":"S0960129512000850_ref30","doi-asserted-by":"publisher","DOI":"10.1007\/11560586_29"},{"key":"S0960129512000850_ref37","doi-asserted-by":"publisher","DOI":"10.1023\/B:JARS.0000021015.15794.82"},{"key":"S0960129512000850_ref7","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796804005453"}],"container-title":["Mathematical Structures in Computer Science"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/www.cambridge.org\/core\/services\/aop-cambridge-core\/content\/view\/S0960129512000850","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,4,23]],"date-time":"2019-04-23T19:28:17Z","timestamp":1556047697000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.cambridge.org\/core\/product\/identifier\/S0960129512000850\/type\/journal_article"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2013,5,17]]},"references-count":42,"journal-issue":{"issue":"5","published-print":{"date-parts":[[2013,10]]}},"alternative-id":["S0960129512000850"],"URL":"https:\/\/doi.org\/10.1017\/s0960129512000850","relation":{},"ISSN":["0960-1295","1469-8072"],"issn-type":[{"value":"0960-1295","type":"print"},{"value":"1469-8072","type":"electronic"}],"subject":[],"published":{"date-parts":[[2013,5,17]]}}}