Decomposing bytecode verification by abstract interpretation

ABSTRACT

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.

REFERENCES

• 1: Gilles Barthe , Pierre Courtieu , Guillaume Dufay , Simão Melo De Sousa, Tool-Assisted Specification and Verification of Typed Low-Level Languages, Journal of Automated Reasoning, v.35 n.4, p.295-354, November 2005 [doi>10.1007/s10817-005-0084-6]
• 2: 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.
• 3: 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à di Pisa, http://www.ing.unipi.it/~o1103499/papers/IET-07-01.pdf.
• 4: C. Bernardeschi , G. Lettieri , L. Martini , P. Masci, Using Control Dependencies for Space-Aware Bytecode Verification, The Computer Journal, v.49 n.2, p.234-248, March 2006 [doi>10.1093/comjnl/bxh161]
• 5: C. Bernardeschi , G. Lettieri , L. Martini , P. Masci, Using postdomination to reduce space requirements of data flow analysis, Information Processing Letters, v.98 n.1, p.11-18, 15 April 2006 [doi>10.1016/j.ipl.2005.11.017]
• 6: Pierre Bieber , Jacques Cazin , A. El Marouani , Pierre Girard , Jean Louis Lanet , Virginie Wiels , Guy Zanon, The PACAP Prototype: A Tool for Detecting Java Card Illegal Flow, Revised Papers from the First International Workshop on Java on Smart Cards: Programming and Security, p.25-37, September 14, 2000
• 7: Ludovic Casset , Lilian Burdy , Antoine Requet, Formal Development of an Embedded Verifier for Java Card Byte Code, Proceedings of the 2002 International Conference on Dependable Systems and Networks, p.51-58, June 23-26, 2002
• 8: Cliff Click , John Rose, Fast subtype checking in the HotSpot JVM, Proceedings of the 2002 joint ACM-ISCOPE conference on Java Grande, p.96-107, November 03-05, 2002, Seattle, Washington, USA [doi>10.1145/583810.583821]
• 9: Coglio, A. 2003. Improving the official specification of Java bytecode verification. Concur. Computat. Pract. Exper. 15, 2, 155--179.
• 10: Alessandro Coglio, Simple verification technique for complex Java bytecode subroutines: Research Articles, Concurrency and Computation: Practice & Experience, v.16 n.7, p.647-670, June 2004 [doi>10.1002/cpe.v16:7]
• 11: Norman H. Cohen, Type-extension type test can be performed in constant time, ACM Transactions on Programming Languages and Systems (TOPLAS), v.13 n.4, p.626-629, Oct. 1991 [doi>10.1145/115372.115297]
• 12: Agostino Cortesi , Gilberto Filé , Francesco Ranzato , Roberto Giacobazzi , Catuscia Palamidessi, Complementation in abstract interpretation, ACM Transactions on Programming Languages and Systems (TOPLAS), v.19 n.1, p.7-47, Jan. 1997 [doi>10.1145/239912.239914]
• 13: Patrick Cousot , Radhia Cousot, Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints, Proceedings of the 4th ACM SIGACT-SIGPLAN symposium on Principles of programming languages, p.238-252, January 17-19, 1977, Los Angeles, California [doi>10.1145/512950.512973]
• 14: Patrick Cousot , Radhia Cousot, Systematic design of program analysis frameworks, Proceedings of the 6th ACM SIGACT-SIGPLAN symposium on Principles of programming languages, p.269-282, January 29-31, 1979, San Antonio, Texas [doi>10.1145/567752.567778]
• 15: Cousot, P. and Cousot, R. 1992. Abstract interpretation frameworks. J. Logic Comput. 2, 511--547.
• 16: Davey, B. A. and Priestley, H. A. 2002. Introduction to Lattices and Order. Cambridge University Press.
• 17: Damien Deville , Gilles Grimaud, Building an "impossible" verifier on a java card, Proceedings of the 2nd conference on Industrial Experiences with Systems Software, p.2-2, December 08, 2002, Boston, MA
• 18: Stephen N. Freund , John C. Mitchell, A type system for object initialization in the Java bytecode language, ACM Transactions on Programming Languages and Systems (TOPLAS), v.21 n.6, p.1196-1250, Nov. 1999 [doi>10.1145/330643.330646]
• 19: Roberto Giacobazzi , Francesco Ranzato, Optimal domains for disjunctive abstract interpretation, Science of Computer Programming, v.32 n.1-3, p.177-210, Sept. 1998 [doi>10.1016/S0167-6423(97)00034-8]
• 20: Roberto Giacobazzi , Francesco Ranzato , Francesca Scozzari, Making abstract interpretations complete, Journal of the ACM (JACM), v.47 n.2, p.361-416, March 2000 [doi>10.1145/333979.333989]
• 21: Roberto Giacobazzi , Francesca Scozzari, A logical model for relational abstract domains, ACM Transactions on Programming Languages and Systems (TOPLAS), v.20 n.5, p.1067-1109, Sept. 1998 [doi>10.1145/293677.293680]
• 22: Allen Goldberg, A specification of Java loading and bytecode verification, Proceedings of the 5th ACM conference on Computer and communications security, p.49-58, November 02-05, 1998, San Francisco, California, United States [doi>10.1145/288090.288104]
• 23: James Gosling , Bill Joy , Guy Steele , Gilad Bracha, Java Language Specification, Second Edition: The Java Series, Addison-Wesley Longman Publishing Co., Inc., Boston, MA, 2000
• 24: Hyppönen, 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.
• 25: JSR 2006. Jsr-000202 Java class file specification update. Tech. rep. JSR202, Java Community Process, http://jcp.org/en/jsr/detail?id=202.
• 26: Gerwin Klein , Tobias Nipkow, A machine-checked model for a Java-like language, virtual machine, and compiler, ACM Transactions on Programming Languages and Systems (TOPLAS), v.28 n.4, p.619-695, July 2006 [doi>10.1145/1146809.1146811]
• 27: Todd B. Knoblock , Jakob Rehof, Type elaboration and subtype completion for Java bytecode, ACM Transactions on Programming Languages and Systems (TOPLAS), v.23 n.2, p.243-272, March 2001 [doi>10.1145/383043.383045]
• 28: Jean Louis Lanet , Antoine Requet, Formal Proof of Smart Card Applets Correctness, Proceedings of the The International Conference on Smart Card Research and Applications, p.85-97, September 14-16, 1998
• 29: Xavier Leroy, Java Bytecode Verification: An Overview, Proceedings of the 13th International Conference on Computer Aided Verification, p.265-285, July 18-22, 2001
• 30: Xavier Leroy, Bytecode verification on Java smart cards, Software—Practice & Experience, v.32 n.4, p.319-340, 10 April 2002 [doi>10.1002/spe.438]
• 31: Xavier Leroy, Java Bytecode Verification: Algorithms and Formalizations, Journal of Automated Reasoning, v.30 n.3-4, p.235-269, 2003 [doi>10.1023/A:1025055424017]
• 32: Tim Lindholm , Frank Yellin, Java Virtual Machine Specification, Addison-Wesley Longman Publishing Co., Inc., Boston, MA, 1999
• 33: Alan Mycroft, Completeness and predicate-based abstract interpretation, Proceedings of the 1993 ACM SIGPLAN symposium on Partial evaluation and semantics-based program manipulation, p.179-185, June 14-16, 1993, Copenhagen, Denmark [doi>10.1145/154630.154648]
• 34: David Naccache , Alexei Tchoulkine , Christophe Tymen , Elena Trichina, Reducing the Memory Complexity of Type-Inference Algorithms, Proceedings of the 4th International Conference on Information and Communications Security, p.109-121, December 09-12, 2002
• 35: George C. Necula, Proof-carrying code, Proceedings of the 24th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.106-119, January 15-17, 1997, Paris, France [doi>10.1145/263699.263712]
• 36: Zhenyu Qian, Standard fixpoint iteration for Java bytecode verification, ACM Transactions on Programming Languages and Systems (TOPLAS), v.22 n.4, p.638-672, July 2000 [doi>10.1145/363911.363915]
• 37: Antoine Requet, A B model for ensuring soundness of a large subset of the java card virtual machine, Science of Computer Programming, v.46 n.3, p.283-306, March 2003 [doi>10.1016/S0167-6423(02)00095-3]
• 38: Eva Rose, Lightweight Bytecode Verification, Journal of Automated Reasoning, v.31 n.3-4, p.303-334, 2003 [doi>10.1023/B:JARS.0000021015.15794.82]
• 39: Rose, E. and Rose, K. 1998. Lightweight bytecode verification. In Proceeding of the Workshop on the Formal Underpinning of Java.
• 40: Ward, M. 1942. The closure operators of a lattice. Annals Math. 43, 2, 191--196.

INDEX TERMS

Primary Classification:
  D. Software
  D.3 PROGRAMMING LANGUAGES
      D.3.1 Formal Definitions and Theory

Additional Classification:
  C. Computer Systems Organization
  C.3 SPECIAL-PURPOSE AND APPLICATION-BASED SYSTEMS
      Subjects: Smartcards

  F. Theory of Computation
  F.3 LOGICS AND MEANINGS OF PROGRAMS
      F.3.1 Specifying and Verifying and Reasoning about Programs
          Subjects: Mechanical verification

General Terms:
Theory, Verification

Keywords:
Abstract interpretation, bytecode verification