Bytecode, such as produced by e.g. Java and .NET compilers, has become an important topic of interest, both for industry and academia. The industrial interest stems from the fact that bytecode is typically used for Internet and mobile devices (smart-cards, phones, etc.) applications, where security is a major issue. Moreover, bytecode is device-independent and allows dynamic loading of classes, which provides an extra challenge for the application of formal methods. In addition, the unstructuredness of the code and the pervasive presence of the operand stack also provide extra challenges for the analysis of bytecode. This workshop will focus on theoretical and practical aspects of semantics, verification, analysis, certification and transformation of bytecode.
|09:00||Invited Speaker: Francesco Logozzo (Microsoft Research, USA)
Language-agnostic Contract specification and checking with CodeContracts and Clousot
|10:00||Jacek Chrzqszcz, Patryk Czarnik and Aleksy Schubert (The University of Warsaw, Poland)
A dozen instructions make Java bytecode
One of the biggest obstacles in the formalisation of the Java bytecode is that the language consists of 200 instructions. However, a rigorous handling of a programming language in the context of program verification and error detection requires a formalism which is compact in size. Therefore, the actual Java bytecode instruction set is never used in the context. Instead, the existing formalisations usually cover a 'representative' set of instructions. This paper describes how to reduce the number of instructions in a systematic and rigorous way into a managable set of more general operations that cover the full functionality of the Java bytecode. The factorisation of the instruction set is based on the use of the runtime structures such as operand stack, heap etc. This is achieved by presentation of a formal semantics for the Java Virtual Machine.
|11:00||Invited Speaker: Mark Marron (IMDEA Software, Spain)
Spec-tacular: heap assertions for .net bytecode
|12:00||Jaroslav Bauml and Premek Brada (University of West Bohemia, Czech Republic)
Reconstruction of Type Information from Java Bytecode for Component Compatibility
The Java type system is strictly checked by both the compiler and the runtime bytecode interpreter of the JVM. These mechanisms together guarantee appropriate usage of class instances. Using modern component systems can however circumvent these static checks, because incompatible versions of classes can be bound together during component installation or update. Such problematic bindings result in ClassCastException or NoSuchMethodException runtime errors. In this paper we describe a representation of Java language types suitable for checking component compatibility. The presented approach applies various bytecode handling techniques to reconstruct a representation of the Java types contained in a component implementation, using different sources of class data. The representation is then used during build- and run-time type system verifications with the aim to prevent these kinds of errors. We have successfully applied this approach to prevent OSGi component incompatibilities.
|14:00||Invited Speaker: Matthew Parkinson (University of Cambridge, UK)
The design of jStar
|15:00||Philippe Wang, Adrien Jonquet and Emmanuel Chailloux (LIP6-UPMC, France)
Non Intrusive Structural Coverage for Objective Caml
This paper presents a non-intrusive method for Objective Caml code coverage analysis. While classic methods rewrite the source code to an instrumented version that will produce traces at run time, our approach choses not to rewrite the source code. Instead, we use a virtual machine to monitor instructions execution and produce traces. These low-level traces are used to produce a machine code coverage report. Combined with control-flow debug information, they can be analyzed to produce a source code coverage report. The purpose of this approach is to make available a method to generate code coverage analysis with the same binary for testing and for production. Our customized virtual machine respects the same semantics as the original virtual machine; one of its original aspects is that it is implemented in the Objective Caml, the very language we build the tool for. This work is part of the Coverage project, which aims to develop open source tools for safety-critical embedded applications and their code generators.
|15:30||Jevgeni Kabanov (Tartu University, Estonia)
JRebel Tool Demo
JRebel started as an academical project that became a successful commercial product used by thousands of developers worldwide. It extends the Java Virtual Machine with a mechanism that allows seamless class reloading. It uses bytecode manipulation extensively, both for the just-in-time class translator and numerous integrations with the Java SE and EE APIs. In this live demo we will show how it can be used in real-life projects to cut development time by 8 to 18 per cent.
|16:30||Invited Speaker: Fausto Spoto (University of Verona, Italy)
Static Analysis of Java: from the Julia Perspective
Verification of real software is recognised as an important topic in software development. Automatic software analysis tools for Java play a prominent role there. They are on main street since a long time now and keep improving every year. We discuss here some of their distinctive aspects, such as genericity, need of annotations, modularity, correctness, precision, real-time and scalability, with some focus on the Julia tool for static analysis of Java bytecode. We then discuss their most notable limitations and their perspective, identifying multi-threading as both the nightmare of next generation tools and a promise for better scalability and efficiency.
|17:30||Michael Eichberg and Andreas Sewe (Technische Universität Darmstadt, Germany)
Encoding the Java Virtual Machine's Instruction Set
New toolkits that read in, analyze, and transform Java Bytecode are regularly developed from scratch to get a representation suitable for a particular purposes. Nevertheless, the functionality implemented by the toolkits to read in class files and do basic control- and data-flow analyses is comparable and is implemented over and over again. Differences mainly manifest themselves in minor technical issues. To avoid the repetitive development of similar functionality, we have developed an XML-based language for specifying bytecode based instructions. Using this language, we have encoded the instruction set of the Java Class File Format such that it can directly be used, e.g., to generate the skeleton of bytecode-based tools. The XML format specifies (a) the format of the instructions and (b) the effect of each instruction on the stack and the local registers when the instruction is executed. This enables to generate generic control- and data-flow analyses such as an analysis that converts Java Bytecode into static single assignment form. To assess the usefulness of our approach, we have used the encoding of the Java Class Format to develop a framework to analyze and transform Java class files. The evaluation shows that using the specification significantly reduces the development effort when compared with manual development.
|December 14, 2009|
|December 21, 2009|
|January 22, 2010|
|February 19, 2010|
Call For Papers[.txt]
SubmissionPaper should be submitted through the easy chair page.
- David Aspinall, University of Edinburgh, Scotland
- Stephen Chong, Harvard University, USA
- Alessandro Coglio, Kestrel Institute, USA
- Pierre Crégut, Orange Labs, France Télécom, France
- Samir Genaim, Complutense University of Madrid, Spain
- Bart Jacobs, Katholieke Universiteit Leuven, Belgium
- Gerwin Klein, University of New South Wales, Australia
- Victor Kuncak, EPFL, Switzerland
- Patrick Lam, University of Waterloo, Canada
- Francesco Logozzo, Microsoft Research, USA
- Matthew Parkinson, University of Cambridge, UK
- David Pichardie (chair), INRIA Rennes, France
- Rene Rydhof Hansen, Aalborg University, Denmark
- Fausto Spoto, University of Verona, Italy