A concolic approach, called Slec-Cf, to check sequential equivalence between a high-level (e.g., C++/SystemC) hardware description and an RTL (e.g., Verilog) is presented. Slec-Cf searches for counterexamples over the possible values of a set of "control signals" in a depth-first lexicographic manner, avoiding values that are unrealizable by any concrete input. In addition, Slec-Cf respects user-specified design constraints during search, thus only producing stimuli that are of relevance to users. It is a superior alternative to random simulations, which produce an overwhelming number of irrelevant stimuli for user-constrained designs, and are therefore of limited effectiveness. To handle complex designs, we present an incremental version of Slec-Cf, which iteratively increases the search depth, and set of control signals, and uses a cache to reuse prior results. We implemented Slec-Cf on top an existing industrial tool for sequential equivalence checking. Experimental results indicate that Slec-Cf clearly outperforms random simulation in terms of coverage achieved. On complex designs, incremental Slec-Cf demonstrates superior ability to achieve good coverage in almost all cases, compared to non-incremental Slec-Cf.

Robust security on a commodity low-cost and popular computing platform is a worthy goal for today's Internet of Things (IoT) and embedded ecosystems. We present the first practical security architecture on the Raspberry PI (PI), a ubiquitous and popular low-cost compute module. Our architecture and framework - called UBERPI - focuses on three goals which are keys to achieving practical security: commodity compatibility (e.g., runs unmodified Raspbian/Debian Linux) and unfettered access to platform hardware, performance (avg. 2%-6% overhead), and low trusted computing base and complexity (modular 5544 SLoC).We present a full implementation followed by a comprehensive evaluation and lessons learned. We believe that our contributions and findings elevate the PI into a next generation, secure, low-cost IoT embedded computing platform.

A timing enforcer is a scheduler that not only allocates CPU cycles to threads, but also uses timers to enforce time budgets. An approach for verifying safety properties of timing enforcers at the source code level is presented. We assume that the enforcer is implemented as a set of “enforcer” functions that are executed atomically on critical system-level events, such as the arrival and departure of jobs, and triggering of timers. The key idea is to express the safety property as an invariant, and prove that it is inductive across all the enforcer functions. A formal semantics of timing enforcers is presented, including the semantics of functions used to read the system clock and set timers. Using this semantics, the verification approach is presented, and its soundness proved. Further, the approach also takes into consideration the periodicity of tasks. It is validated by proving the correctness of the enforcement of CPU cycle budgets for tasks by the Zero-Slack Rate Monotonic ( zsrm ) scheduler, which is implemented in C as a Linux kernel module. The inductiveness of the necessary zsrm invariants is proved by expressing them as function contracts using the acsl specification language, and verifying the contracts using the frama-c tool.

Cyber-physical systems (CPS) span the communication, computation and control domains. Creating a single, complete, and detailed model of a CPS is not only difficult, but, in terms of verification, probably not useful; current verification algorithms are likely intractable for such all-encompassing models. However, specific CPS domains have specialized formal reasoning methods that can successfully analyze certain aspects of the integrated system. To prove overall system correctness, however, care must be taken to ensure the interfaces of the proofs are consistent and leave no gaps, which can be difficult since they may use different model types and describe different aspects of the CPS.

Developing cyber-physical systems involves multiple engineering domains, e.g., timing, logical correctness, thermal resilience, and mechanical stress. In today's industrial practice, these domains rely on multiple analyses to obtain and verify critical system properties. Domain differences make the analyses abstract away interactions among themselves, potentially invalidating the results. Specifically, one challenge is to ensure that an analysis is never applied to a model that violates the assumptions of the analysis. Since such violation can originate from the updating of the model by another analysis, analyses must be executed in the correct order. Another challenge is to apply diverse analyses soundly and scalably over models of realistic complexity. To address these challenges, we develop an analysis integration approach that uses contracts to specify dependencies between analyses, determine their correct orders of application, and specify and verify applicability conditions in multiple domains. We implement our approach and demonstrate its effectiveness, scalability, and extensibility through a verification case study for thread and battery cell scheduling.

We verify safety properties of periodic programs, consisting of periodically activated threads scheduled preemptively based on their priorities. We develop an approach based on generating, and solving, a provably correct verification condition (VC). The VC is generated by adapting Lamport's sequential consistency to the semantics of periodic programs. Our approach is able to handle periodic programs that synchronize via two commonly used types of locks - priority ceiling protocol (PCP) locks, and CPU locks. To improve the scalability of our approach, we develop a strategy called snapshotting, which leads to VCs containing fewer redundant sub-formulas, and are therefore more easily solved by current SMT engines. We develop two types of snapshotting - SS-ALL snapshots all shared variables aggressively, while SS-MOD snapshots only modified variables. We have implemented our approach in a tool. Experiments on a benchmark of robot controllers indicate that SS-MOD is the best overall strategy, and even outperforms significantly the state-of-the art periodic program verifier prior to this work.

We present preliminary results on parameterized verification of distributed applications that assume a synchronous model of computation. Our theoretical results are negative -- the problem is undecidable even if each node has a single bit of non-determinism and the property is a 1-index safety property. Further, even if each node is completely deterministic, and the property is again a 1-index safety, parameterized verification cannot be solved via the cutoff method. Empirically, we show how to encode such applications as Array-Based Systems and verify them using existing model checkers. We demonstrate this approach on protocols for distributed mutual exclusion and collision avoidance.

We present the design, implementation, and verification of XMHF- an eXtensible and Modular Hypervisor Framework. XMHF is designed to achieve three goals -- modular extensibility, automated verification, and high performance. XMHF includes a core that provides functionality common to many hypervisor-based security architectures and supports extensions that augment the core with additional security or functional properties while preserving the fundamental hypervisor security property of memory integrity (i.e., ensuring that the hypervisor's memory is not modified by software running at a lower privilege level). We verify the memory integrity of the XMHF core -- 6018 lines of code -- using a combination of automated and manual techniques. The model checker CBMC automatically verifies 5208 lines of C code in about 80 seconds using less than 2GB of RAM. We manually audit the remaining 422 lines of C code and 388 lines of assembly language code that are stable and unlikely to change as development proceeds. Our experiments indicate that XMHF's performance is comparable to popular high-performance general-purpose hypervisors for the single guest that it supports.

In many industries, the importance of software components provided by third-party suppliers is steadily increasing. As the suppliers seek to secure their intellectual property (IP) rights, the customer usually has no direct access to the suppliers’ source code, and is able to enforce the use of verification tools only by legal requirements. In turn, the supplier has no means to convince the customer about successful verification without revealing the source code. This article presents an approach to resolve the conflict between the IP interests of the supplier and the quality interests of the customer. We introduce a protocol in which a dedicated server (called the “amanat”) is controlled by both parties: the customer controls the verification task performed by the amanat, while the supplier controls the communication channels of the amanat to ensure that the amanat does not leak information about the source code. We argue that the protocol is both practically useful and mathematically sound. As the protocol is based on well-known (and relatively lightweight) cryptographic primitives, it allows a straightforward implementation on top of existing verification tool chains. To substantiate our security claims, we establish the correctness of the protocol by cryptographic reduction proofs.

Consider non-preemptive fixed-priority scheduling of arbitrary-deadline sporadic tasks on a single processor assuming that the execution time of a job J depends on the actual schedule (sequence) of jobs executed before J. We present exact schedulability analysis for such a system.

The ability to identify semantically-related functions, in large collections of binary executables, is important for malware detection. Intuitively, two pieces of code are similar if they have the same effect on a machine's state. Current state-of-the-art tools employ a variety of pair wise comparisons (e.g., template matching using SMT solvers, Value-Set analysis at critical program points, API call matching, etc.) However, these methods are unshakable for clustering large datasets, of size N, since they require O(N2) comparisons. In this paper, we present an alternative approach based upon "hashing". We propose a scheme that captures the semantics of functions as semantic hashes. Our approach treats a function as a set of features, each of which represent the input-output behavior of a basic block. Using a form of locality-sensitive hashing known as Min Hashing, functions with many common features can be quickly identified, and the complexity of clustering is reduced to O(N). Experiments on functions extracted from the CERT malware catalog indicate that we are able to cluster closely related code with a low false positive rate.

Understanding, measuring, and leveraging the similarity of binaries (executable code) is a foundational challenge in software engineering. We present a notion of similarity based on provenance -- two binaries are similar if they are compiled from the same (or very similar) source code with the same (or similar) compilers. Empirical evidence suggests that provenance-similarity accounts for a significant portion of variation in existing binaries, particularly in malware. We propose and evaluate the applicability of classification to detect provenance-similarity. We evaluate a variety of classifiers, and different types of attributes and similarity labeling schemes, on two benchmarks derived from open-source software and malware respectively. We present encouraging results indicating that classification is a viable approach for automated provenance-similarity detection, and as an aid for malware analysts in particular.

The security of systems such as operating systems, hypervisors, and web browsers depend critically on reference monitors to correctly enforce their desired security policy in the presence of adversaries. Recent progress in developing reference monitors with small code size and narrow interfaces has made automated formal verification of reference monitors a more tractable goal. However, a significant remaining factor for the complexity of automated verification is the size of the data structures (e.g., access control matrices) over which the programs operate. This paper develops a parametric verification technique that scales even when reference monitors and adversaries operate over unbounded, but finite data structures. Specifically, we develop a parametric guarded command language for modeling reference monitors and adversaries. We also present a parametric temporal specification logic for expressing security policies that the monitor is expected to enforce. The central technical results of the paper are a set of small model theorems. These theorems state that in order to verify that a policy is enforced by a reference monitor with an arbitrarily large data structure, it is sufficient to model check the monitor with just one entry in its data structure. We apply our methodology to verify the designs of two hypervisors, SecVisor and the sHype mandatory-access-control extension to Xen. Our approach is able to prove that sHype and a variant of the original SecVisor design correctly enforces the expected security properties in the presence of powerful adversaries.

We present ASPIER - the first framework that combines software model checking with a standard protocol security model to automatically analyze authentication and secrecy properties of protocol implementations in C. The technical approach extends the iterative abstraction-refinement methodology for software model checking with a domain-specific protocol and symbolic attacker model. We have implemented the ASPIER tool and used it to verify authentication and secrecy properties of a part of an industrial strength protocol implementation - the handshake in OpenSSL - for configurations consisting of up to 3 servers and 3 clients. We have also implemented two distinct methods for reasoning about attacker message derivations, and evaluated them in the context of OpenSSL verification. ASPIER detected the "version-rollback" vulnerability in OpenSSL 0.9.6c source code and successfully verified the implementation when clients and servers are only willing to run SSL 3.0.

Boolean manipulation and existential quantification of numeric variables from linear arithmetic (LA) formulas is at the core of many program analysis and software model checking techniques (e.g., predicate abstraction). We present a new data structure, Linear Decision Diagrams (LDDs), to represent formulas in LA and its fragments, which has certain properties that make it efficient for such tasks. LDDs can be seen as an extension of Difference Decision Diagrams (DDDs) to full LA. Beyond this extension, we make three key contributions. First, we extend sifting-based dynamic variable ordering (DVO) from BDDs to LDDs. Second, we develop, implement, and evaluate several algorithms for existential quantification. Third, we implement LDDs inside CUDD, a state-of-the-art BDD package, and evaluate them on a large benchmark consisting of 850 functions derived from the source code of 25 open source programs. Overall, our experiments indicate that LDDs are an effective data structure for program analysis tasks.

Architecture evolution, a key aspect of software evolution, is typically done in an ad hoc manner, guided only by the competence of the architect performing it. This process lacks the rigor of an engineering discipline. In this paper, we argue that architecture evolution must be engineered - based on rational decisions that are supported by formal models and objective analyses. We believe that evolutions of a restricted form - close-ended evolution, where the starting and ending design points are known a priori - are amenable to being engineered. We discuss some of the key challenges in engineering close-ended evolution. We present a conceptual framework in which an architecture evolutionary trajectory is modeled as a sequence of steps, each captured by an operator. The goal of our framework is to support exploration and objective evaluation of different evolutionary trajectories. We conclude with open research questions in developing this framework.

Predicate (PA) and numeric (NA) abstractions are the two principal techniques for software analysis. In this paper, we develop an approach to couple the two techniques tightly into a unified framework via a single abstract domain called NumPredDom. In particular, we develop and evaluate four data structures that implement NumPredDom but differ in their expressivity and internal representation and algorithms. All our data structures combine BDDs (for efficient prepositional reasoning) with data structures for representing numerical constraints. Our technique is distinguished by its support for complex transfer functions that allow two way interaction between predicate and numeric information during state transformation. We have implemented a general framework for reachability analysis of C programs on top of our four data structures. Our experiments on non-trivial examples show that our proposed combination of PA and NA is more powerful and more efficient than either technique alone.

We extend the learning-based automated assume guarantee paradigm to perform compositional deadlock detection. We define failure automata, a generalization of finite automata that accept regular failure sets. We develop a learning algorithm LF that constructs the minimal deterministic failure automaton accepting any unknown regular failure set using a minimally adequate teacher. We show how LF can be used for compositional regular failure language containment, and deadlock detection, using non-circular and circular assume guarantee rules. We present an implementation of our techniques and encouraging experimental results on several non-trivial benchmarks

Abstract We present a framework for model checking concurrent software systems which incorporates both states and events. Contrary to other state/event approaches, our work also integrates two powerful verification techniques, counterexample-guided abstraction refinement and compositional reasoning. Our specification language is a state/event extension of linear temporal logic, and allows us to express many properties of software in a concise and intuitive manner. We show how standard automata-theoretic LTL model checking algorithms can be ported to our framework at no extra cost, enabling us to directly benefit from the large body of research on efficient LTL verification. We also present an algorithm to detect deadlocks in concurrent message-passing programs. Deadlock- freedom is not only an important and desirable property in its own right, but is also a prerequisite for the soundness of our model checking algorithm. Even though deadlock is inherently non-compositional and is not preserved by classical abstractions, our iterative algorithm employs both (non-standard) abstractions and compositional reasoning to alleviate the state-space explosion problem. The resulting framework differs in key respects from other instances of the counterexample-guided abstraction refinement paradigm found in the literature. We have implemented this work in the magic verification tool for concurrent C programs and performed tests on a broad set of benchmarks. Our experiments show that this new approach not only eases the writing of specifications, but also yields important gains both in space and in time during verification. In certain cases, we even encountered specifications that could not be verified using traditional pure event-based or state-based approaches, but became tractable within our state/event framework. We also recorded substantial reductions in time and memory consumption when performing deadlock-freedom checks with our new abstractions. Finally, we report two bugs (including a deadlock) in the source code of Micro-C/OS versions 2.0 and 2.7, which we discovered during our experiments.

MAGIC is a software verification project for C source code which verifies conformance of software components against statemachine specifications. To this aim, MAGIC extracts abstract software models using predicate abstraction, and resolves the inherent trade-off between model accuracy and scalability by an iterative abstraction refinement methodology. This paper presents the core principles implemented in the MAGIC verification engine, i.e. specification conformance using simulation and abstraction refinement. Viewing counterexamples as winning strategies in a simulation game between the implementation and the specification, we describe an algorithm where abstractions are refined on the basis of multiple winning strategies simultaneously. The refinement process is iterated until either a conformance with the specification is established, or a strategy to violate the specification is found to be realizable. In addition to the increase in expressiveness achieved by using simulation instead of trace containment, experimental results using OpenSSL indicate that our approach can lead to orders of magnitude improvement in verification time.

We present an algorithm to detect deadlocks in concurrent message-passing programs. Even though deadlock is inherently noncompositional and its absence is not preserved by standard abstractions, our framework employs both abstraction and compositional reasoning to alleviate the state space explosion problem. We iteratively construct increasingly more precise abstractions on the basis of spurious counterexamples to either detect a deadlock or prove that no deadlock exists. Our approach is inspired by the counterexample-guided abstraction refinement paradigm. However, our notion of abstraction as well as our schemes for verification and abstraction refinement differs in key respects from existing abstraction refinement frameworks. Our algorithm is also compositional in that abstraction, counterexample validation, and refinement are all carried out component-wise and do not require the construction of the complete state space of the concrete system under consideration. Finally, our approach is completely automated and provides diagnostic feedback in case a deadlock is detected. We have implemented our technique in the MAGIC verification tool and present encouraging results (up to 20 times speed-up in time and 4 times less memory consumption) with concurrent message-passing C programs. We also report a bug in the real-time operating system MicroC/OS version 2.70.

When a program violates its specification a model checker produces a counterexample that shows an example of undesirable behavior. It is up to the user to understand the error, locate it, and fix the problem. Previous work introduced a technique for explaining and localizing errors based on finding the closest execution to a counterexample, with respect to a distance metric. That approach was applied only to concrete executions of programs. This paper extends and generalizes the approach by combining it with predicate abstraction. Using an abstract state-space increases scalability and makes explanations more informative. Differences between executions are presented in terms of predicates derived from the specification and program, rather than specific changes to variable values. Reasoning to the cause of an error from the factthat in the failing run x < y, but in the successful execution x = y is easier than reasoning from the information that in the failing run y = 239, but in the successful execution y = 232. An abstract explanation is automatically generalized

We present a new methodology for automatic verification of C programs against finite state machine specifications. Our approach is compositional, naturally enabling us to decompose the verification of large software systems into subproblems of manageable complexity. The decomposition reflects the modularity in the software design. We use weak simulation as the notion of conformance between the program and its specification. Following the counterexample guided abstraction refinement (CEGAR) paradigm, our tool MAGIC first extracts a finite model from C source code using predicate abstraction and theorem proving. Subsequently, weak simulation is checked via a reduction to Boolean satisfiability. MAGIC has been interfaced with several publicly available theorem provers and SAT solvers. We report experimental results with procedures from the Linux kernel, the OpenSSL toolkit, and several industrial strength benchmarks.

We present a new methodology for automatic verification of C programs against finite state machine specifications. Our approach is compositional, naturally enabling us to decompose the verification of large software systems into subproblems of manageable complexity. The decomposition reflects the modularity in the software design. We use weak simulation as the notion of conformance between the program and its specification. Following the abstract-verify-refine paradigm, our tool MAGIC first extracts a finite model from C source code using predicate abstraction and theorem proving. Subsequently, simulation is checked via a reduction to Boolean satisfiability. MAGIC is able to interface with several publicly available theorem provers and SAT solvers. We report experimental results with procedures from the Linux kernel and the OpenSSL toolkit.

Abstraction and composition are the fundamental issues in making model checking viable for software. This paper proposes new techniques for automating abstraction and decomposition using source level type information provided by the programmer. Our system includes two novel components to achieve this end: (1) a behavioral type-and-effect system for the π-calculus, which extracts sound models as types, and (2) an assume-guarantee proof rule for carrying out compositional model checking on the types. Open simulation between CCS processes is used as both the subtyping relation in the type system and the abstraction relation for compositional model checking.We have implemented these ideas in a tool---PIPER. PIPER exploits type signatures provided by the programmer to partition the model checking problem, and emit model checking obligations that are discharged using the SPIN model checker. We present the details on applying PIPER on two examples: (1) the SIS standard for managing trouble tickets across multiple organizations and (2) a file reader from the pipelined implementation of a web server.

Implicit invocation or publish-subscribe has become an important architectural style for large-scale system design and evolution. The publish-subscribe style facilitates developing large-scale systems by composing separately developed components because the style permits loose coupling between various components. One of the major bottlenecks in using publish-subscribe systems for very large scale systems is the efficiency of filtering incoming messages, i.e., matching of published events with event subscriptions. This is a very challenging problem because in a realistic publish subscribe system the number of subscriptions can be large. We present an approach for matching published events with subscriptions which scales to a large number of subscriptions. Our approach uses binary decision diagrams, a compact data structure for representing Boolean functions which has been successfully used in verification techniques such as model checking. Experimental results clearly demonstrate the efficiency of our approach.