Richard L. Apodaca · Front Matter · 2006
In the ideal world for many Java developers, all software would be written in Java. The reality is that a great deal of software is written in other languages, one of the most widespread of which is C. This article discusses a unique approach to working with C code from Java, producing 100% pure Java bytecode that runs anywhere Java does.
Cited by 0Open access
Jonathan Bell · Columbia Academic Commons (Columbia University) · 2015
A lot of my research has involved Java bytecode instrumentation with ASM and more recently, also JVMTI development. For instance, with VMVM, we instrumented bytecode to enable efficient java class reinitialization. With Phosphor, we instrumented bytecode to track metadata with every single variable, enabling performant and portable dynamic taint tracking. In ElectricTest, we combined bytecode instrumentation with JVMTI to efficiently detect data dependencies between test cases running within the same JVM. As I built each of these projects, I leaned heavily on code snippets that I found across the internet – while I had done a lot of Java development before starting these projects, I’d done nothing with bytecode instrumentation. I found it particularly difficult to find examples of how to use JVMTI (aside from the basic man-pages, and a few excellent blog posts by Kelly O’Hair). This archive consists of a number of examples on JVMTI and byte code rewriting.
Cited by 0Open access
Peter Bertelsen · Future Generation Computer Systems · 2000
Cited by 17
Gabriel Bizzotto, Gilles Grimaud · 2002
Our work concerns bytecode compression on an embedded, tiny and safe environment, and more specifically JAVA CARDS. [2] and [4] propose a way to compress java card bytecode into a format executable in an ultra light embedded system, using macro-packing. Our implementation, improved with new specifical algorithms, allows a better compress rate (up to 32%). In a smart card having 32kB EEPROM, up to 10kB can be freed, it is enough to store some applets. The execution of macro-packed programs is very simple and the code overhead in the operating system and in the virtual machine is very small. Unfortunately, the compression process is not feasible in a tiny embedded system. We propose a distribution of the compression process called Compression-Carrying Code or simply CCC. This distribution maintains the Java Card 2.11 compatibility [11], and allows a trusted, just-in-time compression by the embedded bytecode loader.
Cited by 0
Ramos Horta, Rubén · RECERCAT (Consorci de Serveis Universitaris de Catalunya) · 2016
This dissertation focuses on runtime optimization of Java programs, based on the application of code optimizations.The concept is based on runtime generation of bytecode using code templates.This work proposes an approach for developing these templates and studies their impact in different platforms
Cited by 0Open access
Mark C. Reynolds · Science of Computer Programming · 2011
Cited by 2
Mark P. Jones · 1998
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. This paper describes 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 prope...
Cited by 0
Aleksy Schubert, Krzysztof Jakubczyk, Jędrzej Fulara · 2008
The proof-carrying code (PCC) techniques allow the executable code to be augmented with a proof that the code obeys certain policies (e.g. the program does not store passwords in clear in a le). BML (Bytecode Modelling Language) can be regarded as a part of the PCC architecture which allows to express detailed properties of Java bytecode programs. As most of the programming is done at the source code level, it is desirable to have a way to translate properties expressed at the source code level (in our case written in Java Modeling Language, JML) to the bytecode level. In this paper we present a JML2BML compiler, a tool that for a given Java source le annotated with speci cations generates class les with BML.
Cited by 0
Diarmuid O'Donoghue, Aine Leddy, James Power et al. · 2002
Introduction Much research has been conducted in the analysis of Java bytecodes in order to gain a better understanding of how Java programs behave. One branch of this research has focused on analysing bytecode usage within the Java Virtual Machine (JVM), with particular emphasis on analysing bytecodes associated with various benchmark programs. Previous research has focused on the frequencies of the individual bytecodes at the static class-file level [2]. Another branch examines dynamic bytecodes, as executed by the JVM itself at run-time [4, 6]. This project follows on from previous dynamic bytecode analysis, analysing streams of Java bytecodes produced at the platform independent level. It di#ers from previous projects, in that it is not concentrating on the occurrences of the individual bytecodes, but in the occurrences of bigrams, or bytecode pairs. We report on a project that performed a bigram analysis of dynamic bytecode sequences. The objective was to identify the most comm
Cited by 0
Jianjun Zhao · 1999
Understanding control \nows in a computer program is essential for many software engineering tasks such as testing, debugging, reverse engineering, and mainte-nance. In this paper, we present a control \now anal-ysis technique to analyze the control \now in Java byte-code. To perform the analysis, we construct a control ow graph (CFG) for Java bytecode not only at the in-traprocedural level but also at the interprocedural level. We also discuss some applications of a CFG in a main-tenance environment for Java bytecode. some primary experimental results.
Cited by 0
Jens Dietrich, Behnaz Hassanshahi · ArXiv.org · 2025
The security of software builds has attracted increased attention in recent years in response to incidents like solarwinds and xz. Now, several companies including Oracle and Google rebuild open source projects in a secure environment and publish the resulting binaries through dedicated repositories. This practice enables direct comparison between these rebuilt binaries and the original ones produced by developers and published in repositories such as Maven Central. These binaries are often not bitwise identical; however, in most cases, the differences can be attributed to variations in the build environment, and the binaries can still be considered equivalent. Establishing such equivalence, however, is a labor-intensive and error-prone process. While there are some tools that can be used for this purpose, they all fall short of providing provenance, i.e. readable explanation of why two binaries are equivalent, or not. To address this issue, we present daleq, a tool that disassembles Java byte code into a relational database, and can normalise this database by applying datalog rules. Those databases can then be used to infer equivalence between two classes. Notably, equivalence statements are accompanied with datalog proofs recording the normalisation process. We demonstrate the impact of daleq in an industrial context through a large-scale evaluation involving 2,714 pairs of jars, comprising 265,690 class pairs. In this evaluation, daleq is compared to two existing bytecode transformation tools. Our findings reveal a significant reduction in the manual effort required to assess non-bitwise equivalent artifacts, which would otherwise demand intensive human inspection. Furthermore, the results show that daleq outperforms existing tools by identifying more artifacts rebuilt from the same code as equivalent, even when no behavioral differences are present.
Cited by 0Open access
Krzysztof Jakubczyk, Aleksy Schubert · 2008
Abstract. The proof-carrying code (PCC) techniques allow the exe-cutable code to be augmented with a proof that the code obeys certain policies (e.g. the program does not store passwords in clear in a file). BML (Bytecode Modelling Language) can be regarded as a part of the PCC architecture which allows to express detailed properties of Java bytecode programs. As most of the programming is done at the source code level, it is desirable to have a way to translate properties expressed at the source code level (in our case written in Java Modeling Language, JML) to the bytecode level. In this paper we present a JML2BML com-piler, a tool that for a given Java source file annotated with specifications generates class files with BML. 1
Cited by 0
Jianjun Zhao Department, Jianjun Zhao · 1999
Understanding control flows in a computer program is essential for many software engineering tasks such as testing, debugging, reverse engineering, and maintenance. In this paper, we present a control flow analysis technique to analyze the control flow in Java bytecode. To perform the analysis, we construct a control flow graph (CFG) for Java bytecode not only at the intraprocedural level but also at the interprocedural level. We also discuss some applications of a CFG in a maintenance environment for Java bytecode. some primary experimental results. Keywords Control flow analysis, Java virtual machine, software testing, software maintenance. 1 Introduction Many compiler optimizations and program analysis techniques rely on control flow information, which is topically represented by a control flow graph (CFG) [4]. The CFG, although originally proposed for compiler optimizations, has been used for various software engineering tasks such as program slicing, debugging, testing, mainte...
Cited by 0
Cinzia Bernardeschi Luca, Key Words · 2004
Java applets run on a Virtual Machine that checks code's integrity and correctness before execution using a module called Bytecode Verifier. Java Card technology allows Java applets to run on smart cards. Large memory space requirements of the verification process do not allow the implementation of a Bytecode Verifier embedded in the Java Card Virtual Machine. To address this feasibility problem, we propose a modified verification algorithm that optimizes the use of system memory. The algorithm, inspired to compilers ' techniques, partitions the code of the methods into control regions. In this way data structures can be dynamically allocated and the verification process can be applied locally to a subset of instructions.
Cited by 0
Rui Guo · Scholarship at UWindsor (University of Windsor) · 2001
Java security is a problem that is raised sharply with its ubiquity through Internet. Sun provides two kinds of specifications of Java bytecode verifier, which is used to ensure the soundness of a program. One is a prose specification and the other is a reference to implementation. Neither of these two way is a good approach to solve the security problems. This thesis proposes a new way to formalize Java bytecode verifier by using Z language. The formal method is usually a perfect choice to some novel, difficult and critical projects. As a model-based formal specification language, Z is a good language to model a well-structured system. Besides the well-structured way it can offer, Z can also support verification of the implementation based on its specification. This approach offers a formal basis for any operation that is crucial to security. This helps to avoid causing security holes. By giving formal description to each bytecode instruction, the verifier could check the typing correctness within a method at each step of runtime. On the other hand, a more flexible and clearer module is constructed, which is applied to the type checking system, not only for Java but also for other similar mechanism. This thesis focuses on two essential problems: subroutine and object initialization. Since this thesis gives a core model to deal with the Java bytecode verifier, it is easy to be extended to include all the instructions of Java bytecode. Paper copy at Leddy Library: Theses & Major Papers - Basement, West Bldg. / Call Number: Thesis2001 .G86. Source: Masters Abstracts International, Volume: 40-06, page: 1545. Adviser: Liwu Li. Thesis (M.Sc.)--University of Windsor (Canada), 2001.
Cited by 0Open access
Samuel Willimann · 2007
This master thesis is based on B2BPL, a translator from BML annotated Java Bytecode to BoogiePL conceived and implemented in previous work at ETH Zurich. We are primarily interested in extending the existing translator with some more elaborate mechanisms in terms of translating method invocations and invariant checks. Although B2BPL is doing fine in translating annotated Bytecode programs already, there is still room for improvement. We are also keen to see B2BPL integrated in a broader verification environment, where Java Bytecode can be directly translated to BoogiePL and verified by Boogie in an integrated development environment like Eclipse. In order to achieve these goals, we roll up the existing implementation of the method call translation algorithm and introduce a mechanism to perform simple but more flexible invariant checks (with a particular focus on method calls). The translation of method calls is improved by using the Boogie-specific call command while at the same time, exception handling is extended with an additional level of flexibility. Furthermore, invariant checks are refined such that only the invariants of modified objects need to be checked, and that inadmissible invariants are ruled out automatically. In addition to these modification in the translator itself, an Eclipse plugin is developed which is intended to integrate the translator seemlessly into the Eclipse IDE as well as the anticipated Mobius workspace, which is aimed at developers who want to have even more capabilities to verify their Java/Bytecode projects in Eclipse.
Cited by 0
Doyon, Stéphane · Library and Archives Canada (Government of Canada) · 1999
Cited by 0
César Soto-Valero, Thomas Durieux, Nicolas Harrand et al. · ACM Transactions on Software Engineering and Methodology · 2022
Software bloat is code that is packaged in an application but is actually not necessary to run the application. The presence of software bloat is an issue for security, performance, and for maintenance. In this article, we introduce a novel technique for debloating, which we call coverage-based debloating. We implement the technique for one single language: Java bytecode. We leverage a combination of state-of-the-art Java bytecode coverage tools to precisely capture what parts of a project and its dependencies are used when running with a specific workload. Then, we automatically remove the parts that are not covered, in order to generate a debloated version of the project. We succeed to debloat 211 library versions from a dataset of 94 unique open-source Java libraries. The debloated versions are syntactically correct and preserve their original behaviour according to the workload. Our results indicate that 68.3% of the libraries’ bytecode and 20.3% of their total dependencies can be removed through coverage-based debloating. For the first time in the literature on software debloating, we assess the utility of debloated libraries with respect to client applications that reuse them. We select 988 client projects that either have a direct reference to the debloated library in their source code or which test suite covers at least one class of the libraries that we debloat. Our results show that 81.5% of the clients, with at least one test that uses the library, successfully compile and pass their test suite when the original library is replaced by its debloated version.
Cited by 18Open access
Étienne Payet, Fred Mesnard, Fausto Spoto · arXiv (Cornell University) · 2014
We introduce a fully automated static analysis that takes a sequential Java bytecode program P as input and attempts to prove that there exists an infinite execution of P. The technique consists in compiling P into a constraint logic program P_CLP and in proving non-termination of P_CLP; when P consists of instructions that are exactly compiled into constraints, the non-termination of P_CLP entails that of P. Our approach can handle method calls; to the best of our knowledge, it is the first static approach for Java bytecode able to prove the existence of infinite recursions. We have implemented our technique inside the Julia analyser. We have compared the results of Julia on a set of 113 programs with those provided by AProVE and Invel, the only freely usable non-termination analysers comparable to ours that we are aware of. Only Julia could detect non-termination due to infinite recursion.
Cited by 0Open access
2008
x to a variable y, denoted by x;y, if changes in the input values of x are observable from the output valuesof
Cited by 0