This workshop ran on Sunday 19 October. Over forty people attended. Approximately 55% of the attendees came from universities and most of the rest came from research centres. There were fourteen talks, half about Java bytecode. Proceedings are available from the web.

This workshop ran on Sunday 19 October. Over forty people attended. Approximately 55% of the attendees came from universities and most of the rest came from research centres. There were four attendees from various parts of Sun.

The workshop brought together people who were interested in the application of formal methods to the Java paradigm. Formal methods helps to provide a better understanding of the approach by rigorously formulating and trying to prove some of the guarantees made by Java. It also aims to provide some guidance for further development of the paradigm by uncovering possible design flaws and by supplying a platform for the description of future extension. The areas covered by the workshop included the semantics of both Java and bytecode, correctness of the bytecode verifier and verification of Java programs.

There were fourteen talks including two from invited speakers. The two invited speakers were Martín Abadi, from Compaq Systems Research Center, and Gilad Bracha, from Sun Java Software.

The workshop started with an invited talk by Martín Abadi of Systems Research Center Compaq. His talk was entitled Understanding Java: from languages to systems.

Martín Abadi started his talk by asking "What is in the `Java paradigm'? " Were we just interested in the Java language, or just the Java bytecode language (JVML) or Java, JVML and the libraries? Were we interested in the Java Virtual Machine (JVM), or the systems in which these are embedded? Are we interested in Jini and all related languages, libraries, and systems?

He observed that we have done well on individual languages (``physics''), less well on systems (``chemistry''). Decades of formal work on type theory, logics, and semantics have not been completely in vain. The results of that work apply to Java. Several standard concepts and techniques have been adapted to Java with moderate effort such as type soundness and program­verification methods. Some trouble spots (e.g., dynamic linking) can be explained fairly formally. This should not be completely surprising.

A coherent, formal study of the complete Java language is still work in progress. Martín Abadi would like to see more work on a precise, useful Java memory model. Since threads and locks are part of the language, a good model should help in verification and in optimization (e.g., code motion). He would also like to see more practical program verification. Conversely, Martín Abadi sees Java as helping to focus formal work.

In parallel with the Java language work, JVML has been treated rigorously. We have obtained definitions and theorems, and a handle on trouble spots (e.g.., interaction of initialization and subroutines).

A coherent, formal study of JVML is still work in progress. But (roughly) JVML is no harder than Java. Formal work has not yet led to more uniform or efficient JVMs.

It is not entirely clear what all the formal methods work has to do with security. An implementation of Java should be functionally correct, even in interaction with malicious systems that are not the result of compiling Java.

Common Java compilers produce JVML code. This code is trusted code. Hostile JVML code can be created and is not to be trusted. Java Virtual Machines execute JVML code within web browsers and as applications. Bytecode verifiers are supposed to ensure that bytecode can be trusted.

Bytecode verification ensures that the binary representation of a class or interface is structurally correct. For example, it checks that every instruction has a valid operation code; that every branch instruction branches to the start of some other instruction, rather than into the middle of an instruction; that every method is provided with a structurally correct signature; and that every instruction obeys the type discipline of the Java language.

It is unusual to have two languages, in this case Java and JVML where one is defined by referencing the other. When does JVML code ``obey the type discipline of the Java language?'' ``The question is,'' said Alice, ``whether you can make words mean so different things.''

The idea of ``full abstraction'' is useful for understanding the security of implementations in the case of Java, for communication abstractions (e.g., RMI), perhaps in general.

Loosely, two programs are equivalent in a language if they have the same observable behavior in all contexts of the language. A translation is fully abstract if it respects equivalence.

Privacy at the JVML level can be important for protection against mobile objects. Java libraries interact with mobile code at the JVML level. Inter­applet communication may remain at the JVML level. Privacy in JVML is less meaningful for protection of mobile objects. Mobile objects on untrusted machines are subject to lower­level attacks.

For security, one cannot ignore type errors, operand stack overflow or underflow, or access control violations. The bytecode verifier helps prevent errors by checking untrusted JVML code before execution. But bytecode verification is not clearly the same as security.

There are discrepancies between Java and JVML. One area is exceptions in Java. The handler for an exception is never inside the code that the handler protects, in JVML it may be.

In the Java language, method calls and locking are nicely nested (so locks can be placed on the stack). JVML allows fairly arbitrary patterns of monitorenter and monitorexit operations.

Although qualifiers like private appear in both Java and JVML, they may not provide the same guarantees. Java has inner classes but there is no support for them in JVML. Something declared as private in a package with inner classes cannot be respected within JVML.

Rich Cohen, of EDS Austin Technology Service Center, gave a talk entitled Formal Underpinnings of Java:Some Requirements. He started out by asking why we should have a formal underpinnings for Java and answered that we would like to be able to execute a mixture of trusted and untrusted JVM classes with confidence that an untrusted class cannot take advantage of the authority/capabilities of a trusted class. We look to formal specifications and proofs to bolster our confidence and move us toward this goal. Many researchers have attacked sub-problems and Rich wants to that we don't lose sight of the higher-level goal toward which these pieces build; and to make sure that we don't confuse primary safety properties of a system with secondary, or derived, properties of components.

As it is JVM code that executes, we should concentrate there rather than at the language level. The static typing constraints embodied in bytecode verification should be sufficient to assure safe execution, but are not necessary. Static typing constraints are defined only in service of efficient compilation and execution. The goal is type-safe execution. The specification for the bytecode verifier is that it only accepts programs whose dynamic behavior is type safe. The formal specification will be long. Tools are needed to keep it consistent and to help with proofs. Rich then outlined what formal work he thought would be useful.

Stephen Freund of the Department of Computer Science at Stanford gave a talk on The Costs and Benefits of Java Bytecode Subroutines. Java bytecode subroutines are used to compile the Java source language try-finally construct into a succinct combination of special-purpose instructions. However, the space saved by using subroutines, in comparison to simpler compilation strategies, comes at a substantial cost to the complexity of the bytecode verifier and other parts of the Java Virtual Machine. Freund’s talk examined the trade-off between keeping subroutines and eliminating them from the Java bytecode language. He compared the cost of formally specifying the bytecode verifier and implementing the Java Virtual Machine in the presence of subroutines, to the space saved by using them when compiling a set of representative Java programs.

Given the important role of the verifier in the Java paradigm and the many difficulties in both specifying and implementing correct verification methods for subroutines, a natural question to ask is whether or not the benefits of subroutines justify the specification and implementation costs. Eliminating subroutines would not affect the semantics of Java. The only difference would be the compilation strategy for methods, which use try-finally or other statements currently compiled using subroutines. The easiest way, to translate a try-finally block of Java code into JVML without subroutines, requires some amount of code duplication, with an exponential blow up in code size in the worst case. Removing subroutines from JVML would greatly simplify the verifier, as well as possible implementations of other parts of the Java Virtual Machine, such as type-precise garbage collectors.

Subroutines significantly complicate the static analysis for object initialization and constructors at the bytecode level, complicate the checking of exception handlers, and necessitate the introduction of some notion of polymorphic local variables into all aspects of the type system.

Given the difficulty in understanding and specifying type checking for bytecode subroutines, it is not surprising that creating an implementation, which handles subroutines correctly, has also been difficult. One may see this just by looking at the history of bugs and inconsistencies found in the early versions of the Sun verifier.

Conservative garbage collection schemes based on computing reachability from a set of root references can only be replaced by exact collection strategies if the garbage collector is able to determine which local variables contain object references at all appropriate collection points in a program.

Fruend looked at the benefits of using subroutines by measuring the reduction in code size obtained by using subroutines over duplication of code for synchronized and try-finally statements. Code inflation is typically linear in the number of calls to subroutines, but if subroutine calls are nested in a certain way, there could be an exponential blow up in size. To measure the effect in realistic programs, several large programs and libraries were analyzed, as well as many smaller applets and applications. To put the measured savings into perspective, he computed the number of bytes saved by subroutines in the JDK as about 2,200 bytes. The size of all the class files for the JDK is about 8.7MB, making the space saved by subroutines approximately 0.02% of the total size. To put this in perspective, Freund told us that all symbolic names mentioned in the source code are also stored as strings represented as arrays of bytes in the class files. As such, the word java appears roughly 30,000 times in the class files for the JDK. If Sun had stuck with Oak, the original name for the Java language project, the shorter name would have saved 13 times as much space as subroutines do in the compilation of the JDK.

Freund’s measurements of various programs indicated that, while fears of code size inflation are reasonable, it is not encountered in any of the programs studied. Only a handful of all the methods in his test cases were significantly smaller due to subroutines.

Mark Jones of the Department of Computer Science, University of Nottingham, gave a talk entitled The Functions of Java Bytecode. Java bytecode provides a portable representation for programs that allows executable content to be embedded in web pages, transferred across a network, and executed on a remote user's machine. Features like these provide many new opportunities for developers, but special precautions must be taken to protect users from badly-behaved programs, which might otherwise destroy valuable data or compromise their privacy. To avoid such problems, bytecode programs from untrusted sources must be verified before they are used. If a program passes, then it should be well-behaved, and should not be able to subvert the other security mechanisms of the Java

platform. However, if a program fails, then it will be rejected.

Clearly, to be sure that it is effective, we need a precise way to understand bytecode verification. Jones described the main features of a formal specification for Java bytecode that allows us to reason about the correctness of Java implementations, and to guarantee safety properties of verified bytecode. The key to his approach is to model individual bytecode instructions, and their compositions, as appropriately typed functions in a fairly standard functional language. This gives a flexible way to build up and extend the instruction set. In addition, it enables the description of bytecode verification as a well-understood form of type inference, which guarantees that execution of verified programs will not go wrong.

Michael Anthony Smith of Systems Assurance Group, Defence Evaluation and Research Agency, gave a talk entitled Type-based Assessment of the Java Byte-level Language. The Systems Assurance Group (SAG) is involved in software assessment for security and safety related (or critical) systems. During, the last year they have been investigating the Java bytecode. The aim has been to understand the subtleties of this language, to provide a basis for assessing software systems that use the Java technology. This requires an accurate and unambiguous interpretation of the Java Virtual Machine (JVM) specification.

It was decided to start by providing a formal type-based description for each of Java's byte-level operations; as such rules (with an appropriate environmental model) can unambiguously capture many of the specified properties (e.g. memory integrity).

This talk presented an overview of SAG's initial approach. It started with an outline of the approach, followed by a brief discussion of the related work. Then it described the constant aspects of the formal model that underpin the approach, which included an overview of the type-system and class file inheritance structure. This was followed by a description of the concrete and abstract representations of a class-file's method, indicating why both are desirable (although not strictly necessary). Next, an outline of the structure of the type-based rules (including a few examples) was presented. Finally, a summary of what has been achieved and SAG's intentions for the future was given. SAG's approach is aimed at software assessment rather than development.

It is targeted at software products that the assessors have no control over, such as commercial off the shelf (COTS) products. Therefore, the only valid reasons for rejecting such a product are that it can be shown not to satisfy a given safety (or security) property; or that it is not cost-effective to demonstrate such a property. This means that an assessment tool based on this approach should aim to cope with the full complexity of the byte-level language, rather than enforcing a particular style of programming (e.g. no overlapping exception handlers). SAG's approach is based on applying a type-based theory to each of Java's bytecode operations, including the exception handling mechanism; as the exception handling mechanism is an integral part of the Java language, and thus cannot be avoided or ignored.

To date the work has focussed on investigating a single method within a class-file. This has produced both a concrete and an abstract model of the Java class-file's method format, along with a collection of type-based rules for most of the bytecode operations (i.e. a method's algorithm).

Harald Vogt of Technologiezentrum Deutsche Telekom, Germany gave a talk entitled Java Bytecode Verification Using Model Checking. They provide an abstract interpretation for Java bytecode in order to build finite state models of bytecode programs. The bytecode constraints for assuring safety are formulated in terms of temporal logic formulae. These formulae are checked against the finite program models by a (standard) model checker. By doing so they see a practical way to perform bytecode verification on a formal basis. This could help to achieve higher security and open the door for further extensions to prove additional properties of Java bytecode.

Alessandro Coglio of Kestel Institute gave the final talk of the morning. Entitled Toward a Provably-Correct Implementation of the JVM Bytecode Verifier, he described their ongoing efforts to realize a provably-correct implementation of the Java Virtual Machine bytecode verifier. They take the perspective that bytecode verification is a dataflow analysis problem, or more generally, a constraint-solving problem on lattices. They employ Specware , a system available from Kestrel Institute that supports the development of programs from specifications, to formalize the bytecode verifier and to formally derive an executable program from their specification.

The afternoon session was started off with an invited talk from Gilad Bracha entitled Formal Underpinnings of the Java^TM Platform: A Perspective from Sun. Bracha, from Sun Java Software calls himself a Computational Theologist. He thinks that the promising issues for formal study are wherever innovation has occurred. In particular he thinks we should look at bytecode verification, dynamic loading and resolution, binary compatibility, memory models and concurrency, nested classes, packages, and exceptions

Sun want features modeled as they are rather than, as we would like them to be. We should be careful of what simplifying assumptions we make. For example there is no need to model all 250 bytecodes but we must make sure we don’t skip over the controversial ones such as subroutine calls. When we are unsure of how Java is supposed to behave we should get in touch with Sun and just ask.

Some of the things they would like to have modeled include verifying the use of interfaces and class loading. Sun has seen benefits from the research work into the foundational underpinnings of Java. Some specific examples, but by no means a complete list, would include that work done by Abadi and Stata and the work done by Freund and Mitchell gave new insights, especially with respect to subroutines and object initialization. Qian’s work on bytecode verification was more realistic then most verifier work. - Rose offers intriguing possibilities for the future, based on theoretical insight. Saraswat provided new insights with his work, which first discussed interaction of class loaders and type safety informally and then followed on with a formal analysis.

Commonly, it is assumed that verification has to be performed off-card and shipped by means of cryptographic protection techniques, e.g., digital signatures, to ensure that the bytecode is not tampered with after it has been verified. These techniques, however, create a single point of failure trust because of their dependence on a secret (private) key. This is particularly serious when dealing with embedded systems with a very wide distribution such as Java Cards.

Eva Rose's talk proposed an alternative solution by splitting the verification process in two parts. There should be an off-card part, where sufficient verification information is constructed as a verification certificate to be sent together with the bytecode. And there should be an on-card part, where the remaining verification is performed as a check of the code and the certificate, the lightweight verification, which has the advantage of running in a reasonable almost constant space (and almost linear time).

Eva Rose gave a formal specification of the two components for a subset of Sun’s Java Card Language, sufficiently strong to write non-trivial downloadable applets. She proved that the technique is tamper-proof by showing it both sound and complete with respect to standard bytecode verification. Finally she argued that her approach is safer than usual bytecode verification because it isolates a non-complex safety-critical component, the bytecode checker.

Cornelia Pusch of the Institut für Informatik, Technische Universität München, Germany gave a talk entitled Proving the Soundness of a Java Bytecode Verifier in Isabelle/HOL. She said that the group she is in has formalized large parts of the Java Virtual Machine (JVM) with the theorem prover Isabelle/HOL. They provide an operational semantics for each instruction in a context of the current state. They then formalized a specification for a Java bytecode verifier and formally proved the soundness of the specification. She believes this is the first verifier formalization that has been aided by a theorem prover.

Gary T. Leavens of the Department of Computer Science, Iowa State University gave a talk called JML: a Java Modeling Language. He told the audience that JML is a behavioral interface specification language tailored to Java. It also allows assertions to be intermixed with Java code, as an aid to verification and debugging. JML is designed to be used by working software engineers, and requires only modest mathematical training. To achieve this goal, JML uses Eiffel-style assertion syntax combined with the model-based approach to specifications typified by VDM and Larch. However, JML supports quantifiers, specification-only variables, frame conditions, and other enhancements that make it more expressive for specification than Eiffel. The talk discusses the goals of JML, the overall approach, and prospects for giving JML a formal semantics through a verification logic.

Gianna Reggio of the Dipartimento di Informatica e Scienze dell'Informazione Universita di Genova in Italy gave a talk entitled A Proposal for a Semantics of a Subset of Multi-Threaded " Java Programs. She was interested in modeling multi-threaded Java programs, to improve understanding, and to provide a formal basis for checking the correctness when turning design specifications into code. She chose to develop a structural operational semantics because it provided a formal but simple and natural description of Java. In her approach, multi-threaded Java programs are modeled by a labeled transition system (lts), that is two sets describing, respectively, the intermediate interesting states of the program execution and the information exchanged with the external environment during such execution, plus a transition relation. Any transition of the model describes the execution of an atomic step in the computation.

A program has an internal structure, which can be identified as components with independent activity. Such components are modeled by a lts too. A set of inductive rules describes the transitions of the model and gives the operational, structured semantics of the language in a simple and intuitive way. Since it is not possible to simply associate a result with a multi-threaded Java program, it is absolutely necessary to have a correct observational semantics and, consequently, an equivalence notion to test if two programs are equivalent.

The Java memory model has both main and working memory and it is possible to write programs that behave in insensible ways. Gianna Reggio then looked at the set of Java programs

whose threads’ behavior was well behaved. The operational semantics for this subset of Java was much simpler than that for the full multi-threaded Java.

Marjorie Russo of Sophia Antipolis Cedex, France gave a talk entitled A Formal Executable Semantics for Java. Some of the main features of the Java language are that it is object- oriented and multi-threaded. Russo presented a formal semantics of a large subset of Java, including inheritance, dynamic linking and multi-threading. To describe the object-oriented features, she used a big-step semantics. The semantics of the concurrency is defined in a small-step semantics, using a structural operational semantics. This semantics is directly executable using the Centaur system. An interactive programming environment, which provides textual and graphical visualization tools during program execution, is derived from this semantics.

Dyke Stiles of the Electrical and Computer Engineering Department at Utah State gave a talk on the Safe and Verifiable Design of Multithreaded Java Programs with CSP and FDR. He said that since Java may used to develop code for life-, safety-, and mission-critical embedded systems; multithreaded applications we must ensure that these applications are free from deadlock and livelock. These problems can be eliminated by basing designs on the structures and formalisms of Hoare's Communicating Sequential Processes (CSP). Java class libraries supporting CSP constructs exist so programmers can to take advantage of these methods. CASE tools are available to automatically check CSP designs for deadlock and livelock and to validate implementations against specifications.

The last session in the workshop was devoted to wrapping up. We discussed that the complete picture is still missing. We are not ready to unify our work and we discussed what were the issues that we should work on next. Drew Dean suggested that we think about the problems that arise between different parts of the Java system. He showed us peculiar code where both the class loader and the verifier assume that the other is dealing with the problems it posed.

We also discussed that the specification of Java consists of several large natural language books. We asked the Sun attendees whether there was any way that the next version of the specification could be more precise and shorter. They said that they too would benefit from such a specification.

Kristoffer Rose wanted the people who were dealing with bytecode to go to the JavaOne Conference and put their work to the scrutiny of application developers. In general, it was felt that our work was not mature enough for this type of scrutiny.

The workshop was held in a room with wonderful views. Burrard Inlet provided an alternative view to the speakers. The programme and papers are available from www-dse.doc.ic.ac.uk/~sue/oopsla/cfp.html.

Susan Eisenbach

November 1998