{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,19]],"date-time":"2025-06-19T04:35:06Z","timestamp":1750307706607,"version":"3.41.0"},"reference-count":40,"publisher":"Association for Computing Machinery (ACM)","issue":"1","license":[{"start":{"date-parts":[[2008,12,1]],"date-time":"2008-12-01T00:00:00Z","timestamp":1228089600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"DOI":"10.13039\/501100004965","name":"Sixth Framework Programme","doi-asserted-by":"publisher","award":["IST-026764"],"award-info":[{"award-number":["IST-026764"]}],"id":[{"id":"10.13039\/501100004965","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["ACM Trans. Program. Lang. Syst."],"published-print":{"date-parts":[[2008,12]]},"abstract":"<jats:p>Bytecode verification is a key point in the security chain of the Java platform. This feature is only optional in many embedded devices since the memory requirements of the verification process are too high. In this article we propose an approach that significantly reduces the use of memory by a serial\/parallel decomposition of the verification into multiple specialized passes. The algorithm reduces the type encoding space by operating on different abstractions of the domain of types. The results of our evaluation show that this bytecode verification can be performed directly on small memory systems. The method is formalized in the framework of abstract interpretation.<\/jats:p>","DOI":"10.1145\/1452044.1452047","type":"journal-article","created":{"date-parts":[[2008,12,10]],"date-time":"2008-12-10T15:32:31Z","timestamp":1228923151000},"page":"1-63","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":3,"title":["Decomposing bytecode verification by abstract interpretation"],"prefix":"10.1145","volume":"31","author":[{"given":"C.","family":"Bernardeschi","sequence":"first","affiliation":[{"name":"Universit\u00e0 di Pisa, Pisa, Italy"}]},{"given":"N. De","family":"Francesco","sequence":"additional","affiliation":[{"name":"Universit\u00e0 di Pisa, Pisa, Italy"}]},{"given":"G.","family":"Lettieri","sequence":"additional","affiliation":[{"name":"Universit\u00e0 di Pisa, Pisa, Italy"}]},{"given":"L.","family":"Martini","sequence":"additional","affiliation":[{"name":"Universit\u00e0 di Pisa, Pisa, Italy"}]},{"given":"P.","family":"Masci","sequence":"additional","affiliation":[{"name":"Universit\u00e0 di Pisa, Pisa, Italy"}]}],"member":"320","published-online":{"date-parts":[[2008,12,12]]},"reference":[{"key":"e_1_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-005-0084-6"},{"key":"e_1_2_1_2_1","volume-title":"Proceedings of the OTM Workshops. Lecture Notes in Computer Science","volume":"2889","author":"Bernardeschi C.","unstructured":"Bernardeschi , C. , De Francesco , N. , and Martini , L . 2003. Efficient bytecode verification using immediate postdominators in control flow graphs . In Proceedings of the OTM Workshops. Lecture Notes in Computer Science , vol. 2889 . Springer, 425--436. Bernardeschi, C., De Francesco, N., and Martini, L. 2003. Efficient bytecode verification using immediate postdominators in control flow graphs. In Proceedings of the OTM Workshops. Lecture Notes in Computer Science, vol. 2889. Springer, 425--436."},{"key":"e_1_2_1_3_1","unstructured":"Bernardeschi C. Francesco N. D. Lettieri G. Martini L. and Masci P. 2007. Decomposing bytecode verification by abstract interpretation for space awareness in embedded systems. Tech. rep. IET-07-01 Dipartimento di Ingegneria dell'Informazione Universit\u00e0 di Pisa http:\/\/www.ing.unipi.it\/~o1103499\/papers\/IET-07-01.pdf.  Bernardeschi C. Francesco N. D. Lettieri G. Martini L. and Masci P. 2007. Decomposing bytecode verification by abstract interpretation for space awareness in embedded systems. Tech. rep. IET-07-01 Dipartimento di Ingegneria dell'Informazione Universit\u00e0 di Pisa http:\/\/www.ing.unipi.it\/~o1103499\/papers\/IET-07-01.pdf."},{"key":"e_1_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1093\/comjnl\/bxh161"},{"key":"e_1_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.ipl.2005.11.017"},{"key":"e_1_2_1_6_1","doi-asserted-by":"crossref","unstructured":"Bieber P. Cazin J. Marouani A. E. Girard P. Lanet J.-L. Wiels V. and Zanon G. 2001. The PACAP prototype: A tool for detecting Java card illegal flow. Lecture Notes in Computer Science vol. 2041.   Bieber P. Cazin J. Marouani A. E. Girard P. Lanet J.-L. Wiels V. and Zanon G. 2001. The PACAP prototype: A tool for detecting Java card illegal flow. Lecture Notes in Computer Science vol. 2041.","DOI":"10.1007\/3-540-45165-X_3"},{"volume-title":"Proceedings of the International Conference on Dependable Systems and Networks (DSN'02)","author":"Casset L.","key":"e_1_2_1_7_1","unstructured":"Casset , L. , Burdy , L. , and Requet , A . 2002. Formal development of an embedded verifier for Java Card byte code . In Proceedings of the International Conference on Dependable Systems and Networks (DSN'02) . IEEE Computer Society, 51--58. Casset, L., Burdy, L., and Requet, A. 2002. Formal development of an embedded verifier for Java Card byte code. In Proceedings of the International Conference on Dependable Systems and Networks (DSN'02). IEEE Computer Society, 51--58."},{"key":"e_1_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1145\/583810.583821"},{"key":"e_1_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1002\/cpe.714"},{"key":"e_1_2_1_10_1","doi-asserted-by":"crossref","unstructured":"Coglio A. 2004. Simple verification technique for complex Java bytecode subroutines. Concur.\u2014Pract. Exper. 16 7 647--670.   Coglio A. 2004. Simple verification technique for complex Java bytecode subroutines. Concur.\u2014Pract. Exper. 16 7 647--670.","DOI":"10.1002\/cpe.798"},{"key":"e_1_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1145\/115372.115297"},{"key":"e_1_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1145\/239912.239914"},{"key":"e_1_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1145\/512950.512973"},{"key":"e_1_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1145\/567752.567778"},{"key":"e_1_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1093\/logcom\/2.4.511"},{"key":"e_1_2_1_16_1","doi-asserted-by":"crossref","unstructured":"Davey B. A. and Priestley H. A. 2002. Introduction to Lattices and Order. Cambridge University Press.  Davey B. A. and Priestley H. A. 2002. Introduction to Lattices and Order. Cambridge University Press.","DOI":"10.1017\/CBO9780511809088"},{"volume-title":"Java Card. In Proceedings of the 2nd USENIX Workshop on Industrial Experiences with Systems Software. USENIX, 15--24","author":"Deville D.","key":"e_1_2_1_17_1","unstructured":"Deville , D. and Grimaud , G. 2002. Building an \u201cimpossible\u201d verifier on a Java Card. In Proceedings of the 2nd USENIX Workshop on Industrial Experiences with Systems Software. USENIX, 15--24 . Deville, D. and Grimaud, G. 2002. Building an \u201cimpossible\u201d verifier on a Java Card. In Proceedings of the 2nd USENIX Workshop on Industrial Experiences with Systems Software. USENIX, 15--24."},{"key":"e_1_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1145\/330643.330646"},{"key":"e_1_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0167-6423(97)00034-8"},{"key":"e_1_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1145\/333979.333989"},{"key":"e_1_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1145\/293677.293680"},{"key":"e_1_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1145\/288090.288104"},{"key":"e_1_2_1_23_1","unstructured":"Gosling J. Joy B. Steele G. and Bracha G. 2000. Java Language Specification 2nd Ed.: The Java Series. Addison-Wesley Longman Publishing Co. Inc. Boston MA.   Gosling J. Joy B. Steele G. and Bracha G. 2000. Java Language Specification 2nd Ed.: The Java Series. Addison-Wesley Longman Publishing Co. Inc. Boston MA."},{"volume-title":"Proceedings of the 5th International Conference Information and Communications Security (ICICS'03)","author":"Hypp\u00f6nen K.","key":"e_1_2_1_24_1","unstructured":"Hypp\u00f6nen , K. , Naccache , D. , Trichina , E. , and Tchoulkine , A . 2003. Trading-off type-inference memory complexity against communication . In Proceedings of the 5th International Conference Information and Communications Security (ICICS'03) , S. Qing, D. Gollmann, and J. Zhou, Eds. Lecture Notes in Computer Science. Springer, 60--71. Hypp\u00f6nen, K., Naccache, D., Trichina, E., and Tchoulkine, A. 2003. Trading-off type-inference memory complexity against communication. In Proceedings of the 5th International Conference Information and Communications Security (ICICS'03), S. Qing, D. Gollmann, and J. Zhou, Eds. Lecture Notes in Computer Science. Springer, 60--71."},{"key":"e_1_2_1_25_1","unstructured":"JSR 2006. Jsr-000202 Java class file specification update. Tech. rep. JSR202 Java Community Process http:\/\/jcp.org\/en\/jsr\/detail?id=202.  JSR 2006. Jsr-000202 Java class file specification update. Tech. rep. JSR202 Java Community Process http:\/\/jcp.org\/en\/jsr\/detail?id=202."},{"key":"e_1_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.1145\/1146809.1146811"},{"key":"e_1_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.1145\/383043.383045"},{"key":"e_1_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.5555\/646692.703437"},{"key":"e_1_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.5555\/647770.734254"},{"key":"e_1_2_1_30_1","doi-asserted-by":"publisher","DOI":"10.1002\/spe.438"},{"key":"e_1_2_1_31_1","doi-asserted-by":"publisher","DOI":"10.1023\/A:1025055424017"},{"key":"e_1_2_1_32_1","unstructured":"Lindholm T. and Yellin F. 1999. Java Virtual Machine Specification 2nd Ed. Addison-Wesley Longman Publishing Co. Inc. Reading MA.   Lindholm T. and Yellin F. 1999. Java Virtual Machine Specification 2nd Ed. Addison-Wesley Longman Publishing Co. Inc. Reading MA."},{"key":"e_1_2_1_33_1","doi-asserted-by":"publisher","DOI":"10.1145\/154630.154648"},{"key":"e_1_2_1_34_1","volume-title":"Eds. Lecture Notes in Computer Science","volume":"2513","author":"Naccache D.","unstructured":"Naccache , D. , Tchoulkine , A. , Tymen , C. , and Trichina , E . 2003. Reducing the memory complexity of type-inference algorithms. In Information and Communications Security, R. Deng, S.Quing, F.Bao, and J. Zhou , Eds. Lecture Notes in Computer Science , vol. 2513 , Springer-Verlag, 109--121. Naccache, D., Tchoulkine, A., Tymen, C., and Trichina, E. 2003. Reducing the memory complexity of type-inference algorithms. In Information and Communications Security, R. Deng, S.Quing, F.Bao, and J. Zhou, Eds. Lecture Notes in Computer Science, vol. 2513, Springer-Verlag, 109--121."},{"key":"e_1_2_1_35_1","doi-asserted-by":"publisher","DOI":"10.1145\/263699.263712"},{"key":"e_1_2_1_36_1","doi-asserted-by":"publisher","DOI":"10.1145\/363911.363915"},{"key":"e_1_2_1_37_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0167-6423(02)00095-3"},{"key":"e_1_2_1_38_1","doi-asserted-by":"publisher","DOI":"10.1023\/B:JARS.0000021015.15794.82"},{"volume-title":"Proceeding of the Workshop on the Formal Underpinning of Java.","author":"Rose E.","key":"e_1_2_1_39_1","unstructured":"Rose , E. and Rose , K . 1998. Lightweight bytecode verification . In Proceeding of the Workshop on the Formal Underpinning of Java. Rose, E. and Rose, K. 1998. Lightweight bytecode verification. In Proceeding of the Workshop on the Formal Underpinning of Java."},{"key":"e_1_2_1_40_1","doi-asserted-by":"publisher","DOI":"10.2307\/1968865"}],"container-title":["ACM Transactions on Programming Languages and Systems"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/1452044.1452047","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/1452044.1452047","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T13:30:06Z","timestamp":1750253406000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/1452044.1452047"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2008,12]]},"references-count":40,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2008,12]]}},"alternative-id":["10.1145\/1452044.1452047"],"URL":"https:\/\/doi.org\/10.1145\/1452044.1452047","relation":{},"ISSN":["0164-0925","1558-4593"],"issn-type":[{"type":"print","value":"0164-0925"},{"type":"electronic","value":"1558-4593"}],"subject":[],"published":{"date-parts":[[2008,12]]},"assertion":[{"value":"2007-01-01","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2008-03-01","order":1,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2008-12-12","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}