Decomposing bytecode verification by abstract interpretation

act Interpretation C. BERNARDESCHI, N. DE FRANCESCO, G. LETTIERI, L. MARTINI, and P. MASCI Universit`a di Pisa 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 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 ystems. The method is formalized in the framework of abstract interpretation. Categories and Subject Descriptors: D.3.1 [Programming Languages]: Formal Definitions and Theory; F.3.1 [Logics and Meanings of Programs]: Specifying and Verifying and Reasoning about Programs--Mechanical verification; C.3 [Com...

• Type: Journal
• Year: 2008
• Where: TOPLAS
• Authors: Cinzia Bernardeschi, Nicoletta De Francesco, Giuseppe Lettieri, Luca Martini, Paolo Masci
• Keywords: Abstract Interpretation, Bytecode Verification, De Francesco, TOPLAS 2008