Tomáš Šafařík · Digital Repository (National Repository of Grey Literature) · 2016
Both J2BP and PANDA tools verify compiled Java programs. By now, these tools are not able to process some programs with specific JVM bytecode instruction sequences in the correct way. We described these instruction sequences and proposed their transformations. We developed the new application, called BytecodeTransformer, based on these propositions. This application transforms compiled Java programs and replaces the problematic instruction sequences with some others. Usage of BytecodeTransformer enlarges the set of programs that can be verified by both J2BP and PANDA. We also evaluated BytecodeTransformer on several Java programs, including own tests and well-known open-source programs. These tests demonstrated the correct functionality of BytecodeTransformer. Powered by TCPDF (www.tcpdf.org)
Cited by 0
James Hamilton, Sebastian Danicic · 2009
Decompilation of Java bytecode is the act of transforming Java bytecode to Java source code. Although easier than that of decompilation of machine code, problems still arise in Java bytecode decompilation. These include type inference of local variables and exception-handling. Since the last such evaluation (2003) several new commercial, free and open-source Java decompilers have appeared and some of the older ones have been updated. In this paper, we evaluate the currently available Java bytecode decompilers using an extension of the criteria that were used in the original study. Although there has been a slight improvement since this study, it was found that none passed all the tests, each of which were designed to target different problem areas. We give reasons for this lack of success and suggest methods by which future Java bytecode decompilers could be improved.
Cited by 25
Lucas C. Cordeiro, Daniel Kroening, Peter Schrammel · Lecture notes in computer science · 2019
Cited by 21Open access
Antoniu, Gabriel, Namyst, Raymond, Bouge, Luc et al. · OpenGrey (Institut de l'Information Scientifique et Technique) · 2000
Cited by 0
Mangala Gowri Nanda, S. Arunkumar · 2016
Java bytecode obfuscates the original structure of a Java expression in the source code. So a simple expression such as (c1 || c2) or (c1 && c2) may be captured in the bytecode in 4 different ways (as shown in the paper). And correspondingly, when we reconvert the bytecode back into Java source code, there are four different ways this may happen. Further, although gotos are not permitted in the Java source code, the bytecode is full of gotos. If you were to blindly convert the bytecode into Java source code, then you would replace a goto by a labeled break. A labeled break has the advantage that it only allows you to break out of a block structure and (unlike a setjump) does not permit you to jump arbitrarily into a block structure. So while the data structures used in the regenerated Java source code are still relatively "clean" arbitrary usage of labeled breaks makes for unreadable code (as we show in the paper). And this can be a point of concern, since decompilation is generally related to debugging code.
Cited by 1
Schott, Stefan, Ponta, Serena Elisa, Fischer, Wolfram et al. · DROPS (Schloss Dagstuhl – Leibniz Center for Informatics) · 2024
Analyzing the similarity of two code fragments has many applications, including code clone, vulnerability and plagiarism detection. Most existing approaches for similarity analysis work on source code. However, in scenarios like plagiarism detection, copyright violation detection or Software Bill of Materials creation source code is often not available and thus similarity analysis has to be performed on binary formats. Java bytecode is a binary format executable by the Java Virtual Machine and obtained from the compilation of Java source code. Performing similarity detection on bytecode is challenging because different compilers can compile the same source code to syntactically vastly different bytecode. In this work we assess to what extent one can nonetheless enable similarity detection by bytecode normalization, a procedure to transform Java bytecode into a representation that is identical for the same original source code, irrespective of the Java compiler and Java version used during compilation. Our manual study revealed 16 classes of compilation differences that various compilation environments may induce. Based on these findings, we implemented bytecode normalization in a tool jNorm. It uses Jimple as intermediate representation, applies common code optimizations and transforms all classes of compilation difference to a normalized form, thus achieving a representation of the bytecode that is identical despite different compilation environments. Our evaluation, performed on more than 300 popular Java projects, shows that solely the act of incrementing a compiler version may cause differences in 46% of all resulting bytecode files. By applying bytecode normalization, one can remove more than 99% of these differences, thus acting as a crucial enabler for subsequent applications of bytecode similarity analysis.
Cited by 2Open access
Shengyi Wang, Zongyan Qiu, Shengchao Qin et al. · Teesside University Research Portal (Teesside University) · 2010
Ubiquitous embedded systems are often resource-constrained. Developing software for these systems should take into account resources such as memory space. In this paper, we develop and implement an analysis framework to infer statically stack usage bounds for assembly-level programs in abstract Java Byte code. Our stack bound inference process, extended from a theoretical framework proposed earlier by some of the authors, is composed of deductive inference rules in multiple passes. Based on these rules, a usable tool has been developed for processing programs to capture the stack memory needs of each procedure in terms of the symbolic values of its parameters. The final result contains path-sensitive information to achieve better precision. The tool invokes a Presburger solver to perform fixed point analysis for loops and recursive procedures. Our initial experiments have confirmed the viability and power of the approach.
Cited by 3Open access
Jens Dietrich, Tim White, Mohammad Mahdi Abdollahpour et al. · Zenodo (CERN European Organization for Nuclear Research) · 2023
Novel approaches to improve software supply chain security hinge on the notion of binary equivalence. A naive notion based on bitwise equivalence is not suitable for this purpose, and a perfect solution is not possible due to the undecidability of functional equivalence. Pragmatic solutions rely on comprehensive datasets for the evaluation and/or training of classifiers. We present such a dataset for Java bytecode, consisting of several oracles for both equivalence and non-equivalence, extracted from software repositories and existing security databases. The dataset contains 277,727 pairs of equivalent (but different) and 169,651 pairs of non-equivalent (but similar) compiled classes extracted from real-world programs.
Cited by 0Open access
Schrammel, Peter · Zenodo (CERN European Organization for Nuclear Research) · 2025
JBMC is a bounded model checking tool for verifying Java bytecode. It is built on top of the CPROVER framework. JBMC processes Java bytecode together with a model of the standard Java libraries. It checks a set of desired properties, such as assertions and absence of uncaught exceptions, under given bounds on loops, recursion and data structures. Internally, it uses the same bounded model checking engine as its sibling tool CBMC and discharges the generated verification conditions with the help of MiniSAT 2.2.1.
Cited by 0Open access
Gabriel Antoniu, Luc Bougé, Philip J. Hatcher et al. · Lecture notes in computer science · 2000
Cited by 17Open access
Elvira Albert, Puri Arenas, Samir Genaim et al. · Electronic Notes in Theoretical Computer Science · 2007
Recently, we proposed a general framework for the cost analysis of Java bytecode which can be used for measuring resource usage. This analysis generates, at compile-time, cost relations which define the cost of programs as a function of their input data size. The purpose of this paper is to assess the practicality of such cost analysis by experimentally evaluating a prototype analyzer implemented in Ciao. With this aim, we approximate the computational complexity of a set of selected benchmarks, including both well-known algorithms which have been used to evaluate existing cost analyzers in other programming paradigms, and other benchmarks which illustrate object-oriented features. In our evaluation, we first study whether the generated cost relations can be automatically solved. Our experiments show that in some cases the inferred cost relations can be automatically solved by using the Mathematica system, whereas, in other cases, some prior manipulation is required for the equations to be solvable. Moreover, we experimentally evaluated the running time of the different phases of the analysis process. Overall, we believe our experiments show that the efficiency of our cost analysis is acceptable, and that the obtained cost relations are useful in practice since, at least in our experiments, it is possible to get a closed form solution.
Cited by 11Open access
Zhenyu Qian · ACM Transactions on Programming Languages and Systems · 2000
Java bytecode verification forms the basis for Java-based Internet security and needs a rigorous description. One important aspect of bytecode verification is to check if a Java Virtual Machine (JVM) program is statically well-typed. So far, several formal specifications have been proposed to define what the static well-typedness means. This paper takes a step further and presents a chaotic fixpoint iteration, which represents a family of fixpoint computation strategies to compute a least type for each JVM program within a finite number of iteration steps. Since a transfer function in the iteration is not monotone, we choose to follow the example of a nonstandard fixpoint theorem, which requires that all transfer functions are increasing, and monotone in case the bigger element is already a fixpoint. The resulting least type is the artificial top element if and only if he JVM program is not statically well-typed. The iteration is standard and close to Sun's informal specification and most commercial bytecode verifiers.
Cited by 41Open access
Iu, Christopher Ming-Yee, Zwaenepoel, Willy · Infoscience (Ecole Polytechnique Fédérale de Lausanne) · 2006
When interfacing Java with other systems such as databases, programmers must often program in special interface languages like SQL. Code written in these languages often needs to be embedded in strings where they cannot be error-checked at compile-time, or the Java compiler needs to be altered to directly recognize code written in these languages. We have taken a different approach to adding database query facilities to Java. Bytecode rewriting allows us to add query facilities to Java whose correctness can be checked at compile-time but which don't require any changes to the Java language, Java compilers, Java VMs, or IDEs. Like traditional object-relational mapping tools, we provide Java libraries for accessing individual database entries as objects and navigating among them. To express a query though, a programmer simply writes code that takes a Collection representing the entire contents of a database, iterates over each entry like they would with a normal Collection, and choose the entries of interest. The query is fully valid Java code that, if executed, will read through an entire database and copy entries into Java objects where they will be inspected. Executing queries in this way is obviously inefficient, but we have a special bytecode rewriting tool that can decompile Java class files, identify queries in the bytecode, and rewrite the code to use SQL instead. The rewritten bytecode can then be run using any standard Java VM. Since queries use standard Java set manipulation syntax, Java programmers do not need to learn any new syntax. Our system is able to handle complex queries that make use of all the basic relational operations and exhibits performance comparable to that of hand-written SQL.
Cited by 0Open access
Cole Normale Suprieure De Lyon, Cole Normale Suprieure De, Gabriel Antoniu et al. · 2000
Our work combines Java compilation to native code with a run-time library that executes Java threads in a distributed-memory environment. This allows a Java programmer to view a cluster of processors as executing a single Java virtual machine. The system we present is available on top of several UNIX systems and can use a large variety of network protocols thanks to the high portability of the run-time system. To evaluate our approach, we compare serial C, serial Java, and multithreaded Java implementations of a branch-and-bound solution to the minimal-cost map-coloring problem. All measurements have been carried out on three platforms using different network protocols: SISCI/SCI, BIP/Myrinet and TCP/Myrinet.
Cited by 0
Fausto Spoto · 2004
Flow sensitive static analyses are often more precise than their flow insensitive counterparts, but much more expensive. To cope with this problem, we defined, some years ago, a watchpoint semantics as an abstract interpretation of a trace semantics. It is not itself a trace semantics, but it lets us specify flow and control sensitive analyses which are focused on a given set of program points only, called watchpoints. This means that
Cited by 0
Aymerick Savary · theses.fr (ABES) · 2016
La vérification de la résistance aux attaques des implémentations embarquées des vérifieurs de code intermédiaire Java Card est une tâche complexe. Les méthodes actuelles n'étant pas suffisamment efficaces, seule la génération de tests manuelle est possible. Pour automatiser ce processus, nous proposons une méthode appelée VTG (Vulnerability Test Generation, génération de tests de vulnérabilité). En se basant sur une représentation formelle des comportements fonctionnels du système sous test, un ensemble de tests d'intrusions est généré. Cette méthode s'inspire des techniques de mutation et de test à base de modèle. Dans un premier temps, le modèle est muté selon des règles que nous avons définies afin de représenter les potentielles attaques. Les tests sont ensuite extraits à partir des modèles mutants. Deux modèles Event-B ont été proposés. Le premier représente les contraintes structurelles des fichiers d'application Java Card. Le VTG permet en quelques secondes de générer des centaines de tests abstraits. Le second modèle est composé de 66 événements permettant de représenter 61 instructions Java Card. La mutation est effectuée en quelques secondes. L'extraction des tests permet de générer 223 tests en 45 min. Chaque test permet de vérifier une précondition ou une combinaison de préconditions d'une instruction. Cette méthode nous a permis de tester différents mécanismes d'implémentations de vérifieur de code intermédiaire Java Card. Bien que développée pour notre cas d'étude, la méthode proposée est générique et a été appliquée à d'autres cas d'études.
Cited by 0Open access
Joloboff, Vania, de Ferriere, Francois, Fabre, Christian et al. · HAL (Le Centre pour la Communication Scientifique Directe) · 1998
Cited by 0
Claire Quigley, Claire Louise Quigley · OpenGrey (Institut de l'Information Scientifique et Technique) · 2003
A copy can be downloaded for personal non-commercial research or study, without prior permission or charge This thesis cannot be reproduced or quoted extensively from without first obtaining permission in writing from the Author The content must not be changed in any way or sold commercially in any format or medium without the formal permission of the Author When referring to this work, full bibliographic details including the author, title, awarding institution and date of the thesis must be given
Cited by 0
Michael Orlov, Moshe Sipper · Genetic and evolutionary computation · 2010
Cited by 9
Gary Meehan, Mike Joy · Software Practice and Experience · 1999
The Java Virtual Machine (JVM) was designed as the target for Java compilers, but there is no reason why it cannot be used as the target for other languages. We describe the implementation of a compiler which translates a lazy, weakly-typed functional program into Java class files. We compare the performance of our compiler to the only other known compiler from a lazy functional language to the JVM. The results are broadly similar, suggesting that to get a significant performance speed-up using this compilation paradigm will come only from increasing the performance of the JVM, rather than enhancing the compiler itself. Copyright © 1999 John Wiley & Sons, Ltd.
Cited by 4