A Type System for Java Bytecode Subroutines.
94b8f3b85c39948c444b417306a68857d124d0b9525e7246490eb11ff08cb363<HTML><HEAD><TITLE>
Digital Systems Research Center: Report 158</TITLE></HEAD>
<BODY><H1><IMG SRC=
"http://www.research.digital.com/digital/pics/DEC-logo.gif" ALT="d i g i t a l">
SRC Research Report 158</H1>
<H1>A Type System for Java Bytecode Subroutines</H1>
<HR>
<H2>Raymie Stata and Martin Abadi</H2>
<b>Report #158, June 11, 1998</b><BR><i>62 pages</i>
<P>
Java is typically compiled into an intermediate language, JVML, that
is interpreted by the Java Virtual Machine. Because mobile JVML code
is not always trusted, a bytecode verifier enforces static constraints
that prevent various dynamic errors. Given the importance of the
bytecode verifier for security, its current descriptions are
inadequate. This paper proposes using typing rules to describe the
bytecode verifier because they are more precise than prose, clearer
than code, and easier to reason about than either.
<P>
JVML has a subroutine construct which is used for the compilation of
Java's try-finally statement. Subroutines are a major source of
complexity for the bytecode verifier because they are not obviously
last-in/first-out and because they require a kind of polymorphism.
Focusing on subroutines, we isolate an interesting, small subset of
JVML. We give typing rules for this subset and prove their correctness.
Our type system constitutes a sound basis for bytecode verification
and a rational reconstruction of a delicate part of Sun's bytecode
verifier.
<P>
<p><b>Back to</b> the <a href='http://www.research.digital.com/SRC/publications/src-rr.html'>SRC Research Reports main page</a>.
<HR><B>Download report as:</B>
<P><UL>
<LI><B><A HREF="ftp://ftp.digital.com/pub/DEC/SRC/research-reports/SRC-158.ps.Z">PostScript compressed with UNIX compress</A></B> -- 776 Kbytes<BR>
<LI><B><A HREF="ftp://ftp.digital.com/pub/DEC/SRC/research-reports/SRC-158.ps.gz">PostScript compressed with GNU compress (gzip)</A></B> -- 736 Kbytes<BR>
<LI><B><A HREF="ftp://ftp.digital.com/pub/DEC/SRC/research-reports/SRC-158.ps.zip">PostScript compressed with ZIP</A></B> -- 736 Kbytes<BR>
<LI><B><A HREF="ftp://ftp.digital.com/pub/DEC/SRC/research-reports/SRC-158.ps">PostScript</A></B> -- 1464 Kbytes<BR>
<LI><B><A HREF="ftp://ftp.digital.com/pub/DEC/SRC/research-reports/SRC-158.pdf">Portable Document Format (PDF)</A></B> -- 336 Kbytes<BR>
</UL></P>
</BODY></HTML>
© 2022 Packet Storm. All rights reserved.
%7Cutmcsr%3D(direct)%7Cutmcmd%3D(none)){kind=small}
Follow us on Twitter
Follow us on Facebook
Subscribe to an RSS Feed