jContractor: Bytecode Instrumentation Techniques for Implementing Design by Contract in Java

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 a detailed design and implementation overview of jContractor, a freely available tool that allows programmers to write “contracts” as standard Java methods following an intuitive naming convention. Preconditions, postconditions, and invariants can be associated with, or inherited by, any class or interface. jContractor performs on-the-fly bytecode instrumentation to detect violation of the contract specification during a program's execution. jContractor's bytecode engineering technique allows it to specify and check contracts even when source code is not available. jContractor is a pure Java library providing a rich set of syntactic constructs for expressing contracts without extending the Java language or runtime environment. These constructs include support for predicate logic expressions, and referencing entry values of attributes and return values of methods. Fine grain control over the level of monitoring is possible at runtime. Since contract methods are allowed to use unconstrained Java expressions, in addition to runtime verification they can perform additional runtime monitoring, logging, and testing.     

Jass — Java with Assertions

Design by Contract, proposed by Meyer for the programming language Eiffel, is a technique that allows run-time checks of specification violation and their treatment during program execution. Jass, Java with assertions, is a Design by Contract extension for Java allowing to annotate Java programs with specifications in the form of assertions. The Jass tool is a pre-compiler that translates annotated into pure Java programs in which compliance with the specification is dynamically tested. Besides the standard Design by Contract features known from classical program verification (e.g. pre- and postconditions, invariants), Jass additionally supports refinement, i.e. subtyping, checks and the novel concept of trace assertions. Trace assertions are used to monitor the dynamic behaviour of objects in time.     

Design by Contract to Improve Software Vigilance

Design by contract is a lightweight technique for embedding elements of formal specification (such as invariants, pre and postconditions) into an object-oriented design. When contracts are made executable, they can play the role of embedded, online oracles. Executable contracts allow components to be responsive to erroneous states and, thus, may help in detecting and locating faults. In this paper, we define vigilance as the degree to which a program is able to detect an erroneous state at runtime. Diagnosability represents the effort needed to locate a fault once it has been detected. In order to estimate the benefit of using design by contract, we formalize both notions of vigilance and diagnosability as software quality measures. The main steps of measure elaboration are given, from informal definitions of the factors to be measured to the mathematical model of the measures. As is the standard in this domain, the parameters are then fixed through actual measures, based on a mutation analysis in our case. Several measures are presented that reveal and estimate the contribution of contracts to the overall quality of a system in terms of vigilance and diagnosability     

Uncovering hidden contracts: the .NET example

Software contracts take the form of routine preconditions, postconditions, and class invariants written into the program itself. The design by contract methodology uses such contracts for building each software element, an approach that is particularly appropriate for developing safety-critical software and reusable libraries. This methodology is a key design element of some existing libraries, especially the Eiffel Software development environment, which incorporates contract mechanisms in the programming language itself. Because the authors see the contract metaphor as inherent to quality software development, they undertook the work reported in the article as a sanity check to determine whether they see contracts everywhere simply because their development environment makes using them natural or whether contracts are intrinsically present, even when other designers don't express or even perceive them. They studied classes from the .NET collections library for implicit contracts and assessed improvements that might result from making them explicit.     

程序不变量检测技术

基于合约的程序设计是提高软件质量的一种重要技术,已经得到了很大的发展。合约描述了程序内部的基本属性、程序良性运行的保证条件以及运行后的期望结果。作为合约的一种表达形式,程序不变量一般包含类不变量、前置条件和后置条件。程序不变量是程序中隐含的属性,它可以应用于程序验证、软件测试技术、逆向工程、程序质量保证等领域。本文结合当前主流的程序不变量研究的相关成果和基于合约的程序不变量程序设计方法,分别从源程序编配技术、测试用例生成技术、程序运行轨迹收集技术和程序不变量分析技术四个方面,对程序不变量挖掘的关键方法和原理进行了详细的剖析。     

Specifying and checking method call sequences of Java programs

In a pre and postcondition-style specification, it is difficult to specify the allowed sequences of method calls, referred to as protocols. The protocols are essential properties of reusable object-oriented classes and application frameworks, and the approaches based on the pre and postconditions, such as design by contracts (DBC) and formal behavioral interface specification languages (BISL), are being accepted as a practical and effective tool for describing precise interfaces of (reusable) program modules. We propose a simple extension to the Java Modeling Language (JML), a BISL for Java, to specify protocol properties in an intuitive and concise manner. The key idea of our approach is to separate protocol properties from functional properties written in pre and post-conditions and to specify them in a regular expression-like notation. The semantics of our extension is formally defined and provides a foundation for implementing runtime checks. Case studies have been performed to show the effectiveness our approach. We believe that our approach can be adopted by other BISLs.

Application invariants: Design by Contract augmented with deployment correctness logic

Design by Contract is a method for the development of robust object‐oriented software, introducing class invariants as conditions corresponding to the design axioms that should be satisfied by every valid instance of a class. Additionally, the method states formally the way client programs should correctly utilize supplier classes, so that the composition of correct programs may be accomplished. However, the contextual correctness of supplier instances within client programs, only reflected in the client‐specific semantics for supplier‐class deployment, cannot be expressed through Design by Contract. For instance, supplier instances satisfying the supplier class invariant may not constitute plausible supplier instances in the context of a particular client program. In this context, we introduce application invariants as an extension to Design by Contract, for hosting the contextual‐correctness logic for supplier instances, as conditionally defined by client programs. This allows stronger validation of supplier instances, through the dynamic encapsulation of client‐specific acceptance filtering, enabling more intensive defect detection. Application invariants are implemented in the context of client classes as methods utilizing correctness condition expressions, are dynamically hosted within supplier instances, while always called by supplier instances when the basic supplier‐class invariant test is performed. Copyright © 2005 John Wiley & Sons, Ltd.     

Reverse-engineering 1-n associations from Java bytecode using alias analysis

1-n associations are design language constructs that represent one-to-many structural invariants for objects. To implement 1-n associations, container classes, such as Vector in Java, are frequently used as programming language constructs. Many of the current CASE tools fail to reverse-engineer 1-n associations that have been implemented via containers because sophisticated analyses are required to infer the type of elements collected in containers. This paper presents a new approach to reverse-engineering 1-n associations from Java bytecode based on alias analysis. In our approach, 1-n associations are inferred by examining the abstract heap structure that is constructed by applying an alias analysis on inter-variable relationships extracted from assignments and method invocations of containers. Our approach handles container alias problem that has been neglected by previous techniques by approximating the relationships between containers and elements at the object level rather than analyzing only the bytecode. Our prototype implementation was used with a suite of well-known Java programs. Most of the 1-n associations were successfully reverse-engineered from hundreds of class files in less than 1 minute.     

Static verification of dynamically detected program invariants: Integrating Daikon and ESC/Java

This paper shows how to integrate two complementary techniques for manipulating program invariants: dynamic detection and static verification. Dynamic detection proposes likely invariants based on program executions, but the resulting properties are not guaranteed to be true over all possible executions. Static verification checks that properties are always true, but it can be difficult and tedious to select a goal and to annotate programs for input to a static checker. Combining these techniques overcomes the weaknesses of each: dynamically detected invariants can annotate a program or provide goals for static verification, and static verification can confirm properties proposed by a dynamic tool.We have integrated a tool for dynamically detecting likely program invariants, Daikon, with a tool for statically verifying program properties, ESC/Java. Daikon examines run-time values of program variables; it looks for patterns and relationships in those values, and it reports properties that are never falsified during test runs and that satisfy certain other conditions, such as being statistically justified. ESC/Java takes as input a Java program annotated with preconditions, postconditions, and other assertions, and it reports which annotations cannot be statically verified and also warns of potential runtime errors, such as null dereferences and out-of-bounds array indices.Our prototype system runs Daikon, inserts its output into code as ESC/Java annotations, and then runs ESC/Java, which reports unverifiable annotations. The entire process is completely automatic, though users may provide guidance in order to improve results if desired. In preliminary experiments, ESC/Java verified all or most of the invariants proposed by Daikon.     

Behavioral specification of distributed software componentinterfaces

Networked computers are finding their way into a broader range of environments, from corporate offices to schools, homes, and shirt pockets. This new computing model fosters the development of distributed software components that communicate with one another across the underlying networked infrastructure. A distributed software component can be plugged into distributed applications that may not have existed when it was created. The intention is that many developers will reuse distributed software components to build new systems. An interface definition language usually is used to describe a distributed software component's interface. However, a notable limitation of current IDLs is that they generally only describe the names and type signatures of the component's attributes and operations. Current IDLs don't formally specify the behavior of the software component's operations. To help solve these problems, the authors have developed Biscotti (behavioral specification of distributed software component interfaces), a Java extension that enhances Java remote method invocation interfaces with Eiffel-style preconditions, postconditions, and invariants     

Polymorphic bytecode instrumentation

Bytecode instrumentation is a widely used technique to implement aspect weaving and dynamic analyses in virtual machines such as the Java virtual machine. Aspect weavers and other instrumentations are usually developed independently and combining them often requires significant engineering effort, if at all possible. In this article, we present polymorphic bytecode instrumentation(PBI), a simple but effective technique that allows dynamic dispatch amongst several, possibly independent instrumentations. PBI enables complete bytecode coverage, that is, any method with a bytecode representation can be instrumented. We illustrate further benefits of PBI with three case studies. First, we describe how PBI can be used to implement a comprehensive profiler of inter‐procedural and intra‐procedural control flow. Second, we provide an implementation of execution levels for AspectJ, which avoids infinite regression and unwanted interference between aspects. Third, we present a framework for adaptive dynamic analysis, where the analysis to be performed can be changed at runtime by the user. We assess the overhead introduced by PBI and provide thorough performance evaluations of PBI in all three case studies. We show that pure Java profilers like JP2 can, thanks to PBI, produce accurate execution profiles by covering all code, including the core Java libraries. We then demonstrate that PBI‐based execution levels are much faster than control flow pointcuts to avoid interference between aspects and that their efficient integration in a practical aspect language is possible. Finally, we report that PBI enables adaptive dynamic analysis tools that are more reactive to user inputs than existing tools that rely on dynamic aspect‐oriented programming with runtime weaving. These experiments position PBI as a widely applicable and practical approach for combining bytecode instrumentations. © 2015 The Authors. Software: Practice and Experience Published by John Wiley & Sons Ltd.     

基于字节码的以太坊智能合约分类方法

近年来,区块链技术已在金融、医疗和政务等领域得到了广泛应用和关注。然而,由于智能合约的不易篡改性和运行环境的特殊性,各类安全问题频繁出现。一方面是合约开发者在编写合约时出现的代码安全问题,另一方面是以太坊出现不少高风险智能合约,普通用户很容易被高风险合约提供的高回报所吸引,但对合约的风险却无从知晓。然而,关于智能合约安全的研究主要集中于代码安全方面,对合约功能识别的研究相对较少。假如能对智能合约功能进行准确分类,将有助于人们更好地理解智能合约的行为,同时保障智能合约生态安全,减少或挽回用户的损失。已有的智能合约分类方法通常依赖于对智能合约开源代码的分析,但以太坊发布的合约仅强制要求部署字节码,且只有极少数合约公布了其开源代码。因此,提出了一种基于字节码的以太坊智能合约分类方法。收集以太坊智能合约字节码和对应类别标签,然后提取操作码频率特征以及控制流图特征;通过实验对特征重要性进行分析,获取适合的图向量维度及最优的分类模型;在交易所、金融、赌博、游戏和高风险5个类别的智能合约多分类任务中进行实验验证,使用XGBoost分类器时的F1值达到0.9138。实验结果表明所提方法能较好地完成以太坊智能合约的分类任务,并且能够应用于现实中的智能合约类别预测。     

JBInsTrace: A tracer of Java and JRE classes at basic-block granularity by dynamically instrumenting bytecode

Understanding what happens during the runtime of a Java program is difficult. Tracking runtime flow can bring valuable information for program understanding and behavior analysis. Polymorphism, thread concurrency or even simple facts like the number of method invocations and the number of executed bytecodes are valuable information to track, but are difficult to compute outside the Java Virtual Machine (JVM) on running programs. In this paper, we present JBInsTrace, a new tool that instruments and traces Java bytecode. It produces static information about source code and a very fine grained trace of Java software execution, combining them to allow detailed analysis of the runtime. Our tool differs from others because it does not only trace program classes but also JRE classes, and does so at basic block level, without altering the JVM and without statically modifying class files. We explain JBInsTrace design, focused towards efficiency, which results in reasonable performance penalty.     

在Java中使用契约式设计

契约式设计DBC是面向对象程序设计的一项技术，其目的在于提高软件的质量、可靠性与可复用性。Java语言本身还不直接支持契约式设计，但借助一些外部辅助工具可以使该项技术获得应用。对此，给出了两种实现方法：一种是使用预编译器；另一种是使用面向方面的程序设计技术。     

Ambient contracts: verifying and enforcing ambient object compositions à la carte

Current programming languages do not offer adequate abstractions to discover and compose heterogenous objects over unreliable networks. This forces programmers to discover objects one by one, compose them manually, and keep track of their individual connectivity state at all times. In this paper we propose Ambient Contracts, a novel programming abstraction to deal with the difficulties of composing objects connected over unreliable networks. Ambient Contracts provide declarative heterogenous group discovery and composition while dealing with the unreliability of the network. An ambient contract allows runtime verification and enforcement of the messages sent between the participants in the contract. The use of our abstraction significantly reduces the code base and allows programmers to focus on the core functionality of their application. Our claims are reinforced by comparing the implementation of an example scenario in our contracts with a Java implementation using M2MI.     

QoS contract preservation through dynamic reconfiguration: A formal semantics approach

The increasing pervasiveness of computing services in everyday life, combined with the dynamic nature of their execution contexts, constitutes a major challenge in guaranteeing the expected quality of such services at runtime. Quality of Service (QoS) contracts have been proposed to specify expected quality levels (QoS levels) on different context conditions, with different enforcing mechanisms. In this paper we present a definition for QoS contracts as a high-level policy for governing the behavior of software systems that self-adapt at runtime in response to context changes. To realize this contract definition, we specify its formal semantics and implement it in a software framework able to execute and reconfigure software applications, in order to maintain fulfilled their associated QoS contracts. The contribution of this paper is threefold. First, we extend typed-attributed graph transformation systems and finite-state machines, and use them as denotations to specify the semantics of QoS contracts. Second, this semantics makes it possible to systematically exploit design patterns at runtime by dynamically deploying them in the managed software application. Third, our semantics guarantees self-adaptive properties such as reliability and robustness in the contract satisfaction. Finally, we evaluate the applicability of our semantics implementation by integrating and executing it in FraSCAti, a multi-scale component-based middleware, in three case studies.     

Model Checking Programs

The majority of work carried out in the formal methods community throughout the last three decades has (for good reasons) been devoted to special languages designed to make it easier to experiment with mechanized formal methods such as theorem provers, proof checkers and model checkers. In this paper we will attempt to give convincing arguments for why we believe it is time for the formal methods community to shift some of its attention towards the analysis of programs written in modern programming languages. In keeping with this philosophy we have developed a verification and testing environment for Java, called Java PathFinder (JPF), which integrates model checking, program analysis and testing. Part of this work has consisted of building a new Java Virtual Machine that interprets Java bytecode. JPF uses state compression to handle big states, and partial order and symmetry reduction, slicing, abstraction, and runtime analysis techniques to reduce the state space. JPF has been applied to a real-time avionics operating system developed at Honeywell, illustrating an intricate error, and to a model of a spacecraft controller, illustrating the combination of abstraction, runtime analysis, and slicing with model checking.     

A portable CPU-management framework for Java

The Java resource accounting framework, second edition (J-RAF2), is a portable CPU-management framework for Java environments. It is based on fully automated program-transformation techniques applied at the bytecode level and can be used with every standard Java virtual machine. J-RAF2 modifies applications, libraries, and the Java development kit itself to expose details regarding thread execution. This article focuses on the extensible runtime APIs, which are designed to let developers tailor management policies to their needs.