Dennis Dams (Bell Labs), StackSnuffer: Curing Orion's Unsoundness

Software analysis and verification require abstraction of the program under consideration. As a result, many reported errors may in fact be false alarms. The Orion static analyzer reduces the ratio of false alarms by performing a state space exploration at two levels of precision. At the first level, a conservative analysis is performed. This detects all errors of a certain kind, but with a potentially high number of superfluous warnings. At the second level, each potential-error trace that is produced at the first level, is subjectedo a feasibility analysis using symbolic reasoning - typically by invoking third-party decision procedures. If a trace cannot be shown to be infeasible, it is reported. Orion's precision can be tuned by varying the resources spent in the second level.

This approach results in an excellent signal-to-noise ratio. Orion has uncovered many errors in well-tested open source code, with only little human processing required to separate the wheat from the chaff. However, the interaction between the two levels causes Orion to miss certain errors, and when used to prove absence of bugs, it therefore needs to be run with the second level switched off.

In this talk, we present an adaptation of the depth-first search algorithm, called StackSnuffer, aimed at finding all errors without sacrificing Orion's signal-to-noise ratio. We formalize correctness and discuss the condition under which StackSnuffer is correct. This condition turns out to be equivalent to reducibility of the analyzed program's flow graph.

Experiments with StackSnuffer confirm that previously missed errors are now found. Furthermore, another small adaptation to the algorithm results in an intriguing new approach to deal with loops.

Nina Amla (Cadence), Combining Abstraction Refinement and Interpolation-based Model Checking.

This talk will explore the implications of using abstraction refinement in conjunction with interpolation-based model checking. Based on experiments using a large industrial benchmark set, we conclude that when using interpolation-based model checking, measures must be taken to prevent the overhead of abstraction refinement from dominating runtime. We present two new approaches to this problem. One is a hybrid approach that decides heuristically when to apply abstraction. The other is a very coarse but inexpensive abstraction order-of-magnitude reductions in memory usage, allowing significantly larger designs to be verified.

Sebastian Burckhardt (U Penn.), Checking Consistency of Concurrent Data Types on Relaxed Memory Models

Concurrency libraries can facilitate the development of multi-threaded programs by providing concurrent implementations of familiar data types such as queues or sets. On multiprocessors, optimized algorithms can achieve superior performance by allowing concurrent data accesses without using locks for mutual exclusion. Unfortunately, such implementations often harbor subtle concurrency bugs and are susceptible to relaxations in the memory model. Moreover, state-of-the-art verification tools are not directly applicable, because they assume a sequentially consistent memory model or race-free programs.

We present our tool CheckFence that helps the algorithm designer or library implementor by exhaustively checking all concurrent executions of a given symbolic test program on the chosen memory model and verifying that they are observationally equivalent to some serial execution. CheckFence automatically translates the C implementation code (including memory ordering fences) and the test program into a SAT formula, hands the latter to a standard SAT solver, and presents formatted counterexample traces if there exist incorrect executions. We applied CheckFence to seven previously published algorithms and were able to (a) confirm correct behavior for sequentially consistent platforms or find bugs in some cases, and (b) determine how to insert memory ordering fences for correct execution on architectures with relaxed memory models.

Yeting Ge (NYU), Solving Quantified Verification Conditions using Satisfiability Modulo Theories

Joint work with Clark Barrett (NYU) & Cesare Tinelli (U Iowa)

First order logic provides a convenient formalism for describing a wide variety of verification conditions. Two main approaches to checking such conditions are pure first order automated theorem proving (ATP) and automated theorem proving based on satisfiability modulo theories (SMT). Traditional ATP systems are designed to handle quantifiers easily, but often have difficulty reasoning with respect to theories. SMT systems, on the other hand, have built-in support for many useful theories, but have a much more difficult time with quantifiers. One clue on how to get the best of both worlds can be found in the legacy system Simplify which combines built-in theory reasoning with quantifier instantiation heuristics.

Inspired by Simplify and motivated by a desire to provide a competitive alternative to ATP systems, we describe a methodology for reasoning about quantifiers in SMT systems. We present the methodology in the context of the Abstract DPLL Modulo Theories framework. Besides adapting many of Simplify's techniques, we also introduce a number of new heuristics. Most important is the notion of instantiation level which provides an effective mechanism for prioritizing the search space and managing the blow-up inherent in quantifier instantiation.

Richard Chang (UT Austin), Formal Analysis of Authentication in Bluetooth Device Pairing

Joint work with Vitaly Shmatikov (UT Austin).

Bluetooth is a popular standard for short-range wireless communications. Bluetooth device pairing enables two mobile devices to authenticate each other and establish a secure wireless connection. We present a formal analysis of authentication properties of Bluetooth device pairing. Using the ProVerif cryptographic protocol verifier, we first analyze the standard device pairing protocol specified in the Bluetooth Core Specification, which relies on short, low-entropy PINs for authentication. Our analysis confirms a previously known attack guessing attack. We then analyze a recently proposed Simple Pairing protocol. Simple Pairing involves Diffie-Hellman-based key establishment, in which authentication relies on a human visual channel : owner(s) of the mobile devices confirm the established keys by manually comparing the respective hash values of the parameters used to generate each key, as displayed on the devices’¡Ç screens. This form of authentication presents an interesting modeling challenge. We demonstrate how to formalize it in ProVerif. Our analysis shows that authentication can fail when the same device is involved in concurrent Simple Pairing sessions. We discuss the implications of this authentication failure for typical Bluetooth usage scenarios. We then refine our model to incorporate session identifiers, and prove that the authentication properties of Simple Pairing hold in the new model. Out-of-band, human-verifiable channels based on image- or audio-matching are increasingly used for authentication of mobile devices. This study is the first step towards automated analysis of formal models of human- authenticated protocols.

Yogesh Mahajan (Princeton), Verification Driven Formal Microarchitecture Modeling

Joint work with Sharad Malik (Princeton).

We will motivate and describe formal transaction-level architecture and microarchitecture modeling, which separates the computation on data from the usage of resources. Such modeling has applications to verification and we will highlight one specific application - how to check a transaction-level microarchitecture model for the presence of data hazards.

Scott Stoller (SUNY), Efficient Policy Analysis for Administrative Role Based Access Control

Abstract TBA

Stephen Edwards (Columbia), Verification Challenges in the SHIM Concurrent Language

Concurrent programming languages should be a good fit for embedded systems because they match the intrinsic parallelism of their architectures and environments. Unfortunately, typical concurrent programming formalisms are prone to races and nondeterminism, despite the presence of mechanisms such as monitors.

We propose an alternative for describing such systems. Our SHIM (software/hardware integration medium) language, which uses Kahn networks with rendezvous communication at its heart, provides scheduling-independent concurrency in an asynchronous setting. It is a C-like imperative language extended with concurrency, inter-process communication, and exceptions.

After introducing the SHIM language, we present a set of verification challenges (static deadlock detection, performance analysis, and implementation verification) specific to SHIM and propose some possible approaches to their solution. Our goal is to pose questions and hopefully find some answers related to SHIM.

John Field (IBM Research), Semantics-Based Reverse Engineering of Logical Data Models

This work is joint with G. Ramalingam, R. Komondoor, and S. Sinha.

"Show me your flowchart and conceal your tables, and I shall continue to be mystified. Show me your tables, and I won't usually need your flowchart, it'll be obvious." So said Fred Brooks in his seminal treatise on software engineering, The Mythical Man-Month. His point was that data organization, rather than code structure, is very often the key to understanding the behavior of complex applications.

In this talk, I will present a technique for extracting object-oriented (OO) data models from programs written in weakly-typed languages such as Cobol. These models, similar to UML class diagrams, can be viewed as partial program specifications, and can facilitate a variety of program maintenance and migration activities. Our algorithm is based on a semantic analysis of the program's code, and we provide a bisimulation-based formalization of what it means for an OO data model to be correct for a program.

I will begin the talk with a brief overview of software quality and verification projects at IBM Research.