{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,5]],"date-time":"2024-09-05T00:17:57Z","timestamp":1725495477042},"publisher-location":"Berlin, Heidelberg","reference-count":43,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540753339"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"DOI":"10.1007\/978-3-540-75336-0_2","type":"book-chapter","created":{"date-parts":[[2007,11,16]],"date-time":"2007-11-16T01:38:37Z","timestamp":1195177117000},"page":"10-29","source":"Crossref","is-referenced-by-count":11,"title":["MOBIUS: Mobility, Ubiquity, Security"],"prefix":"10.1007","author":[{"given":"Gilles","family":"Barthe","sequence":"first","affiliation":[]},{"given":"Lennart","family":"Beringer","sequence":"additional","affiliation":[]},{"given":"Pierre","family":"Cr\u00e9gut","sequence":"additional","affiliation":[]},{"given":"Benjamin","family":"Gr\u00e9goire","sequence":"additional","affiliation":[]},{"given":"Martin","family":"Hofmann","sequence":"additional","affiliation":[]},{"given":"Peter","family":"M\u00fcller","sequence":"additional","affiliation":[]},{"given":"Erik","family":"Poll","sequence":"additional","affiliation":[]},{"given":"Germ\u00e1n","family":"Puebla","sequence":"additional","affiliation":[]},{"given":"Ian","family":"Stark","sequence":"additional","affiliation":[]},{"given":"Eric","family":"V\u00e9tillard","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"2_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"380","DOI":"10.1007\/b100428","volume-title":"LPAR","author":"E. Albert","year":"2004","unstructured":"Albert, E., Puebla, G., Hermenegildo, M.V.: Abstraction-carrying code. In: Baader, F., Voronkov, A. (eds.) LPAR 2004. LNCS, vol.\u00a03452, pp. 380\u2013397. Springer, Heidelberg (2004)"},{"key":"2_CR2","doi-asserted-by":"publisher","first-page":"247","DOI":"10.1109\/LICS.2001.932501","volume-title":"Proceedings of the Sixteenth Annual IEEE Symp. on Logic in Computer Science, LICS 2001 (Invited Talk)","author":"A.W. Appel","year":"2001","unstructured":"Appel, A.W.: Foundational proof-carrying code. In: Halpern, J. (ed.) Proceedings of the Sixteenth Annual IEEE Symp. on Logic in Computer Science, LICS 2001 (Invited Talk), p. 247. IEEE Computer Society Press, Los Alamitos (2001)"},{"key":"2_CR3","series-title":"Lecture Notes in Computer Science","volume-title":"Proceedings of TPHOLs 2004","author":"D. Aspinall","year":"2004","unstructured":"Aspinall, D., Beringer, L., Hofmann, M., Loidl, H.-W., Momigliano, A.: A program logic for resource verification. In: TPHOLs 2004. LNCS, Springer, Heidelberg (2004)"},{"key":"2_CR4","series-title":"Lecture Notes in Computer Science","first-page":"1","volume-title":"Construction and Analysis of Safe, Secure, and Interoperable Smart Devices","author":"D. Aspinall","year":"2005","unstructured":"Aspinall, D., Gilmore, S., Hofmann, M., Sannella, D., Stark, I.: Mobile Resource Guarantees for Smart Devices. In: Barthe, G., Burdy, L., Huisman, M., Lanet, J.-L., Muntean, T. (eds.) CASSIS 2004. LNCS, vol.\u00a03362, pp. 1\u201327. Springer, Heidelberg (2005)"},{"key":"2_CR5","doi-asserted-by":"publisher","first-page":"131","DOI":"10.1017\/S0956796804005453","volume":"15","author":"A. Banerjee","year":"2005","unstructured":"Banerjee, A., Naumann, D.: Stack-based access control for secure information flow. Journal of Functional Programming (Special Issue on Language-Based Security)\u00a015, 131\u2013177 (2005)","journal-title":"Journal of Functional Programming"},{"key":"2_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","DOI":"10.1007\/11741060","volume-title":"SAS 2006: Proceedings of Static Analysis Symposium","author":"G. Barthe","year":"2006","unstructured":"Barthe, G., Gr\u00e9goire, B., Kunz, C., Rezk, T.: Certificate translation for optimizing compilers. In: SAS 2006: Proceedings of Static Analysis Symposium. LNCS, Springer, Heidelberg (2006)"},{"key":"2_CR7","volume-title":"Symposium on Security and Privacy, 2006","author":"G. Barthe","year":"2006","unstructured":"Barthe, G., Naumann, D., Rezk, T.: Deriving an information flow checker and certifying compiler for java. In: Symposium on Security and Privacy, 2006, IEEE Press, Orlando (2006)"},{"key":"2_CR8","series-title":"Lecture Notes in Computer Science","volume-title":"Proceedings of ESOP 2007","author":"G. Barthe","year":"2007","unstructured":"Barthe, G., Pichardie, D., Rezk, T.: A certified lightweight non-interference java bytecode verifier. In: Niccola, R.D. (ed.) Proceedings of ESOP 2007. LNCS, vol.\u00a04xxx, Springer, Heidelberg (2007)"},{"key":"2_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"389","DOI":"10.1007\/11924661_24","volume-title":"Programming Languages and Systems","author":"L. Beringer","year":"2006","unstructured":"Beringer, L., Hofmann, M.: A bytecode logic for JML and types. In: Kobayashi, N. (ed.) APLAS 2006. LNCS, vol.\u00a04279, pp. 389\u2013405. Springer, Heidelberg (2006)"},{"key":"2_CR10","series-title":"Lecture Notes in Computer Science","volume-title":"ESORICS 2006: Proceeding of 11th European Symposium On Research In Computer Security","author":"F. Besson","year":"2006","unstructured":"Besson, F., Dufay, G., Jensen, T.P.: A formal model of access control for mobile interactive devices. In: ESORICS 2006. LNCS, Springer, Heidelberg (2006)"},{"key":"2_CR11","unstructured":"Bracha, G.: Pluggable type systems. Presented at the OOPSLA 2004 Workshop on Revival of Dynamic Languages (October 2004)"},{"key":"2_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"180","DOI":"10.1007\/11693024_13","volume-title":"Programming Languages and Systems","author":"N. Broberg","year":"2006","unstructured":"Broberg, N., Sands, D.: Flow locks: Towards a core calculus for dynamic flow policies. In: Sestoft, P. (ed.) ESOP 2006 and ETAPS 2006. LNCS, vol.\u00a03924, pp. 180\u2013196. Springer, Heidelberg (2006)"},{"key":"2_CR13","unstructured":"Burdy, L., Huisman, M., Pavlova, M.: Preliminary design of BML: A behavioral interface specification language for Java bytecode. In: TSDM 2000. LNCS, Springer, Heidelberg (to appear)"},{"key":"2_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"91","DOI":"10.1007\/11526841_8","volume-title":"FM 2005: Formal Methods","author":"D. Cachera","year":"2005","unstructured":"Cachera, D., Jensen, D.P.T., Schneider, G.: Certified memory usage analysis. In: Fitzgerald, J.A., Hayes, I.J., Tarlecki, A. (eds.) FM 2005. LNCS, vol.\u00a03582, pp. 91\u2013106. Springer, Heidelberg (2005)"},{"key":"2_CR15","unstructured":"Charles, J.: Adding native specifications to JML. In: ECOOP workshop on Formal Techniques for Java-like Programs (FTfJP\u20192006) (2006)"},{"key":"2_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/3-540-44898-5_1","volume-title":"Static Analysis Available from","author":"A.S. Christensen","year":"2003","unstructured":"Christensen, A.S., M\u00f8ller, A., Schwartzbach, M.I.: Precise analysis of string expressions. In: Cousot, R. (ed.) SAS 2003. LNCS, vol.\u00a02694, pp. 1\u201318. Springer, Heidelberg (2003), Available from http:\/\/www.brics.dk\/JSA\/"},{"key":"2_CR17","doi-asserted-by":"crossref","unstructured":"Clarke, D.G., Drossopoulou, S.: Ownership, Encapsulation and the Disjointness of Type and Effect. In: OOPSLA, pp. 292\u2013310 (2002)","DOI":"10.1145\/583854.582447"},{"key":"2_CR18","doi-asserted-by":"publisher","first-page":"48","DOI":"10.1145\/286936.286947","volume-title":"Proceedings of the 13th Conference on Object-Oriented Programming, Systems, Languages, and Applications (OOPSLA-1998), ACM SIGPLAN Notices","author":"D.G. Clarke","year":"1998","unstructured":"Clarke, D.G., Potter, J.M., Noble, J.: Ownership Types for Flexible Alias Protection. In: Proceedings of the 13th Conference on Object-Oriented Programming, Systems, Languages, and Applications (OOPSLA-1998), ACM SIGPLAN Notices, vol.\u00a033(10), pp. 48\u201364. ACM Press, New York (1998)"},{"key":"2_CR19","unstructured":"Consortium, M.: Deliverable\u00a01.1: Resource and information flow security requirements (2006), Available online from http:\/\/mobius.inria.fr"},{"key":"2_CR20","unstructured":"Consortium, M.: Deliverable\u00a01.2: Framework-specific and application-specific security requirements (2006), Available online from http:\/\/mobius.inria.fr"},{"key":"2_CR21","unstructured":"Consortium, M.: Deliverable\u00a02.1: Intermediate report on type systems (2006), Available online from http:\/\/mobius.inria.fr"},{"key":"2_CR22","unstructured":"Consortium, M.: Deliverable\u00a03.1: Bytecode specification language and program logic (2006), Available online from http:\/\/mobius.inria.fr"},{"key":"2_CR23","unstructured":"Consortium, M.: Deliverable\u00a04.1: Scenarios for proof-carrying code (2006), Available online from http:\/\/mobius.inria.fr"},{"key":"2_CR24","series-title":"Electronic Notes in Theoretical Computer Science","volume-title":"Workshop on Bytecode Semantics, Verification, Analysis and Transformation (Bytecode 2005)","author":"P. Cr\u00e9gut","year":"2005","unstructured":"Cr\u00e9gut, P., Alvarado, C.: Improving the security of downloadable Java applications with static analysis. In: Workshop on Bytecode Semantics, Verification, Analysis and Transformation (Bytecode 2005). Electronic Notes in Theoretical Computer Science, vol.\u00a0141, Elsevier Science, Inc, North-Holland (2005)"},{"key":"2_CR25","unstructured":"Cunningham, D., Drossopoulou, S., Eisenbach, S., Dietl, W., M\u00fcller, P.: CUJ: Universe Types for Race Safety. Preliminary version at http:\/\/slurp.doc.ic.ac.uk\/pubs.html#cuj06"},{"issue":"8","key":"2_CR26","doi-asserted-by":"crossref","first-page":"5","DOI":"10.5381\/jot.2005.4.8.a1","volume":"4","author":"W. Dietl","year":"2005","unstructured":"Dietl, W., M\u00fcller, P.: Universes: Lightweight ownership for JML. Journal of Object Technology (JOT)\u00a04(8), 5\u201332 (2005)","journal-title":"Journal of Object Technology (JOT)"},{"key":"2_CR27","doi-asserted-by":"publisher","first-page":"235","DOI":"10.1145\/581478.581501","volume-title":"ICFP 2002: Proceedings of the International Conference on Functional Programming","author":"B. Gr\u00e9goire","year":"2002","unstructured":"Gr\u00e9goire, B., Leroy, X.: A compiled implementation of strong reduction. In: ICFP 2002: Proceedings of the International Conference on Functional Programming, pp. 235\u2013246. ACM Press, New York (2002)"},{"key":"2_CR28","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"151","DOI":"10.1007\/978-3-540-30569-9_8","volume-title":"Construction and Analysis of Safe, Secure, and Interoperable Smart Devices","author":"R. H\u00e4hnle","year":"2005","unstructured":"H\u00e4hnle, R., Mostowski, W.: Verification of safety properties in the presence of transactions. In: Barthe, G., Burdy, L., Huisman, M., Lanet, J.-L., Muntean, T. (eds.) CASSIS 2004. LNCS, vol.\u00a03362, pp. 151\u2013171. Springer, Heidelberg (2005)"},{"key":"2_CR29","volume-title":"Proceedings of the 19th IEEE Computer Security Foundations Workshop","author":"D. Hedin","year":"2006","unstructured":"Hedin, D., Sands, D.: Noninterference in the presence of non-opaque pointers. In: Proceedings of the 19th IEEE Computer Security Foundations Workshop, IEEE Computer Society Press, Los Alamitos (2006)"},{"key":"2_CR30","doi-asserted-by":"publisher","first-page":"185","DOI":"10.1145\/604131.604148","volume-title":"POPL 2003, Proceedings of the 30rd Annual. ACM SIGPLAN - SIGACT. Symposium. on Principles of Programming Languages","author":"M. Hofmann","year":"2003","unstructured":"Hofmann, M., Jost, S.: Static prediction of heap space usage for first-order functional programs. In: POPL 2003, Proceedings of the 30rd Annual. ACM SIGPLAN - SIGACT. Symposium. on Principles of Programming Languages, pp. 185\u2013197. ACM Press, New York (2003)"},{"key":"2_CR31","doi-asserted-by":"crossref","unstructured":"Hofmann, M., Jost, S.: Type-based amortised heap-space analysis. In: Proceedings of ESOP 2006, pp. 22\u201337 (2006)","DOI":"10.1007\/11693024_3"},{"key":"2_CR32","unstructured":"U.T. Initiative Unified testing criteria for Java technology-based applications for mobile devices. Technical report, Sun Microsystems, Motorola, Nokia, Siemens, Sony Ericsson, Version 2.1 (May 2006)"},{"key":"2_CR33","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","DOI":"10.1007\/11822035","volume-title":"Practical Aspects of Declarative Languages","author":"E. Mera","year":"2006","unstructured":"Mera, E., L\u00f3pez-Garc\u00eda, P., Puebla, G., Carro, M., Hermenegildo, M.: Combining Static Analysis and Profiling for Estimating Execution Times. In: Hanus, M. (ed.) PADL 2007. LNCS, vol.\u00a04354, Springer, Heidelberg (2006)"},{"key":"2_CR34","doi-asserted-by":"publisher","first-page":"228","DOI":"10.1145\/292540.292561","volume-title":"POPL 1999, Proceedings of the 26rd Annual. ACM SIGPLAN - SIGACT. Symposium. on Principles of Programming Languages","author":"A. Myers","year":"1999","unstructured":"Myers, A.: JFlow: Practical mostly-static information flow control. In: Myers, A. (ed.) POPL 1999, Proceedings of the 26rd Annual. ACM SIGPLAN - SIGACT. Symposium. on Principles of Programming Languages, pp. 228\u2013241. ACM Press, New York (1999)"},{"key":"2_CR35","doi-asserted-by":"crossref","unstructured":"M\u00fcller, P.: Modular Specification and Verification of Object-Oriented Programs. PhD thesis, FernUniversit\u00e4t Hagen (2001)","DOI":"10.1007\/3-540-45651-1"},{"key":"2_CR36","doi-asserted-by":"publisher","first-page":"106","DOI":"10.1145\/263699.263712","volume-title":"POPL 1997: Proceedings of the 24th ACM SIGPLAN-SIGACT Symposium on Principles of programming languages","author":"G.C. Necula","year":"1997","unstructured":"Necula, G.C.: Proof-carrying code. In: POPL 1997: Proceedings of the 24th ACM SIGPLAN-SIGACT Symposium on Principles of programming languages, pp. 106\u2013119. ACM Press, New York (1997)"},{"key":"2_CR37","doi-asserted-by":"crossref","unstructured":"Necula, G.C., Lee, P.: Safe kernel extensions without run-time checking. In: Proceedings of Operating Systems Design and Implementation (OSDI), Seattle, WA, USENIX Assoc, pp. 229\u2013243 (October 1996)","DOI":"10.1145\/238721.238781"},{"key":"2_CR38","first-page":"31","volume":"281","author":"E. Parliement","year":"1995","unstructured":"Parliement, E., Council, E.: Directive 95\/46\/ec of the european parliament and of the council of 24 october 1995 on the protection of individuals with regard to the processing of personal data and on the free movement of such data. Official Journal of the European Communities, number L 281, 31\u201350 (October 1995)","journal-title":"Official Journal of the European Communities, number L"},{"key":"2_CR39","volume-title":"Proceedings of CARDIS\u201904","author":"M. Pavlova","year":"2004","unstructured":"Pavlova, M., Barthe, G., Burdy, L., Huisman, M., Lanet, J.-L.: Enforcing high-level security properties for applets. In: Paradinas, P., Quisquater, J.-J. (eds.) Proceedings of CARDIS\u201904, Toulouse, France, August 2004, Kluwer Academic Publishers, Boston (2004)"},{"issue":"3-4","key":"2_CR40","doi-asserted-by":"publisher","first-page":"303","DOI":"10.1023\/B:JARS.0000021015.15794.82","volume":"31","author":"E. Rose","year":"2003","unstructured":"Rose, E.: Lightweight bytecode verification. Journal of Automated Reasoning\u00a031(3-4), 303\u2013334 (2003)","journal-title":"Journal of Automated Reasoning"},{"key":"2_CR41","doi-asserted-by":"crossref","unstructured":"Russo, A., Sabelfeld, A.: Securing interaction between threads and the scheduler. In: Proceedings of CSFW 2006 (2006)","DOI":"10.1109\/CSFW.2006.29"},{"key":"2_CR42","volume-title":"Proceedings of CSFW 2005","author":"A. Sabelfeld","year":"2005","unstructured":"Sabelfeld, A., Sands, D.: Dimensions and principles of declassification. In: Proceedings of CSFW 2005, IEEE Press, Orlando (2005)"},{"key":"2_CR43","unstructured":"The Coq development team. The coq proof assistant reference manual v8.0. Technical Report 255, INRIA, France, mars (2004), http:\/\/coq.inria.fr\/doc\/main.html"}],"container-title":["Lecture Notes in Computer Science","Trustworthy Global Computing"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-75336-0_2.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,4,27]],"date-time":"2021-04-27T10:59:26Z","timestamp":1619521166000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-75336-0_2"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[null]]},"ISBN":["9783540753339"],"references-count":43,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-75336-0_2","relation":{},"subject":[]}}