Defensive Java Virtual Machine Version 0.5 alpha Release. Built in ACL2.
923d0c210fb0b95a1401ef4399bd66906ef94c5d9e4a15ea88925bdd27370025<head><title>Defensive Java Virtual Machine Announcement</title></head>
<body text=#000000>
<body bgcolor="#FFFFFF">
<img src ="./html-0.5/maroon-line.gif" align=left><br>
<h1>Defensive Java Virtual Machine<br>
Version 0.5 alpha Release</h1>
<h3>May 13, 1997</h3><br>
<img src ="./html-0.5/maroon-line.gif" align=left><br><p>
Over the last several months Computational Logic, Inc. (CLI) in
collaboration with <a href="http://www.slb.com/et/">Schlumberger
Electronic Transactions</a> and <a href="http://www.javasoft.com/">
JavaSoft</a>
(see <a href="http://www.javasoft.com/forum/securityForum.html">"Where
is JavaSoft going with its model" in the original Javasoft announcement</a>)
has been building a formal model of a subset of the Java Virtual Machine
(JVM). The model has been built using ACL2, a mathematical logic
based on Common Lisp. The result can serve as the basis for
rigorous, formal analysis of the JVM and JVM (bytecode) programs. Because
models written in ACL2 can be executed, the formal JVM
model can run programs within the subset of the JVM supported.<p>
The model is called the "defensive" JVM (or dJVM) because it includes
sufficient run-time checks to assure type-safe execution (or at least
to detect and prevent any unsafe execution). In the standard JVM
these checks are not present; type safety is dependent an unstated
property of the bytecode verifier and the JVM.<p>
The first phase of the CLI effort has been to build an initial model
of a significant portion of the Java Card subset of the JVM. This
includes object creation, field access, and method invocation. This
phase has been completed, and CLI and its collaborators are making the
"alpha" release of the initial model publicly available for external
review and comment. This snapshot demonstrates one
approach to formalizing and clarifying the JVM specification.<p>
<h3>Availability</h3>
The draft formal description of the model is available.
Please mail any comments to <a href="mailto:cohen@cli.com">Richard Cohen.</a>
<ul>
<li> <a href="./html-0.5/djvm-report.html">HTML version</a>.</li>
<li> The full report can be downloaded as a
<a href="ftp://dirleton.csres.utexas.edu/pub/djvm/djvm-report.ps">postscript</a> or <a
href="ftp://dirleton.csres.utexas.edu/pub/djvm/djvm-report.pdf">pdf</a> file. Each is approximately 2MB.</li>
</ul><p>
<blockquote><small>NOTE: The HTML version was generated mechanically from LaTeX
sources generated mechanically from the ACL2 source files. While this
has produced a readable hyper-linked rendition, there are a number
of minor formatting glitches. For the authoritative documentation see
the report.</small></blockquote><p>
The model is available as gzipped or compressed TAR files which
include an executable image and the dJVM 0.5 <cite>User's Guide</cite> in PostScript and PDF
formats:
<ul>
<li> Gzipped for <a href="ftp://dirleton.csres.utexas.edu/pub/djvm/djvm0.50.sunos-5.sun4.tar.gz">Solaris 2.5 on SPARC architecture.</a>(31 megabytes)</li>
<li> Compressed for <a href="ftp://dirleton.csres.utexas.edu/pub/djvm/djvm0.50.sunos-5.sun4.tar.Z">Solaris 2.5 on SPARC architecture.</a>(38 megabytes)</li>
<li> Gzipped for <a href="ftp://dirleton.csres.utexas.edu/pub/djvm/djvm0.50.sunos-5.i86pc.tar.gz">Solaris 2.5 on x86 architecture.</a>(26 megabytes)</li>
<li> Compressed for <a href="ftp://dirleton.csres.utexas.edu/pub/djvm/djvm0.50.sunos-5.i86pc.tar.Z">Solaris 2.5 on x86 architecture.</a>(37 megabytes)</li>
</ul><p>
<blockquote>
WARNING: The current executable images are very large; they are
approximately 70MB each when expanded. The gzipped versions are about
30 MB. The image includes the executable dJVM model
as well as the complete ACL2 theorem prover, compiler, and all of the
definitions and theorems of the dJVM model.
</blockquote><p>
The <cite>User's Guide</cite> briefly explains how to run the model
and is available as a <a href="ftp://dirleton.csres.utexas.edu/pub/djvm/djvm-guide.ps">postscript</a> or
<a href="ftp://dirleton.csres.utexas.edu/pub/djvm/djvm-guide.pdf">pdf</a> file.
The ACL2 source files comprising the model are also
available as a <a href="ftp://dirleton.csres.utexas.edu/pub/djvm/djvm0.50.sources.tar.gz">gzipped tar file
(300KB) </a>.<p>
<small>Java, Java Card and Solaris are trademarks of Sun Microsystems, Inc.
SPARC is a trademark of SPARC International, Inc.</small>
<h6><EM>This page is URL http://www.cli.com/software/djvm/index.html </h6></EM>
© 2024 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