nach oben

2009 | Buch

Kapitel lesen Erstes Kapitel lesen

Model Checking Software

16th International SPIN Workshop, Grenoble, France, June 26-28, 2009. Proceedings

herausgegeben von: Corina S. Păsăreanu

Verlag: Springer Berlin Heidelberg

Buchreihe : Lecture Notes in Computer Science

Enthalten in: Springer Professional "Wirtschaft+Technik" , Springer Professional "Technik" , Springer Professional "Wirtschaft"

Einloggen, um Zugang zu erhalten

Inhaltsverzeichnis

Frontmatter

Invited Contributions

Software Model Checking Improving Security of a Billion Computers

Abstract

I will present a form of software model checking that has improved the security of a billion computers (and has saved Microsoft millions of dollars). This form of software model checking is dubbed whitebox fuzz testing, and builds upon recent advances in systematic dynamic test generation (also known as DART) and constraint solving. Starting with a well-formed input, whitebox fuzzing symbolically executes the sequential program under test dynamically, and gathers constraints on inputs from conditional statements encountered along the execution. The collected constraints are negated systematically one-by-one and solved with a constraint solver, yielding new inputs that exercise different execution paths in the program. This process is repeated using novel state-space exploration techniques that attempt to sweep through all (in practice, many) feasible execution paths of the program while checking simultaneously many properties. This approach thus combines program analysis, testing, model checking and automated theorem proving (constraint solving).

Whitebox fuzzing has been implemented in the tool SAGE, which is optimized for long symbolic executions at the x86 binary level. Over the past 18 months, SAGE has been running on hundreds of machines and has discovered many new expensive security-critical bugs in large shipped Windows applications, including image processors, media players and file decoders, that are deployed on more than a billion computers worldwide. SAGE is so effective in finding bugs missed by other techniques like static analysis or blackbox random fuzzing that it is now used daily in various Microsoft groups.

This is joint work with Michael Levin (Microsoft CSE) and other contributors.

Patrice Godefroid

On Quantitative Software Verification

Abstract

Software verification has made great progress in recent years, resulting in several tools capable of working directly from source code, for example, SLAM and Astree. Typical properties that can be verified are expressed as Boolean assertions or temporal logic properties, and include whether the program eventually terminates, or the executions never violate a safety property. The underlying techniques crucially rely on the ability to extract from programs, using compiler tools and predicate abstraction, finite-state abstract models, which are then iteratively refined to either demonstrate the violation of a safety property (e.g. a buffer overflow) or guarantee the absence of such faults. An established method to achieve this automatically executes an abstraction-refinement loop guided by counterexample traces [1].

Marta Kwiatkowska

The Quest for Correctness-Beyond a Posteriori Verification

Abstract

In this presentation, I discuss the main achievements in the area of formal verification, in particular regarding their impact thus far on the development of Computer Science as a discipline and on future research directions.

The presentation starts with a short overview of formal verification techniques and their main characteristics, followed by an analysis of their current status with respect to: 1) requirements specification; 2) faithfulness of modeling; 3) scalability of verification methods. Compositional modeling and verification is the main challenge to tackling complexity. System verification should be tightly integrated into the design process, making use of knowledge about the system’s structure and its properties.

I identify two complementary research directions for overcoming some of the current difficulties in compositional techniques: 1) Moving away from low-level automata-based composition to component-based composition, by developing frameworks encompassing heterogeneous components; 2) Using such frameworks to study compositionality techniques for particular architectures and/or specific properties.

I illustrate these ideas through the BIP (Behavior, Interaction, Priority) component framework which encompasses high-level composition of heterogeneous components.

BIP supports a design methodology for building systems in a three-dimensional design space by using property-preserving transformations. This allows efficient compositional verification techniques for proving invariants, and deadlock-freedom in particular.

Joseph Sifakis

Who Really Cares If the Program Crashes?

Abstract

After spending eight years at NASA doing research in model checking and testing, I decided it would be a nice change of scene to see how software is being developed in a fast-paced technology start-up (SEVEN Networks). Of course I was secretly hoping to solve all their testing problems with the cool research techniques from the verification and testing community.

At NASA software is written once, for the most part run once, and if it fails there are serious (even life-threatening) consequences. Clearly this is a fruitful hunting ground for advanced verification and testing technology. At SEVEN, on the other hand, code is maintained and adapted for years and the same programs execute thousands of times a second on various platforms. Failures are plentiful, but they only become important once they start to impact service level agreements with the paying customers; i.e. when they start to have a negative impact on the bottom-line. Failures are not necessarily crashes either, it is much more likely to be a performance bottle-neck that eventually causes a system-wide failure. What does the verification and testing community have to offer in this arena, bearing in mind there are very few ”NASA”s and very many ”SEVEN”s in the world?

This talk is about what I learned in the past two years at SEVEN and how it is influencing my current research. In particular I will explain why I ran a model checker on SEVEN code just once, used a static analysis tool only once as well, the reasons why model based testing is no longer used at SEVEN, why I am no longer certain deadlocks are so important (but races are), why SQL is a useful debugging aid and why performance analysis is important. I will also highlight some of the more interesting errors I encountered at SEVEN and why our current tools cannot find most of these.

Willem Visser

Regular Papers

Tool Presentation: Teaching Concurrency and Model Checking

Abstract

This paper describes software tools for teaching concurrency and model checking. jSpin is an development environment for Spin that formats and filters the output of a simulation according to the user’s specification. SpinSpider uses debugging output from Spin to generate a diagram of the state space of a Promela model; the diagram can be incrementally displayed using iDot. VN supports teaching nondeterministic finite automata. The Erigone model checker is a partial reimplementation of Spin designed to be easy to use, well structured and well documented. It produces a full trace of the execution of the model checker in a format that is both readable and amenable to postprocessing.

Mordechai (Moti) Ben-Ari

Fast, All-Purpose State Storage

Abstract

Existing techniques for approximate storage of visited states in a model checker are too special-purpose and too DRAM-intensive. Bitstate hashing, based on Bloom filters, is good for exploring most of very large state spaces, and hash compaction is good for high-assurance verification of more tractable problems. We describe a scheme that is good at both, because it adapts at run time to the number of states visited. It does this within a fixed memory space and with remarkable speed and accuracy. In many cases, it is faster than existing techniques, because it only ever requires one random access to main memory per operation; existing techniques require several to have good accuracy. Adapting to accommodate more states happens in place using streaming access to memory; traditional rehashing would require extra space, random memory accesses, and hash computation. The structure can also incorporate search stack matching for partial-order reductions, saving the need for extra resources dedicated to an additional structure. Our scheme is wellsuited for a future in which random accesses to memory are more of a limiting factor than the size of memory.

Peter C. Dillinger, Panagiotis (Pete) Manolios

Efficient Probabilistic Model Checking on General Purpose Graphics Processors

Abstract

We present algorithms for parallel probabilistic model checking on general purpose graphic processing units (GPGPUs). For this purpose we exploit the fact that some of the basic algorithms for probabilistic model checking rely on matrix vector multiplication. Since this kind of linear algebraic operations are implemented very efficiently on GPGPUs, the new parallel algorithms can achieve considerable runtime improvements compared to their counterparts on standard architectures. We implemented our parallel algorithms on top of the probabilistic model checker PRISM. The prototype implementation was evaluated on several case studies in which we observed significant speedup over the standard CPU implementation of the tool.

Dragan Bošnački, Stefan Edelkamp, Damian Sulewski

Improving Non-Progress Cycle Checks

Abstract

This paper introduces a new model checking algorithm that searches for non-progress cycles, used mainly to check for livelocks. The algorithm performs an incremental depth-first search, i.e., it searches through the graph incrementally deeper. It simultaneously constructs the state space and searches for non-progress cycles. The algorithm is expected to be more efficient than the method the model checker SPIN currently uses, and finds shortest (w.r.t. progress) counterexamples. Its only downside is the need for a subsequent reachability depth-first search (which is not the bottleneck) for constructing a full counterexample. The new algorithm is better combinable with partial order reduction than SPIN’s method.

David Faragó, Peter H. Schmitt

Reduction of Verification Conditions for Concurrent System Using Mutually Atomic Transactions

Abstract

We present a new symbolic method based on partial order reduction to reduce verification problem size and state space of a multi-threaded concurrent system with shared variables and locks. We combine our method with a previous token-based approach that generates verification conditions directly without a scheduler. For a bounded unrolling of threads, the previous approach adds concurrency constraints between all pairs of global accesses. We introduce the notion of Mutually Atomic Transactions (MAT), i.e., two transactions are mutually atomic when there exists exactly one conflicting shared-access pair between them. We propose to reduce the verification conditions by adding concurrency constraints only between MATs. Such an approach removes all redundant interleavings, thereby, achieves state reduction as well. We guarantee that our MAT-based reduction is both adequate (preserves all the necessary interleavings) and optimal (no redundant interleaving), for a bounded depth analysis. Our experimental results show the efficacy of our approach in reducing the state space and the verification problem sizes by orders of magnitude, and thereby, improving the overall performance, compared with the state-of-the-art approaches.

Malay K. Ganai, Sudipta Kundu

Probabilistic Reachability for Parametric Markov Models

Abstract

Given a parametric Markov model, we consider the problem of computing the rational function expressing the probability of reaching a given set of states. To attack this principal problem, Daws has suggested to first convert the Markov chain into a finite automaton, from which a regular expression is computed. Afterwards, this expression is evaluated to a closed form function representing the reachability probability. This paper investigates how this idea can be turned into an effective procedure. It turns out that the bottleneck lies in the growth of the regular expression relative to the number of states (n ^Θ(logn)). We therefore proceed differently, by tightly intertwining the regular expression computation with its evaluation. This allows us to arrive at an effective method that avoids this blow up in most practical cases. We give a detailed account of the approach, also extending to parametric models with rewards and with non-determinism. Experimental evidence is provided, illustrating that our implementation provides meaningful insights on non-trivial models.

Ernst Moritz Hahn, Holger Hermanns, Lijun Zhang

Extrapolation-Based Path Invariants for Abstraction Refinement of Fifo Systems

Abstract

The technique of counterexample-guided abstraction refinement (Cegar) has been successfully applied in the areas of software and hardware verification. Automatic abstraction refinement is also desirable for the safety verification of complex infinite-state models. This paper investigates Cegar in the context of formal models of network protocols, in our case, the verification of fifo systems. Our main contribution is the introduction of extrapolation-based path invariants for abstraction refinement. We develop a range of algorithms that are based on this novel theoretical notion, and which are parametrized by different extrapolation operators. These are utilized as subroutines in the refinement step of our Cegar semi-algorithm that is based on recognizable partition abstractions. We give sufficient conditions for the termination of Cegar by constraining the extrapolation operator. Our empirical evaluation confirms the benefit of extrapolation-based path invariants.

Alexander Heußner, Tristan Le Gall, Grégoire Sutre

A Decision Procedure for Detecting Atomicity Violations for Communicating Processes with Locks

Abstract

We present a new decision procedure for detecting property violations in pushdown models for concurrent programs that use lock-based synchronization, where each thread’s lock operations are properly nested (à la synchronized methods in Java). The technique detects violations expressed as indexed phase automata (PAs)—a class of non-deterministic finite automata in which the only loops are self-loops.

Our interest in PAs stems from their ability to capture atomic-set serializability violations. (Atomic-set serializability is a relaxation of atomicity to only a user-specified set of memory locations.) We implemented the decision procedure and applied it to detecting atomic-set-serializability violations in models of concurrent Java programs. Compared with a prior method based on a semi-decision procedure, not only was the decision procedure 7.5X faster overall, but the semi-decision procedure timed out on about 68% of the queries versus 4% for the decision procedure.

Nicholas Kidd, Peter Lammich, Tayssir Touili, Thomas Reps

Eclipse Plug-In for Spin and st2msc Tools-Tool Presentation

Abstract

In this article we present an Eclipse plug-in for Spin and st2msc tools. The plug-in can be used to edit a Promela model, run the formal verification of the model, and generate optimized MSC of the Spin trail by st2msc. It simplifies handling with extensive Promela models to a great extent.

Tim Kovše, Boštjan Vlaovič, Aleksander Vreže, Zmago Brezočnik

Symbolic Analysis via Semantic Reinterpretation

Abstract

The paper presents a novel technique to create implementations of the basic primitives used in symbolic program analysis: forward symbolic evaluation, weakest liberal precondition, and symbolic composition. We used the technique to create a system in which, for the cost of writing just one specification—an interpreter for the programming language of interest—one obtains automatically-generated, mutually-consistent implementations of all three symbolic-analysis primitives. This can be carried out even for languages with pointers and address arithmetic. Our implementation has been used to generate symbolic-analysis primitives for x86 and PowerPC.

Junghee Lim, Akash Lal, Thomas Reps

EMMA: Explicit Model Checking Manager (Tool Presentation)

Abstract

Although model checking is usually described as an automatic technique, the verification process with the use of model checker is far from being fully automatic. In this paper we elaborate on concept of a verification manager, which contributes to automation of the verification process by enabling efficient parallel combination of different verification techniques. We introduce a tool EMMA (Explicit Model checking MAnager), which is a practical realization of the concept, and discuss practical experience with the tool.

Radek Pelánek, Václav Rosecký

Efficient Testing of Concurrent Programs with Abstraction-Guided Symbolic Execution

Abstract

In this work we present an abstraction-guided symbolic execution technique that quickly detects errors in concurrent programs. The input to the technique is a set of target locations that represent a possible error in the program. We generate an abstract system from a backward slice for each target location. The backward slice contains program locations relevant in testing the reachability of the target locations. The backward slice only considers sequential execution and does not capture any inter-thread dependencies. A combination of heuristics are to guide a symbolic execution along locations in the abstract system in an effort to generate a corresponding feasible execution trace to the target locations. When the symbolic execution is unable to make progress, we refine the abstraction by adding locations to handle inter-thread dependencies. We demonstrate empirically that abstraction-guided symbolic execution generates feasible execution paths in the actual system to find concurrency errors in a few seconds where exhaustive symbolic execution fails to find the same errors in an hour.

Neha Rungta, Eric G. Mercer, Willem Visser

Subsumer-First: Steering Symbolic Reachability Analysis

Abstract

Symbolic reachability analysis provides a basis for the verification of software systems by offering algorithmic support for the exploration of the program state space when searching for proofs or counterexamples. The choice of exploration strategy employed by the analysis has direct impact on its success, whereas the ability to find short counterexamples quickly and—as a complementary task—to efficiently perform the exhaustive state space traversal are of utmost importance for the majority of verification efforts. Existing exploration strategies can optimize only one of these objectives which leads to a sub-optimal reachability analysis, e.g., breadth-first search may sacrifice the exploration efficiency and chaotic iteration can miss minimal counterexamples. In this paper we present subsumer-first, a new approach for steering symbolic reachability analysis that targets both minimal counterexample discovery and efficiency of exhaustive exploration. Our approach leverages the result of fixpoint checks performed during symbolic reachability analysis to bias the exploration strategy towards its objectives, and does not require any additional computation. We demonstrate how the subsumer-first approach can be applied to improve efficiency of software verification tools based on predicate abstraction. Our experimental evaluation indicates the practical usefulness of the approach: we observe significant efficiency improvements (median value 40%) on difficult verification benchmarks from the transportation domain.

Andrey Rybalchenko, Rishabh Singh

Identifying Modeling Errors in Signatures by Model Checking

Abstract

Most intrusion detection systems deployed today apply misuse detection as analysis method. Misuse detection searches for attack traces in the recorded audit data using predefined patterns. The matching rules are called signatures. The definition of signatures is up to now an empirical process based on expert knowledge and experience. The analysis success and accordingly the acceptance of intrusion detection systems in general depend essentially on the topicality of the deployed signatures. Methods for a systematic development of signatures have scarcely been reported yet, so the modeling of a new signature is a time-consuming, cumbersome, and error-prone process. The modeled signatures have to be validated and corrected to improve their quality. So far only signature testing is applied for this. Signature testing is still a rather empirical and time-consuming pro cess to detect modeling errors. In this paper we present the first approach for verifying signature specifications using the Spin model checker. The signatures are modeled in the specification language EDL which leans on colored Petri nets. We show how the signature specification is transformed into a Promela model and how characteristic specification errors can be found by Spin.

Sebastian Schmerl, Michael Vogel, Hartmut König

Towards Verifying Correctness of Wireless Sensor Network Applications Using Insense and Spin

Abstract

The design and implementation of wireless sensor network applications often require domain experts, who may lack expertise in software engineering, to produce resource-constrained, concurrent, real-time software without the support of high-level software engineering facilities. The Insense language aims to address this mismatch by allowing the complexities of synchronisation, memory management and event-driven programming to be borne by the language implementation rather than by the programmer. The main contribution of this paper is an initial step towards verifying the correctness of WSN applications with a focus on concurrency. We model part of the synchronisation mechanism of the Insense language implementation using Promela constructs and verify its correctness using Spin. We demonstrate how a previously published version of the mechanism is shown to be incorrect by Spin, and give complete verification results for the revised mechanism.

Oliver Sharma, Jonathan Lewis, Alice Miller, Al Dearle, Dharini Balasubramaniam, Ron Morrison, Joe Sventek

Verification of GALS Systems by Combining Synchronous Languages and Process Calculi

Abstract

A Gals (Globally Asynchronous Locally Synchronous) system typically consists of a collection of sequential, deterministic components that execute concurrently and communicate using slow or unreliable channels. This paper proposes a general approach for modelling and verifying Gals systems using a combination of synchronous languages (for the sequential components) and process calculi (for communication channels and asynchronous concurrency). This approach is illustrated with an industrial case-study provided by Airbus: a TftpUdp communication protocol between a plane and the ground, which is modelled using the Eclipse/Topcased workbench for model-driven engineering and then analysed formally using the Cadp verification and performance evaluation toolbox.

Hubert Garavel, Damien Thivolle

Experience with Model Checking Linearizability

Abstract

Non-blocking concurrent algorithms offer significant performance advantages, but are very difficult to construct and verify. In this paper, we describe our experience in using SPIN to check linearizability of non-blocking concurrent data-structure algorithms that manipulate dynamically allocated memory. In particular, this is the first work that describes a method for checking linearizability with non-fixed linearization points.

Martin Vechev, Eran Yahav, Greta Yorsh

Automatic Discovery of Transition Symmetry in Multithreaded Programs Using Dynamic Analysis

Abstract

While symmetry reduction has been established to be an important technique for reducing the search space in model checking, its application in concurrent software verification is still limited, due to the difficulty of specifying symmetry in realistic software. We propose an algorithm for automatically discovering and applying transition symmetry in multithreaded programs during dynamic model checking. Our main idea is using dynamic program analysis to identify a permutation of variables and labels of the program that entails syntactic equivalence among the residual code of threads and to check whether the local states of threads are equivalent under the permutation. The new transition symmetry discovery algorithm can bring substantial state space savings during dynamic verification of concurrent programs. We have implemented the new algorithm in the dynamic model checker Inspect. Our preliminary experiments show that this algorithm can successfully discover transition symmetries that are hard or otherwise cumbersome to identify manually, and can significantly reduce the model checking time while using Inspect to examine realistic multithreaded applications.

Yu Yang, Xiaofang Chen, Ganesh Gopalakrishnan, Chao Wang

Backmatter

Titel: Model Checking Software
herausgegeben von: Corina S. Păsăreanu
Verlag: Springer Berlin Heidelberg
Electronic ISBN: 978-3-642-02652-2
Print ISBN: 978-3-642-02651-5
DOI: https://doi.org/10.1007/978-3-642-02652-2