2008
Abstract. Using the theorem prover Isabelle/HOL we have formalized and proved correct an executable bytecode verifier in the style of Kildall's algorithm for a significant subset of the Java Virtual Machine. First an abstract framework for proving correctness of data flow based type inference algorithms for assembly languages is formalized. It is shown that under certain conditions Kildall's algorithm yields a correct bytecode verifier. Then the framework is instantiated with a model of the JVM. 1 Introduction Over the past few years there has been considerable interest in formal models for Java and the JVM, and in particular its bytecode verifier (BCV). So far most of the work has concentrated on abstract models of particularly tricky aspects of the JVM, in particular the idiosyncratic notion of "subroutines". This paper complements those studies by focussing on machine-checked proofs of executable models. Its distinctive features are:- The first machine-checked proof of correctness of a BCV implementation for
Cited by 0
Lubomír Bulej, Yudi Zheng, Walter Binder · 2016
Many dynamic program analysis (DPA) tools for profiling, debugging, and monitoring programs executing on managed platforms such as the Java Virtual Machine (JVM) rely on bytecode instrumentation (sometimes combined with agents utilizing the JVM Tool Interface and native code libraries) to observe the base program behavior. While this is both the recommended and preferred technique for implementing DPA tools, it has certain noticeable drawbacks [1].
Cited by 0
Christian Gram Kalhauge, Jens Palsberg · 2021
Reducing a failure-inducing input to a smaller one is challenging for input with internal dependencies because most sub-inputs are invalid. Kalhauge and Palsberg made progress on this problem by mapping the task to a reduction problem for dependency graphs that avoids invalid inputs entirely. Their tool J-Reduce efficiently reduces Java bytecode to 24 percent of its original size, which made it the most effective tool until now. However, the output from their tool is often too large to be helpful in a bug report. In this paper, we show that more fine-grained modeling of dependencies leads to much more reduction. Specifically, we use propositional logic for specifying dependencies and we show how this works for Java bytecode. Once we have a propositional formula that specifies all valid sub-inputs, we run an algorithm that finds a small, valid, failure-inducing input. Our algorithm interleaves runs of the buggy program and calls to a procedure that finds a minimal satisfying assignment. Our experiments show that we can reduce Java bytecode to 4.6 percent of its original size, which is 5.3 times better than the 24.3 percent achieved by J-Reduce. The much smaller output is more suitable for bug reports.
Cited by 15Open access
Gerwin Klein, Martin Wildmoser · 2003
Bytecode subroutines are a major complication for Java bytecode verification: they are difficult to fit into the data flow analysis that the JVM specification suggests. Because of that, subroutines are left out or are restricted in most formalizations of the bytecode verifier. We examine the problems that occur with subroutines and give an overview of the most prominent solutions in the literature. Using the theorem prover Isabelle/HOL, we have extended our substantial formalization of the JVM and the bytecode verifier with its proof of correctness by the most general solution for bytecode subroutines.
Cited by 0
Lennart C.L. Kats, Martin Bravenboer, Eelco Visser · ACM SIGPLAN Notices · 2008
Language extensions increase programmer productivity by providing concise, often domain-specific syntax, and support for static verification of correctness, security, and style constraints. Language extensions can often be realized through translation to the base language, supported by preprocessors and extensible compilers. However, various kinds of extensions require further adaptation of a base compiler's internal stages and components, for example to support separate compilation or to make use of low-level primitives of the platform (e.g., jump instructions or unbalanced synchronization). To allow for a more loosely coupled approach, we propose an open compiler model based on normalization steps from a high-level language to a subset of it, the core language. We developed such a compiler for a mixed Java and (core) bytecode language, and evaluate its effectiveness for composition mechanisms such as traits, as well as statement-level and expression-level language extensions.
Cited by 6
Émilie Balland, Pierre‐Etienne Moreau, Antoine Reilles · Electronic Notes in Theoretical Computer Science · 2007
In this paper, we present a term rewriting based library for manipulating Java bytecode. We define a mapping from bytecode programs to algebraic terms, and we use Tom, an extension of Java that adds pattern-matching facilities, to describe transformations. An originality of Tom is that it provides a powerful strategy language to express traversals over trees and to control how transformation rules are applied. To be even more expressive, we use CTL formulae as conditions and we show how their satisfiability can be ensured using the strategy formalism. Through small examples, we show how bytecode analysis and transformations can be defined in an elegant way. In particular, we outline the implementation of a ClassLoader parameterized by a security policy that restricts file access.
Cited by 9Open access
Krýsl, Miroslav · Digital Library (University of West Bohemia)
Tato bakalářská práce se zabývá návrhem a implementací vizuálního intrepreteru pro podmnožinu bajtkódu Javy. V prvních částech je popsána specifikace virtuálního stroje Javy - JVM a také existující emulátory nejen pro Javu. V dalších částech práce je návrh vizuálního interpreteru, stručný popis jeho implementace a výsledky uživatelského testování.
Cited by 0Open access
Parker Abercrombie, Murat Karaorman · 2002
Design by Contract is a software engineering practice that allows semantic information to be added to a class or interface to precisely specify the conditions that are required for its correct operation. The basic constructs of Design by Contract are method preconditions and postconditions, and class invariants. This paper presents
Cited by 0
David Basin, Stefan Friedrich, Marek Gawkowski · 2002
We have used Isabelle/HOL to formalize and prove correct an approach to bytecode verification based on model checking that we have developed for the Java Virtual Machine. Our work builds on, and extends, the formalization of the Java Virtual Machine and data flow analysis framework of Pusch and Nipkow. By building on their framework, we can reuse their results that relate the run-time behavior of programs with the existence of well-typings for the programs.
Cited by 0
Technische Universität München, Technische Universität München, Gerwin Klein et al. · 2003
Kurzfassung Der Bytecode Verifier ist ein essentieller Bestandteil der Sicherheitsarchiktektur der Programmierplattform Java. Die Dissertation präsentiert eine formale, ausführbare Spezifikation des Bytecode Verifiers sowie den Beweis, dass dieser korrekt ist. Die Formalisierung im Theorembeweiser Isabelle besteht aus einem abstrakten Framework für Bytecode-Verifikation, das mit zunehmend ausdrucksstarken Typsystemen instantiiert wird. Diese decken sämtliche interessanten Eigenschaften der Java-Plattform ab: Klassen,
Cited by 0
Han Bok Lee, Han Bok Lee, Benjamin Zorn et al. · 1997
this paper, a customized tool that could aid in branch prediction is presented as in (Srivastava and Eustace, 1994). This tool counts the number of branches taken and not taken at all the branches in different methods. Figure 3 shows the instrumentation code for this tool. BIT's methods are shown in bold. This instrumentation code specifies where the user program is to be instrumented and what methods are to be invoked. This tool takes two arguments: an input file and an output file. The input class file is opened and broken down into more manageable pieces (class, routine, basic block, and instruction), which are then instrumented. In this instrumentation program, we first analyze the input file by creating a new ClassInfo object, whose constructor parses the input file and stores the intermediate representation in its members. A call to the getRoutines() method is invoked to obtain the vector of Routines. A Routine represents a method in the input class file. For each of these Routines, we obtain the basic blocks by invoking the getBasicBlocks() method. To count all the conditional branches in a program, we need to insert analysis code wherever there exists a conditional instruction in the program. This is accomplished by looking at each basic block and seeing whether the last instruction in that basic block is a conditional instruction or not. 13
Cited by 6
Michael Orlov, Michael Orlov, Michael Orlov et al. · 2010
“While it is common to describe GP as evolving programs, GP is not typically used to evolve programs in the familiar Turing-complete languages humans normally use for software development. It is instead more common to evolve programs (or expressions or formulae) in a more constrained and often domain-specific language.” Flight of the Finch through
Cited by 0
Kurzmann, Martin · reposiTUm (TU Wien) · 2020
Im Zeitalter der Kryptowährungen gewinnt die zugrunde liegende Blockchain-Technologie an Relevanz. Während die erste Kryptowährung Bitcoin eine Plattform mit eingeschränkten Funktionen für Programme auf ihrer Blockchain ist, konzentrieren sich einige der Nachfolger ausdrücklich auf blockchainbasierte Programme, die häufig als Smart Contracts bezeichnet werden. Ein etabliertes Beispiel ist die Plattform Ethereum, die nicht nur eine eigene Kryptowährung bereitstellt, sondern mithilfe ihrer universellen virtuellen Maschine (EVM) auch die Entwicklung verschiedener blockchainbasierter Anwendungen ermöglicht. Die EVM ist eine quasi Turing-vollständige, stackbasierte Maschine, die den Bytecode der Smart Contracts auf Ethereum ausführt. Smart Contracts werden jedoch üblicherweise in der Hochsprache Solidity implementiert und zu EVM-Bytecode kompiliert, bevor sie in der Ethereum-Blockchain bereitgestellt werden. Smart Contracts werden häufig für Anwendungen eingesetzt, die mit Vermögenswerten umgehen und bei Fehlern Geldverluste verursachen können. Daher ist die Prüfung des EVM-Bytecodes von Smart Contracts ein wertvolles Mittel zur Analyse. Dieser Bytecode ist jedoch für Menschen schwer zu lesen. Obwohl viele Anwendungen in Solidity entwickelt wurden, ist der Code dieser Applikationen häufig erst nach der Kompilierung als EVM-Bytecode verfügbar. Daher ist eine Dekompilierung erforderlich, die den Bytecode zurück in eine höhere Programmiersprache übersetzt, um ihn besser lesbar zu machen. Da hinsichtlich der Dekompilierung des EVM-Bytecodes noch Forschungsbedarf besteht, soll in dieser Arbeit untersucht werden, inwieweit dieses Problem gelöst werden kann. Wir untersuchen vorhandene Tools und Methoden zum Dekompilieren von Smart Contracts. Darüber hinaus untersuchen wir die Struktur des EVM-Bytecodes. Basierend auf diesen Ergebnissen entwickeln wir den Prototyp Soldec, der den Open-Source-Decompiler Erays erweitert und verbessert. Schließlich evaluieren wir den Prototyp hinsichtlich seiner Fähigkeit, Solidity-ähnlichen Code zu rekonstruieren.
Cited by 0Open access
Forissier, Titouan · KTH Publication Database DiVA (KTH Royal Institute of Technology) · 2024
With the increasing popularity of blockchain technology and smart contracts, the need for secure and private code has become more important than ever. Ethereum, being one of the most widely used blockchain platforms, is no exception. However, the Ethereum Virtual Machine (EVM) bytecode of smart contracts is publicly accessible, making it vulnerable to reverse engineering and exploitation by malicious actors. Obfuscation, which is used to make code harder to understand and reverse engineer, is a potential solution to this problem. This thesis explores the development of obfuscation techniques specifically tailored for EVM bytecode. The research begins by analyzing the complexities involved in smart contract deployment and execution within the EVM, providing a solid foundation for the development of obfuscation methods. The work then presents a range of obfuscation techniques, from established methods to novel approaches designed specifically for the EVM. The primary contribution of this thesis is the design and development of an obfuscator tool for EVM bytecode, aimed at enhancing the security of smart contracts against reverse engineering. The tool is evaluated based on its effectiveness in obfuscating the code while maintaining functionality and gas cost efficiency. The challenge lies in striking a balance between these two factors. In summary, this thesis addresses the significant problem of protecting EVM bytecode from reverse engineering and exploitation by malicious actors. By developing obfuscation techniques and tools tailored for the EVM, the work provides a valuable contribution to the field of smart contract security. The research also highlights the importance of considering both functionality and gas cost efficiency when designing obfuscation techniques for the EVM.
Cited by 0Open access
James Hamilton · 2011
Cited by 0
Javier Cabrera Arteaga, Shrinish Donde, Jian Gu et al. · arXiv (Cornell University) · 2020
Motivated by the fast adoption of WebAssembly, we propose the first functional pipeline to support the superoptimization of WebAssembly bytecode. Our pipeline works over LLVM and Souper. We evaluate our superoptimization pipeline with 12 programs from the Rosetta code project. Our pipeline improves the code section size of 8 out of 12 programs. We discuss the challenges faced in superoptimization of WebAssembly with two case studies.
Cited by 9Open access
Poncová, Vendula · Brno University of Technology Digital Library (Brno University of Technology) · 2016
Tato práce se zabývá optimalizací bajtkódu jazyka Java zhlediska jeho velikosti. Popisuje virtuální stroj Javy a formát jeho instrukčního souboru a uvádí přehled některých knihoven pro manipulaci sbajtkódem. Spomocí těchto knihoven byla provedena analýza vybraného vzorku dat a nalezeny sekvence instrukcí, které by bylo možné optimalizovat. Na základě výsledků analýzy byly navrhnuty a implementovány metody pro optimalizaci velikosti bajtkódu. Velikost bajtkódu zkoumaného vzorku dat se po aplikaci metod snížila o zhruba 25%.
Cited by 0
Gerwin Klein, Tobias Nipkow · Concurrency and Computation Practice and Experience · 2001
Abstract Eva and Kristoffer Rose proposed a (sparse) annotation of Java Virtual Machine code with types to enable a one‐pass verification of well‐typedness. We have formalized a variant of their proposal in the theorem prover Isabelle/HOL and proved soundness and completeness. Copyright © 2001 John Wiley & Sons, Ltd.
Cited by 36
Delphine Demange, Thomas Jensen, David Pichardie et al. · 2010
Cited by 0
Batchelder, Michael Robert · 2007
Programs written for machine execution will always be susceptible to information theft. This information can include trademarked algorithms, data embedded in the program, or even data the program accesses. As technology advances computer scientists are building more and more powerful tools for reverse-engineering such as decompilers.The Java programming language is particularly open to reverse-engineering attacks because of its well-defined, open, and portable binary format. We examine one area of better-securing the intellectual property of a Java program; obfuscation. Obfuscation of a program involves transforming the code of the program into a more complex, but semantically equivalent representation. This can include the addition of confusing control flow, the removal of certain information embedded in the program which is not explicitly required for execution, or the cloaking of data.Obfuscation is one of the only techniques available other than cryptological options. While many approaches to obfuscation are ultimately reversible, it nevertheless seriously hinders those attempting to steal information by increasing the computing time and power required by software to reverse-engineer the program and also severely increases the complexity of any source code that is recovered by the reverse-engineering.In this thesis we present a number of obfuscating transformations implemented within a new automatic tool we name the Java Bytecode Obfuscator (JBCO). We present empirical measures of the performance costs of these transformations in terms of execution speed and program size. Complexity measurements that gauge the effectiveness of the obfuscations are also given. Finally, we review the feasibility of each transformation by looking at source code generated from obfuscated bytecode by various decompilers.
Cited by 1