Cinzia Bernardeschi, N. De Francesco, Giuseppe Lettieri et al. · Software Practice and Experience · 2004
Abstract A method is presented for checking secure information flow in Java bytecode, assuming a multilevel security policy that assigns security levels to the objects. The method exploits the type‐level abstract interpretation of standard bytecode verification to detect illegal information flows. We define an algorithm transforming the original code into another code in such a way that a typing error detected by the Verifier on the transformed code corresponds to a possible illicit information flow in the original code. We present a prototype tool that implements the method and we show an example of application. Copyright © 2004 John Wiley & Sons, Ltd.
Cited by 15
Chun-yuan Chen, Zong Qiang Chen, Wuu Yang · 2004
In order to speed up the execution of a Java program, we implemented a translation system that converts Java bytecode to X86 assembly code. The main approach of our translation system is that objects are still created and manipulated inside the (run-time) Java virtual machine. Other ordinary operations are translated into assembly code. Some pattern-based optimiza-tions are applied during the translation process in an attempt to achieve better performance.
Cited by 0
Algis Rudys, Dan S. Wallach · 2002
Abstract. Bytecode rewriting is a portable way of altering Java’s behavior by changing Java classes themselves as they are loaded. This mechanism allows us to modify the semantics of Java while making no changes to the Java virtual machine itself. While this gives us portability and power, there are numerous pitfalls, mostly stemming from the limitations imposed upon Java bytecode by the Java virtual machine. We reflect on our experience building three security systems with bytecode rewriting, presenting observations on where we succeeded and failed, as well as observing areas where future JVMs might present improved interfaces to Java bytecode rewriting systems. 1
Cited by 0
Sečkařová, Petra · Brno University of Technology Digital Library (Brno University of Technology) · 2017
Grafy toku řízení (Control Flow Graph -- CFG) slouží jako základ pro mnoho analýz vyhodnocujících kvalitu programu. Takovou analýzou je i testování založené na modelech (model-based testing), které na základě analýzy modelu kódu, např. grafu, generuje testovací případy. Aby bylo možné tuto analýzu provádět co nejobecněji, je vhodné, aby instrukce obsažené v CFG patřily do některé z obecných instrukčních sad.Tato práce se zabývá extrakcí grafů toku řízení z bajtkódu jazyka Java a následným překladem jednotlivých instrukcí bajtkódu uvnitř základních bloků do instrukční sady LLVM IR. Výsledný program dokáže spolehlivě získat grafy toku řízení z programů v jazyce Java zadaných v jakékoli z nejběžnějších forem pro šíření tohoto typu software (.jar archiv, .java nebo .class soubory). Grafy na výstupu jsou navíc koncipovány tak, aby nad nimi bylo možné provádět analýzu za účelem generování jednotkových testů.
Cited by 0
Suwimonteerabuth, Dejvuth · Fachbereich Informatik (University of Stuttgart) · 2004
Cited by 1
Antonella Santone · 2011
In this paper we present a formal method-based approach in detecting source code clones by means of analysing and comparing the Java Bytecode that is produced when the source code is compiled. A preliminary investigation has been also conducted to assess the validity of the proposed approach.
Cited by 34
John Waldron · 2003
Java is an object oriented language that has grown in popularity since its release in 1996 and is particularly interesting because it uses a byte code intermediate language to represent programs, so that the same program can be run unchanged on machines with different underlying instruction sets. To measure dynamic byte code usage it was necessary to modify the source code Kaffe, a Java Virtual Machine. A selection of programs was measured to compare the way different applets and applications use the bytecodes, and it was found that very similar patterns of usage appear in all cases. For the test suite studied most of the bytecodes were used at least once during execution. However a small subset of the bytecodes was executed with very high frequency. 40% of instructions executed either pushed local variables or constants onto the operand stack, merely telling the useful instructions which operands to use. This result questions the stack based design for the intermediate representation of Java programs, since the bytecodes only occupy on average twelve percent of a class file, an intermediate representation that is less compact, but executes more efficiently might be possible.
Cited by 8
Alessandro Coglio · Concurrency and Computation Practice and Experience · 2004
Abstract Java is normally compiled to bytecode, which is verified and then executed by the Java Virtual Machine. Bytecode produced via compilation must pass verification. The main cause of complexity for bytecode verification is subroutines, used by compilers to generate more compact code. The techniques to verify subroutines proposed in the literature reject certain programs produced by mundane compilers, are difficult to realize within an implementation of the Java Virtual Machine or are relatively complicated. This paper presents a novel technique which is very simple to understand, implement and prove sound. It is also very powerful: the set of accepted programs has a simple characterization which most likely includes all the code produced by current compilers and which enables future compilers to make more extensive use of subroutines. Copyright © 2004 John Wiley & Sons, Ltd.
Cited by 24
Austin Kim, J. Morris Chang · Lecture notes in computer science · 2000
Cited by 4
Zhenyu Qian · 1999
. (Java) bytecode verification should ensure type-safety for Java Virtual Machine (JVM) programs (bytecode) and form a basis for Java-based internet security. Recent research work has proposed using formal typing rules to enforce constraints on types for memory locations in bytecode and thus formally specify (part of) bytecode verification. In this paper, we take one step forward and show that typing rules can be non-deterministically and repeatedly used in an arbitrary order to compute the least types for memory locations satisfying the constraints, if there are any, or to report a failure, if there are none. The result implies that theoretically a bytecode verifier can have any strategy visiting program points in bytecode without affecting the acceptance of bytecode, i.e. without causing denial of services provided by bytecode. It also suggests ways to implement bytecode verification directly using formal specification. 1 Introduction Java programs are usually compiled into Java b...
Cited by 0
Gerwin Klein · 2002
Cited by 0
Florence Charreteur, Arnaud Gotlieb · HAL (Le Centre pour la Communication Scientifique Directe) · 2010
Abstract—In this paper, we introduce a constraint-based reasoning approach to automatically generate test input for Java bytecode programs. Our goal-oriented method aims at building an input state of the Java Virtual Machine (JVM) that can drive program execution towards a given location within the bytecode. An innovative aspect of the method is the definition of a constraint model for each bytecode that allows backward exploration of the bytecode program, and permits to solve complex constraints over the memory shape (e.g., p = = p.next enforces the creation of a cyclic data structure referenced by p). We implemented this constraint-based approach in a prototype tool called JAUT, that can generate input states for programs written in a subset of JVM including integers and references, dynamic-allocated structures, objects inheritance and polymorphism by virtual method call, conditional and backward jumps. Experimental results show that JAUT generate test input for executing locations not reached by other state-of-the-art code-based test input generators such as jCUTE, JTEST and Pex. I.
Cited by 0Open access
Todd B. Knoblock, et al. · 2008
Java source code is strongly typed, but the translation from Java source to bytecode omits much of the type information originally contained within methods. Type elaboration is a technique for reconstructing strongly typed programs from incompletely typed bytecode by inferring types for local variables. There are situations where, technically, there are not enough types in the original type hierarchy to type a bytecode program. Subtype completion is a technique for adding necessary types to an arbitrary type hierarchy to make type elaboration possible for all verifiable Java bytecode. Type elaboration with subtype completion has been implemented as part of the Marmot Java compiler.
Cited by 0
Nikita V. Lipsky, Vladimir Sergeyevich Solovyov · System Informatics · 2013
: Java : .. ( . .. , ), .. ( . ..
Cited by 0Open access
Takahiro Sakamoto, Tatsurou Sekiguchi, Akinori Yonezawa · Lecture notes in computer science · 2000
Cited by 89
H. McGhan, Mike O’Connor · Computer · 1998
Key to the central promise inherent in Java technology-"write once, run anywhere"-is the fact that Java programs run on the Java virtual machine, insulating them from any contact with the underlying hardware. Consequently, Java programs must execute indirectly through a translation layer built into the Java virtual machine. Translation essentially converts Java virtual machine instructions (called bytecodes) into corresponding machine-specific binary instructions. Bytecode is a single image of a program that will execute identically (in principle) on any system equipped with a JVM. The first step toward the development of a new class of Java processors was the creation of the bytecode execution engine itself, called the picoJava core. PicoJava directly executes Java bytecode instructions and provides hardware support for other essential functions of the JVM. Executing bytecode instructions in hardware eliminates the need for dynamic translation, thus extending the useful range of Java bytecode programs to embedded environments. By the end of 1998, Java processors like Sun's microJava 701 should be available for evaluation from several licensees of the picoJava core technology.
Cited by 165
Eva Rose · 1998
There is a growing interest for using "intelligent" or "smart" cards such as Sun's Java Cards, because of the independence they offer their users by having an on-card microprocessor. Furthermore we have, during the last decade, become accustomed to global, fast and flexible information exchange, as offered by the Internet. Hence an incipient interest has emerged for combining the independence of a Java Card with the extensive flexibility of the Internet in a manner which respects the high security requirements one must demand when dealing with intelligent cards. In particular the "Smart Card" standards do currently not support downloading of executable code onto the card since it opens up too many security breaches. The establishment of a trusted relation with the code distributer, e.g., based on cryptographic techniques, would create a single point of failure relation, which could be fatal when dealing with large distributions of cards. Moreover, the administration of such trusted rel...
Cited by 0
Stephen N. Freund · 1998
Java bytecode subroutines are used to compile the Java source language try-finally construct into a succinct combination of special-purpose instructions. However, the space saved by using subroutines, in comparison to simpler compilation strategies, comes at a substantial cost to the complexity of the bytecode verifier and other parts of the Java Virtual Machine. This paper examines the trade-offs between keeping subroutines and eliminating them from the Java bytecode language. We compare the cost of formally specifying the bytecode verifier and implementing the Java Virtual Machine in the presence of subroutines to the space saved by using them when compiling a set of representative Java programs. 1
Cited by 0
Raja Vallée-Rai, Laurie Hendren · 1998
In this paper we present Jimple, a 3-address intermediate representation that has been designed to simplify analysis and transformation of Java bytecode. We motivate the need for a new intermediate representation by illustrating several difficulties with optimizing the stack-based Java bytecode directly. In general, these difficulties are due to the fact that bytecode instructions affect an expression stack, and thus have implicit uses and definitions of stack locations. We propose Jimple as an alternative representation, in which each statement refers explicitly to the variables it uses. We provide both the definition of Jimple and a complete procedure for translating from Java bytecode to Jimple. This definition and translation have been implemented using Java, and finally we show how this implementation forms the heart of the Sable research projects.
Cited by 109
Cameron Calka · 2008
Assembly language is a valuable subject to teach, yet one of the most underappreciated by students. Students do not see the need for assembly language and they get through it as quickly as possible. Given the time in a computer organization course to teach assembly language, assignments – either quick-and-easy ones or those contrived-to-teach-a-point – contribute to this attitude of malaise. This paper documents a project to inject some fun into the teaching of assembly language. First, we switch the language to Java bytecode. Second, we use unique assignments to use Java bytecode with Lego Mindstorms
Cited by 0