Verification of Java Bytecode using Transformation and Analysis Tools for Logic Programming

Version 0.3  ---  December 2006



In this web, we introduce our approach (and provide the tools required) to verify Java Bytecode in the (Constraint) Logic Programming paradigm --- (C)LP. In order to achieve this goal, we focus on the techniques of meta-programming, program specialisation and static analysis that together support the use of CLP tools to analyse JVML programs (i.e., programs written in the Java Virtual Machine Language).

A complete description of our approach can be found in [AGHP-PADL07].

The whole verification process is split in three main parts:


The Class Reader for Ciao (Download)

The files can be found here.

The JVMLr Interpreter in Ciao (Download)

Our JVMLr Interpreter expresses the JVM semantics and it is written in Ciao Prolog. The formal JVML specification chosen for our work is Bicolano, which is a superset of JVMLr. Bicolano is written with the Coq Proof Assistant which allows checking that the specification is consistent and also proving properties on the behavior of some programs.

The current files of the interpreter can be downloaded. This code can be structured in four main parts:

Transformation and Analysis in the CiaoPP System

You can use the partial evaluator integrated in CiaoPP to produce the residual programs and to analyze them later. CiaoPP is the precompiler of the CIAO Prolog development environment. It can perform a number of program debugging, analysis and source-to-source transformation (including partial evaluation) tasks on (CIAO) Prolog programs. CiaoPP is distributed under the GNU general public license. At this site, you will find all the information about CiaoPP (instructions for downloading, manuals, tutorials, etc.).

Alternatively, you can also use other available partial evaluators developed for Logic Programs (e.g., the ECCE system or MIXTUS) to generate the residual programs and existing analyzers for LP to analyze them later (e.g., the BU tools or the Polymorphic type inference tool ).

Some Examples

The following examples have been generated using the Class_Reader, the JVMLr Interpreter and the CiaoPP system, as explained above.
Java Bytecode JVMLr Program Method Invocation Specification (MIS) Residual Program Java Source
.class File Generated with "javap -v" emb embpt abstractembpt+gen
.class .txt .pl int Exp.exp(int _,int _) .pl .pl .pl .java
.class .txt .pl int Gcd.gcd(int _,int _) .pl .pl .pl .java
.class .txt .pl int Lcm.lcm(int _,int _) .pl .pl .pl .java
.class .txt .pl int Combinatory.combNoRep(int _,int _) .pl .pl .pl .java
.class .txt .pl int Combinatory.combRep(int _,int _) .pl .pl .pl .java
.class .txt .pl int Combinatory.perm(int _) .pl .pl .pl .java
.class .txt .pl int Fib.fib(int _) - .pl .pl .java
.class .txt .pl int LinearSearch.search(int[] _,int _) - .pl .pl .java
.class .txt .pl int BinarySearch.search(int[] _,int _) .pl .pl .pl .java
.class .txt .pl int Signs.signs(int[] _) - .pl .pl .java
.class .txt .pl Rational Rational.exp(int _) .pl .pl .pl .java
.class .txt .pl Rational Rational.simplify() .pl .pl .pl .java
.class .txt .pl Rational Rational.add(Rational _,Rational _) .pl .pl .pl .java
.class .txt .pl Date Date.forward() .pl .pl .pl .java


[AGHP-PADL07]: E. Albert, M. Gomez-Zamalloa, L. Hubert and G. Puebla. Verification of Java Bytecode using Transformation and Analysis Tools for Logic Programming. Ninth International Symposium on Practical Aspects of Declarative Languages (PADL 07), Nice, France January 14-15, 2007. PDF

[AGP-BC07]: M. Gomez-Zamalloa, E. Albert and G. Puebla. Effective and Efficient Decompilation of Java Bytecode to Prolog by Partial Evaluation. Submitted to Second Workshop on Bytecode Semantics, Verification, Analysis and Transformation (Bytecode 07), Braga, Portugal March 31, 2007. PDF


The approach has been proposed and implemented by Elvira Albert, Miguel Gomez-Zamalloa, Laurent Hubert and German Puebla.

Please report any bug or comment to mzamalloa@clip.dia.fi.upm.es.

Last update December 2006 #