Abstract
Lightweight bytecode verification uses stack maps to annotate Java bytecode programs with type information in order to reduce the verification to type checking. This paper describes an improved bytecode analyser together with algorithms for optimizing the stack maps generated. The analyser is simplified in its treatment of base values (keeping only the necessary information to ensure memory safety) and enriched in its representation of interface types, using the Dedekind-MacNeille completion technique. The computed interface information allows to remove the dynamic checks at interface method invocations. We prove the memory safety property guaranteed by the bytecode verifier using an operational semantics whose distinguishing feature is the use of untagged 32-bit values. For bytecode typable without sets of types we show how to prune the fix-point to obtain a stack map that can be checked without computing with sets of interfaces i.e., lightweight verification is not made more complex or costly. Experiments on three substantial test suites show that stack maps can be computed and correctly pruned by an optimized (but incomplete) pruning algorithm.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Barthe, G., Dufay, G., Jakubiec, L., Melo de Sousa, S.: A formal correspondence between offensive and defensive javacard virtual machines. In: Cortesi, A. (ed.) VMCAI 2002. LNCS, vol. 2294, pp. 32–45. Springer, Heidelberg (2002)
Besson, F., Jensen, T., Turpin, T.: Computing stack maps with interfaces. Technical Report 1879, Irisa (2007)
Besson, F., Jensen, T., Turpin, T.: Small witnesses for abstract interpretation-based proofs. In: De Nicola, R. (ed.) ESOP 2007. LNCS, vol. 4421, pp. 268–283. Springer, Heidelberg (2007)
Bracha, G., Lindholm, T., Tao, W., Yellin, F.: CLDC Byte Code Typechecker Specification. Sun Microsystems (2003)
Cousot, P., Cousot, R.: Abstract interpretation: A unified lattice model for static analysis of programs by construction of approximations of fixpoints. In: Proc. of the 4th ACM Symp. on Principles of Programming Languages (POPL 1977), pp. 238–252. ACM Press, New York (1977)
Davey, B.A., Priestley, H.A.: Introduction to Lattices and Order, 2nd edn. Cambridge University Press, Cambridge (1990)
Freund, S.N., Mitchell, J.C.: A type system for the java bytecode language and verifier. Journal of Automated Reasoning 30(3-4), 271–321 (2003)
Goldberg, A.: A specification of java loading and bytecode verification. In: Proc. of the 5th ACM conference on Computer and Communications Security (CCS 1998), pp. 49–58. ACM Press, New York (1998)
JSR 202 Expert Group. Java Class File Specification Update, Sun Microsystems (2006)
Knoblock, T.B., Rehof, J.: Type elaboration and subtype completion for java bytecode. ACM Transactions on Programming Languages and Systems 23(2), 243–272 (2001)
Leroy, X.: Java bytecode verification: algorithms and formalizations. Journal of Automated Reasoning 30(3-4), 235–269 (2003)
Leroy, X., Rouaix, F.: Security properties of typed applets. In: Proc. of the 25th ACM Symp. on Principles of Programming Languages (POPL 1998), pp. 391–403. ACM Press, New York (1998)
Lindholm, T., Yellin, F.: The Java Virtual Machine Specification, 2nd edn. Prentice-Hall, Englewood Cliffs (1999)
Pusch, C.: Proving the soundness of a java bytecode verifier specification in isabelle/hol. In: Cleaveland, W.R. (ed.) TACAS 1999. LNCS, vol. 1579, pp. 89–103. Springer, Heidelberg (1999)
Qian, Z.: A formal specification of java virtual machine instructions for objects, methods and subrountines. In: Formal Syntax and Semantics of Java, pp. 271–312 (1999)
Rose, E.: Lightweight bytecode verification. Journal of Automated Reasoning 31(3-4), 303–334 (2003)
Seo, S., Yang, H., Yi, K., Han, T.: Goal-directed weakening of abstract interpretation results. ACM Transactions on Programming Languages and Systems 29(6), 39 (2007)
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 2008 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Besson, F., Jensen, T., Turpin, T. (2008). Computing Stack Maps with Interfaces. In: Vitek, J. (eds) ECOOP 2008 – Object-Oriented Programming. ECOOP 2008. Lecture Notes in Computer Science, vol 5142. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-70592-5_27
Download citation
DOI: https://doi.org/10.1007/978-3-540-70592-5_27
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-70591-8
Online ISBN: 978-3-540-70592-5
eBook Packages: Computer ScienceComputer Science (R0)