Workshop Description
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.
Program
| 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.
|
| 10:30 | coffee break |
| 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.
|
| 12:30 | lunch |
| 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:00 | coffee break |
| 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.
|
Important Dates
| December 14, 2009 | |
| December 21, 2009 | |
| January 22, 2010 | |
| February 19, 2010 |
Call For Papers
[.txt]Submission
Paper should be submitted through the easy chair page.Program Committee
- 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