As mobile agents reside on on-board units or mobile devices and act on behalf of drivers, it imposes a strong demand to devise mechanisms for protecting the algorithms that are exclusively coded in mobile agents for d...
详细信息
ISBN:
(纸本)9781424465880
As mobile agents reside on on-board units or mobile devices and act on behalf of drivers, it imposes a strong demand to devise mechanisms for protecting the algorithms that are exclusively coded in mobile agents for different drivers. Although contactless smart cards are widely used as a means to protecting personal information, it is still a challenge to protect the whole code of a mobile agent in a limited storage. In this paper, we propose a tool, called jExtractor, by which the private or sensitive data coded in a java-based mobile agent can be extracted and moved to a contactless smart card, and can further be read from the card and merged to be the original mobile agent. Moreover, we use 30,000 java classes as samples to validate jExtractor. In the experimental result, 79.4% of the sample classes can successfully be extracted and moved to Mifare Standard S50 (1K) smart card with our strictest configuration level.
Automatic cost analysis has interesting applications in the context of verification and certification of mobile code. For instance, the code receiver can use cost information in order to decide whether to reject mobil...
详细信息
ISBN:
(纸本)9781595937537
Automatic cost analysis has interesting applications in the context of verification and certification of mobile code. For instance, the code receiver can use cost information in order to decide whether to reject mobile code which has too large cost requirements in terms of computing resources (in time and/or space) or billable events (SMSs sent, bandwidth required). Existing cost analyses for a variety of languages describe the resource consumption of programs by means of Cost Equation Systems (CESs), which are similar to, but more general than recurrence equations. CESs express the cost of a program in terms of the size of its input data. In a further step, a closed form (i.e., non-recursive) solution or upper bound can sometimes be found by using existing Computer Algebra Systems (CASs), such as Maple and Mathematica. In this work, we focus on cost analysis of java bytecode, a language which is widely used in the context of mobile code and we study the problem of identifying variables which are useless in the sense that they do not affect the execution cost and therefore can be ignored by cost analysis. We identify two classes of useless variables and propose automatic analysis techniques to detect them. The first class corresponds to stack variables that can be replaced by program variables or constant values. The second class corresponds to variables whose value is cost-irrelevant, i.e., does not affect the cost of the program. We propose an algorithm, inspired in static slicing which safely identifies cost-irrelevant variables. The benefits of eliminating useless variables are two-fold: (1) cost analysis without useless variables can be more efficient and (2) resulting CESs are more likely to be solvable by existing CASs.
During compilation from java source code to byte-code, some information is irreversibly lost. In other words, compilation and decompilation of java code is not symmetric. Consequently, the decompilation process, which...
详细信息
ISBN:
(纸本)9781728149370
During compilation from java source code to byte-code, some information is irreversibly lost. In other words, compilation and decompilation of java code is not symmetric. Consequently, the decompilation process, which aims at producing source code from bytecode, must establish some strategies to reconstruct the information that has been lost. Modern java decompilers tend to use distinct strategies to achieve proper decompilation. In this work, we hypothesize that the diverse ways in which bytecode can be decompiled has a direct impact on the quality of the source code produced by decompilers. We study the effectiveness of eight java decompilers with respect to three quality indicators: syntactic correctness, syntactic distortion and semantic equivalence modulo inputs. This study relies on a benchmark set of 14 real-world open-source software projects to be decompiled (2041 classes in total). Our results show that no single modern decompiler is able to correctly handle the variety of bytecode structures coming from real-world programs. Even the highest ranking decompiler in this study produces syntactically correct output for 84% of classes of our dataset and semantically equivalent code output for 78% of classes.
This article presents a heap space analysis for (sequential) java bytecode. The analysis generates heap space cost relations which define at compile-time the heap consumption of a program as a function of its data siz...
详细信息
ISBN:
(纸本)9781595938930
This article presents a heap space analysis for (sequential) java bytecode. The analysis generates heap space cost relations which define at compile-time the heap consumption of a program as a function of its data size. These relations can be used to obtain upper bounds on the heap space allocated during the execution of the different methods. In addition, we describe how to refine the cost relations, by relying on escape analysis, in order to take into account the heap space that can be safely deallocated by the garbage collector upon exit from a corresponding method. These refined cost relations are then used to infer upper bounds on the active heap space upon methods return. Example applications for the analysis consider inference of constant heap usage and heap usage proportional to the data size (including polynomial and exponential heap consumption). Our prototype implementation is reported and demonstrated by means of a series of examples which illustrate how the analysis naturally encompasses standard data-structures like lists, trees and arrays with several dimensions written in object-oriented programming style.
Program analyses are an important tool to check if a system fulfills its specification. A typical implementation strategy for program analyses is to use an imperative, general-purpose language like java;and access the...
详细信息
ISBN:
(纸本)9783319747309;9783319747293
Program analyses are an important tool to check if a system fulfills its specification. A typical implementation strategy for program analyses is to use an imperative, general-purpose language like java;and access the program to be analyzed through libraries for manipulating intermediate code, such as ASM for java bytecode. We show that this hampers composability, interoperability and reuse of analysis implementations. We propose a complete Ecore-metamodel for java bytecode as a common basis for program analysis implementations, as well as an Eclipse plug-in to create bytecode metamodel instances from java bytecode and vice versa. Code analyses can be defined as model transformations in a declarative, domain-specific language. As a consequence, the implementations of program analyses become more composable and more modular in general. We demonstrate the effectiveness of this approach with a case study.
Copied, reused and modified program code is a common phenomena in software development. As the resulting code clones are often not labeled as such and their proper detection is crucial to software quality and re-engin...
详细信息
ISBN:
(纸本)9798350344424
Copied, reused and modified program code is a common phenomena in software development. As the resulting code clones are often not labeled as such and their proper detection is crucial to software quality and re-engineering, numerous techniques and tools for finding code clones have been developed. This as well applies to the java programming language, though most clone detectors work on java source code. Only some research addresses code clones in java bytecode and an even smaller fraction investigates the relationship between java source code and bytecode code clones. In this paper, we extend the source-code based clone detector StoneDetector to java bytecode. Using BigCloneBench as state-of-the-art benchmark, we are able to assess and analyze its effectiveness in detecting source code clones in java bytecode. We also report on differences in the performance of clone detection for stack-based and register-based representations of java bytecode. The results show that, while code clones found in java source code and bytecode in general can differ, source code clones can be detected in java bytecode with high recall and precision using the presented system.
In [5, 15] we presented an approach to prove termination of non-recursive java bytecode (JBC) programs automatically. Here, JBC programs are first transformed to finite termination graphs which represent all possible ...
详细信息
ISBN:
(纸本)9783939897309
In [5, 15] we presented an approach to prove termination of non-recursive java bytecode (JBC) programs automatically. Here, JBC programs are first transformed to finite termination graphs which represent all possible runs of the program. Afterwards, the termination graphs are translated to term rewrite systems (TRSs) such that termination of the resulting TRSs implies termination of the original JBC programs. So in this way, existing techniques and tools from term rewriting can be used to prove termination of JBC automatically. In this paper, we improve this approach substantially in two ways: (1) We extend it in order to also analyze recursive JBC programs. To this end, one has to represent call stacks of arbitrary size. (2) To handle JBC programs with several methods, we modularize our approach in order to reuse termination graphs and TRSs for the separate methods and to prove termination of the resulting TRS in a modular way. We implemented our approach in the tool AProVE. Our experiments show that the new contributions increase the power of termination analysis for JBC significantly.
The work presented in this paper extends an existing constraint model defined to automatically generate test inputs for java bytecode programs. We propose to consider also BML specifications for generating valid test ...
详细信息
ISBN:
(纸本)9781509051465
The work presented in this paper extends an existing constraint model defined to automatically generate test inputs for java bytecode programs. We propose to consider also BML specifications for generating valid test data. The main objective is to apply constraint based testing on java bytecode program annotated with BML for detecting the valid execution paths, to check the validity of the returned result, to reduce the domain of input data, and to perform coverage of the testing method under test.
Security of java programs is important as they can be executed in different platforms. This paper addresses the problem of secure information flow for java bytecode. In information flow analysis one wishes to check if...
详细信息
Security of java programs is important as they can be executed in different platforms. This paper addresses the problem of secure information flow for java bytecode. In information flow analysis one wishes to check if high security data can ever propagate to low security observers. We propose a static analysis similar to the type-level abstract interpretation used for standard bytecode verification. Instead of types, our technique works with secrecy levels assigned to classes, methods' parameters and returned values, and handles implicit information flows. A verification tool based on the proposed technique is under development. Using the tool, programs downloaded from untrusted hosts can be checked locally prior to executing them.
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 interpretatio...
详细信息
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 How in the original code. We present a prototype tool that implements the method and we show an example of application. Copyright (C) 2004 John Wiley Sons, Ltd.
暂无评论