Model driven code checking

Model checkers were originally developed to support the formal verification of high-level design models of distributed system designs. Over the years, they have become unmatched in precision and performance in this domain. Research in model checking has meanwhile moved towards methods that allow us to reason also about implementation level artifacts (e.g., software code) directly, instead of hand-crafted representations of those artifacts. This does not mean that there is no longer a place for the use of high-level models, but it does mean that such models are used in a different way today. In the approach that we describe here, high-level models are used to represent the environment for which the code is to be verified, but not the application itself. The code of the application is now executed as is by the model checker, while using powerful forms of abstraction on-the-fly to build the abstract state space that guides the verification process. This model-driven code checking method allows us to verify implementation level code efficiently for high-level safety and liveness properties. In this paper, we give an overview of the methodology that supports this new paradigm of code verification.     

Abstract Regular Tree Model Checking

Regular (tree) model checking (RMC) is a promising generic method for formal verification of infinite-state systems. It encodes configurations of systems as words or trees over a suitable alphabet, possibly infinite sets of configurations as finite word or tree automata, and operations of the systems being examined as finite word or tree transducers. The reachability set is then computed by a repeated application of the transducers on the automata representing the currently known set of reachable configurations. In order to facilitate termination of RMC, various acceleration schemas have been proposed. One of them is a combination of RMC with the abstract-check-refine paradigm yielding the so-called abstract regular model checking (ARMC). ARMC has originally been proposed for word automata and transducers only and thus for dealing with systems with linear (or easily linearisable) structure. In this paper, we propose a generalisation of ARMC to the case of dealing with trees which arise naturally in a lot of modelling and verification contexts. In particular, we first propose abstractions of tree automata based on collapsing their states having an equal language of trees up to some bounded height. Then, we propose an abstraction based on collapsing states having a non-empty intersection (and thus “satisfying”) the same bottom-up tree “predicate” languages. Finally, we show on several examples that the methods we propose give us very encouraging verification results.     

Modular abstractions for verifying real-time distributed systems

In this work we present a verification methodology for real-time distributed systems, based on their modular decomposition into processes. Given a distributed system, each of its components is reduced by abstracting away from details that are irrelevant for the required specification. The abstract components are then composed to form an abstract system to which a model checking procedure is applied. The abstraction relation and the specification language guarantee that if the abstract system satisfies a specification, then the original system satisfies it as well.The specification languageRTL is a branching-time version of the real-time temporal logicTPTL presented in Alur and Henzinger [1]. Its model checking is linear in the size of the system and exponential in the size of the formula. Two notions of abstraction for real-time systems are introduced, each preserving a sublanguage ofRTL.     

Code obfuscation against abstraction refinement attacks

Code protection technologies require anti reverse engineering transformations to obfuscate programs in such a way that tools and methods for program analysis become ineffective. We introduce the concept of model deformation inducing an effective code obfuscation against attacks performed by abstract model checking. This means complicating the model in such a way a high number of spurious traces are generated in any formal verification of the property to disclose about the system under attack.We transform the program model in order to make the removal of spurious counterexamples by abstraction refinement maximally inefficient. Because our approach is intended to defeat the fundamental abstraction refinement strategy, we are independent from the specific attack carried out by abstract model checking. A measure of the quality of the obfuscation obtained by model deformation is given together with a corresponding best obfuscation strategy for abstract model checking based on partition refinement.     

Lightweight Reasoning about Program Correctness

Automated verification tools vary widely in the types of properties they are able to analyze, the complexity of their algorithms, and the amount of necessary user involvement. In this paper we propose a framework for step-wise automatic verification and describe a lightweight scalable program analysis tool that combines abstraction and model checking. The tool guarantees that its True and False answers are sound with respect to the original system. We also check the effectiveness of the tool on an implementation of the Safety-Injection System.     

Abstract regular (tree) model checking

Regular model checking is a generic technique for verification of infinite-state and/or parametrised systems which uses finite word automata or finite tree automata to finitely represent potentially infinite sets of reachable configurations of the systems being verified. The problems addressed by regular model checking are typically undecidable. In order to facilitate termination in as many cases as possible, acceleration is needed in the incremental computation of the set of reachable configurations in regular model checking. In this work, we describe how various incrementally refinable abstractions on finite (word and tree) automata can be used for this purpose. Moreover, the use of abstraction does not only increase chances of the technique to terminate, but it also significantly reduces the problem of an explosion in the number of states of the automata that are generated by regular model checking. We illustrate the efficiency of abstract regular (tree) model checking in verification of simple systems with various sources of infinity such as unbounded counters, queues, stacks, and parameters. We then show how abstract regular tree model checking can be used for verification of programs manipulating tree-like dynamic data structures. Even more complex data structures can be handled using a suitable tree-like encoding.     

A flexible real-time scheduling abstraction: design and implementation

An evolution is happening in the way that operating systems support the real-time requirements of their applications. The need to run real-time applications such as multimedia in the same environment as complex non-real-time servers and applications has motivated much interest in restructuring existing operating systems. Many issues related to thread scheduling and synchronization have been investigated. However, little consideration has been given to the flexibility and modularity required in the support of application-level scheduling needs, although it is well known that application requirements are diverse. In this paper, we describe a real-time scheduling abstraction which provides modularity and flexibility to the scheduling support of operating systems. Our design has been implemented using the Mach 3.0 kernel and a locally developed multiprocessor kernel (the r-kernel) as development platforms. © 1997 John Wiley & Sons, Ltd.     

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.     

模型检测新技术研究

1 引言软件是否可信赖已成为一个国家的经济、国防等系统能否正常运转的关键因素之一,尤其在一些诸如核反应堆控制、航空航天以及铁路调度等安全悠关(safety-critical)领域更是如此。这类系统要求绝对安全可靠,不容半点疏漏,否则将导致灾难性后果。如1996年6月4日,欧洲航天局阿丽亚娜(Ariane)501火箭因为其控制软件的规范和设计错误而导致发射37秒后爆炸。类似的报道屡见不鲜,如何确保这些系统的可靠性成为计算机科学与控制论领域共同关注的一个焦点问题。     

Controlled composition and abstraction for bottom-up integration and verification of abstract components

This work proposes a method for improving the scalability of model-checking compositions in the bottom-up construction of abstract components. The approach uses model checking in the model construction process for testing the composite behaviors of components, including process deadlock and inconsistency in inter-component call sequences. Assuming a single processor model, the scalability issue is addressed by introducing operational models for synchronous/asynchronous inter-component message passing, which are designed to reduce spurious behaviors caused by typical parallel compositions. Together with two abstraction techniques, synchronized abstraction and projection abstraction, that hide verified internal communication behavior, this operational model helps to reduce the complexity of composition and verification.The approach is supported by the Marmot development framework, where the soundness of the approach is assured through horizontal verification as well as vertical verification. Application of the approach on a wireless sensor network application shows promising performance improvement with linear growth in memory usage for the vertically incremental verification of abstract components.     

Light-Weight SMT-based Model Checking

Recently, the notion of an array-based system has been introduced as an abstraction of infinite state systems (such as mutual exclusion protocols or sorting programs) which allows for model checking of invariant (safety) and recurrence (liveness) properties by Satisfiability Modulo Theories (SMT) techniques. Unfortunately, the use of quantified first-order formulae to describe sets of states makes fix-point checking extremely expensive. In this paper, we show how invariant properties for a sub-class of array-based systems can be model-checked by a backward reachability algorithm where the length of quantifier prefixes is efficiently controlled by suitable heuristics. We also present various refinements of the reachability algorithm that allows it to be easily implemented in a client-server architecture, where a “light-weight” algorithm is the client generating proof obligations for safety and fix-point checks and an SMT solver plays the role of the server discharging the proof obligations. We also report on some encouraging preliminary experiments with a prototype implementation of our approach.     

面向源代码的软件模型检测及其实现

模型检测应用于检测软件可靠性具有重要意义.介绍了一种基于谓词抽象和反例引导抽象求精技术对源程序进行建模和验证的模型检测方法,并结合自行研发的Jchecker工具详细介绍了该软件模型检测技术的运作过程和关键算法.     

反例引导的模型检验工具的设计

针对模型组合中常见的"状态空间爆炸"问题,分析了抽象和组合两种方法各自的优缺点,采用"反例引导的抽象精化"框架和模型检验思想,将抽象和组合结合起来,为模型组合的检验提出了一种新的方法.设计了模型的抽象、组合、检验和精化算法,开发了一款基于反例引导的、图形化的模型检验工具,使用Kripke结构建立模型,用LTL描述性质,从而表明了反例引导的模型检验方法的过程.     

Finding feasible abstract counter-examples

A strength of model checking is its ability to automate the detection of subtle system errors and produce traces that exhibit those errors. Given the high-computational cost of model checking most researchers advocate the use of aggressive property-preserving abstractions. Unfortunately, the more aggressively a system is abstracted the more infeasible behavior it will have. Thus, while abstraction enables efficient model checking it also threatens the usefulness of model checking as a defect detection tool, since it may be difficult to determine whether a counter-example is feasible and hence worth developer time to analyze.We have explored several strategies for addressing this problem by extending an explicit-state model checker, Java PathFinder (JPF), to search for and analyze counter-examples in the presence of abstractions. We demonstrate that these techniques effectively preserve the defect detection ability of model checking in the presence of aggressive abstraction by applying them to check properties of several abstracted multi-threaded Java programs. These new capabilities are not specific to JPF and can be easily adapted to other model checking frameworks; we describe how this was done for the Bandera toolset.     

The Elmwood multiprocessor operating system

Elmwood is an object-oriented, multiprocessor operating system designed and implemented during a graduate seminar. It consists of a minimal kernel and a collection of user-implemented services. The kernel provides two major abstractions: objects, which consist of code and data, and processes, which represent asynchronous activity. Objects, like programs, are passive. To operate on an abstraction or to request a service, processes invoke an entry procedure defined by the corresponding object. Objects implement their own protection and synchronization policies using minimal kernel mechanisms. We describe the Elmwood kernel interface, an implementation on the BBN Butterfly parallel processor, and our experiences in developing a multiprocessor operating system under rigid time constraints. These experiences illustrate several general lessons regarding kernel design and trade-offs for implementation expedience.