Sciweavers

Share
TOPLAS
2008

Decomposing bytecode verification by abstract interpretation

10 years 11 months ago
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...
Cinzia Bernardeschi, Nicoletta De Francesco, Giuse
Added 15 Dec 2010
Updated 15 Dec 2010
Type Journal
Year 2008
Where TOPLAS
Authors Cinzia Bernardeschi, Nicoletta De Francesco, Giuseppe Lettieri, Luca Martini, Paolo Masci
Comments (0)
books