Code equivalence analysis is a critical problem in software engineering. In this paper, we focus on assessing if two code segments exhibit diverging behaviors. While symbolic analysis, exemplified by techniques like differential symbolic execution and impacted summaries, has been employed for equivalence analysis, it faces challenges due to limitations of symbolic execution, producing inconclusive results in many cases. To mitigate these limitations, we introduce a hybrid approach that integrates symbolic analysis with differential fuzzing. Differential fuzzing, although unable to prove equivalence like symbolic analysis, is valuable in identifying non-equivalent instances quickly. Our proposed hybrid approach leverages the strengths of symbolic reasoning and fuzzing within a single workflow for more effective analysis. The contributions of this paper include the introduction of a hybrid equivalence/non-equivalence testing approach, multiple heuristics for hybrid analysis, and differential fuzzing. Our experimental evaluation on multiple benchmarks including EQBench [1] and ARDiff [2], demonstrates that our proposed hybrid techniques can prove equivalence/non-equivalence for 28.52% more cases taking 43.21% less time on average compared to state-of-the-art symbolic execution based techniques.

As our lives, our businesses, and indeed our world economy become increasingly reliant on the secure operation of many interconnected software systems, the software engineering research community is faced with unprecedented research challenges, but also with exciting new opportunities. In this roadmap article, we outline our vision of software security analysis for the systems of the future. Given the recent advances in generative AI, we need new methods to assess and maximize the security of code co-written by machines. As our systems become increasingly heterogeneous, we need practical approaches that work even if some functions are automatically generated, e.g., by deep neural networks. As software systems depend evermore on the software supply chain, we need tools that scale to an entire ecosystem. What kind of vulnerabilities exist in future systems and how do we detect them? When all the shallow bugs are found, how do we discover vulnerabilities hidden deeply in the system? Assuming we cannot find all security flaws, how can we nevertheless protect our system? To answer these questions, we start our roadmap with a survey of recent advances in software security, then discuss open challenges and opportunities, and conclude with a long-term perspective for the field.

Equivalence analysis focuses on assessing whether different programs, or different versions of a program, exhibit identical behavior. While extensive research has been done on equivalence analysis, there is a lack of detailed and quantitative reasoning techniques for non-equivalence. In this paper we introduce quantitative symbolic non-equivalence analysis and evaluate its effectiveness on the EqBench [3] benchmark (the largest available benchmark for equivalence analysis), and demonstrate how it can be used for reasoning about the non-equivalence of different versions of C programs.

Since its major release in 2006, the Unified Extensible Firmware Interface (UEFI) has become the industry standard for interfacing a computer's hardware and operating system, replacing BIOS. UEFI has higher privileged security access to system resources than any other software component, including the system kernel. Hence, identifying and characterizing vulnerabilities in UEFI is extremely important for computer security. However, automated detection and characterization of UEFI vulnerabilities is a challenging problem. Static vulnerability analysis techniques are scalable but lack precision (reporting many false positives), whereas symbolic analysis techniques are precise but are hampered by scalability issues due to path explosion and the cost of constraint solving. In this paper, we introduce a technique called STatic Analysis guided Symbolic Execution (STASE), which integrates both analysis approaches to leverage their strengths and minimize their weaknesses. We begin with a rule-based static vulnerability analysis on LLVM bitcode to identify potential vulnerability targets for symbolic execution. We then focus symbolic execution on each target to achieve precise vulnerability detection and signature generation. STASE relies on the manual specification of reusable vulnerability rules and attacker-controlled inputs. However, it automates the generation of harnesses that guide the symbolic execution process, addressing the usability and scalability of symbolic execution, which typically requires manual harness generation to reduce the state space. We implemented and applied STASE to the implementations of UEFI code base. STASE detects and generates vulnerability signatures for 5 out of 9 recently reported PixieFail vulnerabilities and 13 new vulnerabilities in Tianocore's EDKII codebase.

With the growing prevalence of cloud computing, providing secure access to information stored in the cloud has become a critical problem. Due to the complexity of access control policies, administrators may inadvertently allow unintended access to private information, and this is a common source of data breaches in cloud based services. In this paper, we present a quantitative symbolic analysis approach for automated policy repair in order to fix overly permissive policies. We encode the semantics of the access control policies using SMT formulas and assess their permissiveness using model counting. Given a policy, a permissiveness bound, and a set of requests that should be allowed, we iteratively repair the policy through permissiveness reduction and refinement, so that the permissiveness bound is reached while the given set of requests are still allowed. We demonstrate the effectiveness of our automated policy repair technique by applying it to policies written in Amazon's AWS Identity and Access Management (IAM) policy language.

Starting with a random initial seed, fuzzers search for inputs that trigger bugs or vulnerabilities. However, fuzzers often fail to generate inputs for program paths guarded by restrictive branch conditions. In this paper, we show that by first identifying rare-paths in programs (i.e., program paths with path constraints that are unlikely to be satisfied by random input generation), and then, generating inputs/seeds that trigger rare-paths, one can improve the coverage of fuzzing tools. In particular, we present techniques 1) that identify rare paths using quantitative symbolic analysis, and 2) generate inputs that can explore these rare paths using path-guided concolic execution. We provide these inputs as initial seed sets to three state of the art fuzzers. Our experimental evaluation on a set of programs shows that the fuzzers achieve better coverage with the rare-path based seed set compared to a random initial seed.

Information leaks are a significant problem in modern software systems. In recent years, information theoretic concepts, such as Shannon entropy, have been applied to quantifying information leaks in programs. One recent approach is to use symbolic execution together with model counting constraints solvers in order to quantify information leakage. There are at least two reasons for unsoundness in quantifying information leakage using this approach: 1) Symbolic execution may not be able to explore all execution paths, 2) Model counting constraints solvers may not be able to provide an exact count. We present a sound symbolic quantitative information flow analysis that bounds the information leakage both for the cases where the program behavior is not fully explored and the model counting constraint solver is unable to provide a precise model count but provides an upper and a lower bound. We implemented our approach as an extension to KLEE for computing sound bounds for information leakage in C programs.

Due to ubiquitous use of software services, protecting the confidentiality of private information stored in compute clouds is becoming an increasingly critical problem. Although access control specification languages and libraries provide mechanisms for protecting confidentiality of information, without verification and validation techniques that can assist developers in writing policies, complex policy specifications are likely to have errors that can lead to unintended and unauthorized access to data, possibly with disastrous consequences. In this paper, we present a quantitative and differential policy analysis framework that not only identifies if one policy is more permissive than another policy, but also quantifies the relative permissiveness of access control policies. We quantify permissiveness of policies using a model counting constraint solver. We present a heuristic that transforms constraints extracted from access control policies and significantly improves the model counting performance. We demonstrate the effectiveness of our approach by applying it to policies written in Amazon's AWS Identity and Access Management (IAM) policy language and Microsoft's Azure policy language.

We present a heuristic for approximating the likelihood of reaching a given program statement using 1) branch selectivity (representing the percentage of values that satisfy a branch condition), which we compute using model counting, 2) dependency analysis, which we use to identify input-dependent branch conditions that influence statement reachability, 3) abstract interpretation, which we use to identify the set of values that reach a branch condition, and 4) a discrete-time Markov chain model, which we construct to capture the control flow structure of the program together with the selectivity of each branch. Our experiments indicate that our heuristic-based probabilistic reachability analysis tool PReach can identify hard to reach statements with high precision and accuracy in benchmarks from software verification and testing competitions, Apache Commons Lang, and the DARPA STAC program. We provide a detailed comparison with probabilistic symbolic execution and statistical symbolic execution for the purpose of identifying hard to reach statements. PReach achieves comparable precision and accuracy to both probabilistic and statistical symbolic execution for bounded execution depth and better precision and accuracy when execution depth is unbounded and the number of program paths grows exponentially. Moreover, PReach is more scalable than both probabilistic and statistical symbolic execution.

quacky is a tool for quantifying permissiveness of access control policies in the cloud. Given a policy, quacky translates it into a SMT formula and uses a model counting constraint solver to quantify permissiveness. When given multiple policies, quacky not only determines which policy is more permissive, but also quantifies the relative permissiveness between the policies. With quacky, policy authors can automatically analyze complex policies, helping them ensure that there is no unintended access to private data. quacky supports access control policies written in the Amazon Web Services (AWS) Identity and Access Management (IAM), Microsoft Azure, and Google Cloud Platform (GCP) policy languages. It has command-line and web interfaces. It is open-source and available at https://github.com/vlab-cs-ucsb/quacky.

Mobile applications, Internet of Things devices and web services are pervasive and they all encrypt the communications between servers and clients to not have information leakages. While the network traffic is encrypted, packet sizes and timings are still visible to an eavesdropper and these properties can leak information and sacrifice user privacy. We present TSA, a black box network side-channel analysis tool which detects and quantifies side-channel information leakages. TSA provides the users with the means to automate trace gathering by providing a framework in which the users can write mutators for the inputs to the system under analysis. TSA can also take as input traces directly for analysis if the user prefers to gather them separately. TSA is open-source and available as a Python package and a command-line tool. TSA demo, tool and benchmarks are available at https://github.com/kadron/tsa-tool.

Browsers use security policies to block malicious behaviors. Cross-Origin Read Blocking (CORB) is a browser security policy for preventing side-channel attacks such as Spectre. We propose a web browser security policy fuzzer called CorbFuzz for checking CORB and similar policies. In implementing a security policy, the browser only has access to HTTP requests and responses, and takes policy actions based solely on those interactions. In checking the browser security policies, CorbFuzz uses a policy oracle that tracks the web application behavior and infers the desired policy action based on the web application state. By comparing the policy oracle with the browser behavior, CorbFuzz detects weaknesses in browser security policies. CorbFuzz checks the web browser policy by fuzzing a set of web applications where the state-related queries are symbolically evaluated for increased coverage and automation. CorbFuzz collects type information from database queries and branch conditions in order to prevent the generation of inconsistent data values during fuzzing. We evaluated CorbFuzz on CORB implementations of Chromium and Webkit, and Opaque Response Blocking (ORB) policy implementation of Firefox using web applications collected from GitHub. We found three classes of weaknesses in Chromium’s implementation of CORB.

Timing side channels arise in software when a program's execution time can be correlated with security-sensitive program input. Recent results on software side-channel detection focus on analysis of program's source code. However, runtime behavior, in particular optimizations introduced during just-in-time (JIT) compilation, can impact or even introduce timing side channels in programs. In this paper, we present a technique for automatically detecting such JIT-induced timing side channels in Java programs. We first introduce patterns to detect partitions of secret input potentially separable by side channels. Then we present an automated approach for exploring behaviors of the Java Virtual Machine (JVM) to identify states where timing channels separating these partitions arise. We evaluate our technique on three datasets used in recent work on side-channel detection. We find that many code variants labeled "safe" with respect to side-channel vulnerabilities are in fact vulnerable to JIT-induced timing side channels. Our results directly contradict the conclusions of four separate state-of-the-art program analysis tools for side-channel detection and demonstrate that JIT-induced side channels are prevalent and can be detected automatically.

Information leakage in software systems is a problem of growing importance. Networked applications can leak sensitive information even when they use encryption. For example, some characteristics of network packets, such as their size, timing and direction, are visible even for encrypted traffic. Patterns in these characteristics can be leveraged as side channels to extract information about secret values accessed by the application. In this paper, we present a new tool called AutoFeed for detecting and quantifying information leakage due to side channels in networked software applications. AutoFeed profiles the target system and automatically explores the input space, explores the space of output features that may leak information, quantifies the information leakage, and identifies the top-leaking features. Given a set of input mutators and a small number of initial inputs provided by the user, AutoFeed iteratively mutates inputs and periodically updates its leakage estimations to identify the features that leak the greatest amount of information about the secret of interest. AutoFeed uses a feedback loop for incremental profiling, and a stopping criterion that terminates the analysis when the leakage estimation for the top-leaking features converges. AutoFeed also automatically assigns weights to mutators in order to focus the search of the input space on exploring dimensions that are relevant to the leakage quantification. Our experimental evaluation on the benchmarks shows that AutoFeed is effective in detecting and quantifying information leaks in networked applications.

Side-channel vulnerabilities in software are caused by an observable imbalance in resource usage across different program paths. We show that just-in-time (JIT) compilation, which is crucial to the runtime performance of modern interpreted languages, can introduce timing side channels in cases where the input distribution to the program is non-uniform. Such timing channels can enable an attacker to infer potentially sensitive information about predicates on the program input.We define three attack models under which such side channels are harnessable and five vulnerability templates to detect susceptible code fragments and predicates. We also propose profiling algorithms to generate the representative statistical information necessary for the attacker to perform accurate inference.We systematically evaluate the strength of these JIT-based side channels on the java.lang.String, java.lang.Math, and java.math.BigInteger classes from the Java standard library, and on the JavaScript built-in objects String, Math, and Array. We carry out our evaluation using two widely adopted, open-source, JIT-enhanced runtime engines for the Java and JavaScript languages: the Oracle HotSpot Java Virtual Machine and the Google V8 JavaScript engine, respectively.Finally, we demonstrate a few examples of JIT-based side channels in the Apache Shiro security framework and the GraphHopper route planning server, and show that they are observable over the public Internet.

Quantitative program analysis is an emerging area with applications to software reliability, quantitative information flow, side-channel detection and attack synthesis. Most quantitative program analysis techniques rely on model counting constraint solvers, which are typically the bottleneck for scalability. Although the effectiveness of formula caching in expediting expensive model-counting queries has been demonstrated in prior work, our key insight is that many subformulas are shared across non-identical constraints generated during program analyses. This has not been utilized by prior formula caching approaches. In this paper we present a subformula caching framework and integrate it into a model counting constraint solver. We experimentally evaluate its effectiveness under three quantitative program analysis scenarios: 1) model counting constraints generated by symbolic execution, 2) reliability analysis using probabilistic symbolic execution, 3) adaptive attack synthesis for side-channels. Our experimental results demonstrate that our subformula caching approach significantly improves the performance of quantitative program analysis.

We present an automated technique for synthesizing adaptive attacks to extract information from program functions that leak secret data through a side channel. We synthesize attack steps dynamically and consider noisy program environments. Our approach consists of an offline profiling phase using symbolic execution, witness generation, and profiling to construct a noise model. During our online attack synthesis phase, we use weighted model counting and numeric optimization to automatically synthesize attack inputs. We experimentally evaluate the effectiveness of our approach on DARPA benchmark programs created for testing side-channel analysis techniques.

Side-channels in software are an increasingly significant threat to the confidentiality of private user information, and the static detection of such vulnerabilities is a key challenge in secure software development. In this paper, we introduce a new technique for scalable detection of side- channels in software. Given a program and a cost model for a side-channel (such as time or memory usage), we decompose the control flow graph of the program into nested branch and loop components, and compositionally assign a symbolic cost expression to each component. Symbolic cost expressions provide an over-approximation of all possible observable cost values that components can generate. Queries to a satisfiability solver on the difference between possible cost values of a component allow us to detect the presence of imbalanced paths (with respect to observable cost) through the control flow graph. When combined with taint analysis that identifies conditional statements that depend on secret information, our technique answers the following question: Does there exist a pair of paths in the program's control flow graph, differing only on branch conditions influenced by the secret, that differ in observable side-channel value by more than some given threshold? Additional optimization queries allow us to identify the minimal number of loop iterations necessary for the above to hold or the maximal cost difference between paths in the graph. We perform symbolic execution based feasibility analyses to eliminate control flow paths that are infeasible. We implemented our techniques in a prototype, and we demonstrate its favourable performance against state-of-the-art tools as well as its effectiveness and scalability on a set of sizable, realistic Java server-client and peer-to-peer applications.

Recently, symbolic program analysis techniques have been extended to quantitative analyses using model counting constraint solvers. Given a constraint and a bound, a model counting constraint solver computes the number of solutions for the constraint within the bound. We present a parameterized model counting constraint solver for string and numeric constraints. We first construct a multi-track deterministic finite state automaton that accepts all solutions to the given constraint. We limit the numeric constraints to linear integer arithmetic, and for non-regular string constraints we over-approximate the solution set. Counting the number of accepting paths in the generated automaton solves the model counting problem. Our approach is parameterized in the sense that, we do not assume a finite domain size during automata construction, resulting in a potentially infinite set of solutions, and our model counting approach works for arbitrarily large bounds. We experimentally demonstrate the effectiveness of our approach on a large set of string and numeric constraints extracted from software applications. We experimentally compare our tool to five existing model counting constraint solvers for string and numeric constraints and demonstrate that our tool is as efficient and as or more precise than other solvers. Moreover, our tool can handle mixed constraints with string and integer variables that no other tool can.

We present symbolic analysis techniques for detecting vulnerabilities that are due to adaptive side-channel attacks, and synthesizing inputs that exploit the identified vulnerabilities. We start with a symbolic attack model that encodes succinctly all the side-channel attacks that an adversary can make. Using symbolic execution over this model, we generate a set of mathematical constraints, where each constraint characterizes the set of secret values that lead to the same sequence of side-channel measurements. We then compute the optimal attack, i.e, the attack that yields maximum leakage over the secret, by solving an optimization problem over the computed constraints. We use information-theoretic concepts such as channel capacity and Shannon entropy to quantify the leakage over multiple runs in the attack, where the measurements over the side channels form the observations that an adversary can use to try to infer the secret. We also propose greedy heuristics that generate the attack by exploring a portion of the symbolic attack model in each step. We implemented the techniques in Symbolic PathFinder and applied them to Java programs encoding web services, string manipulations and cryptographic functions, demonstrating how to synthesize optimal side-channel attacks.

Modern web applications use complex data models and access control rules which lead to data integrity and access control errors. One approach to find such errors is to use formal verification techniques. However, as a first step, most formal verification techniques require extraction of a formal model which is a difficult problem in itself due to dynamic features of modern languages, and it is typically done either manually, or using ad hoc techniques. In this paper, we present a technique called symbolic model extraction for extracting formal data models from web applications. The key ideas of symbolic model extraction are 1) to use the source language interpreter for model extraction, which enables us to handle dynamic features of the language, 2) to use code instrumentation so that execution of each instrumented piece of code returns the formal model that corresponds to that piece of code, 3) to instrument the code dynamically so that the models of methods that are created at runtime can also be extracted, and 4) to execute both sides of branches during instrumented execution so that all program behaviors can be covered in a single instrumented execution. We implemented the symbolic model extraction technique for the Rails framework and used it to extract data and access control models from web applications. Our experiments demonstrate that symbolic model extraction is scalable and extracts formal models that are precise enough to find bugs in real-world applications without reporting too many false positives.

Symbolic program analysis techniques rely on satisfiability-checking constraint solvers, while quantitative program analysis techniques rely on model-counting constraint solvers. Hence, the efficiency of satisfiability checking and model counting is crucial for efficiency of modern program analysis techniques. In this paper, we present a constraint caching framework to expedite potentially expensive satisfiability and model-counting queries. Integral to this framework is our new constraint normalization procedure under which the cardinality of the solution set of a constraint, but not necessarily the solution set itself, is preserved. We extend these constraint normalization techniques to string constraints in order to support analysis of string-manipulating code. A group-theoretic framework which generalizes earlier results on constraint normalization is used to express our normalization techniques. We also present a parameterized caching approach where, in addition to storing the result of a model-counting query, we also store a model-counter object in the constraint store that allows us to efficiently recount the number of satisfying models for different maximum bounds. We implement our caching framework in our tool Cashew, which is built as an extension of the Green caching framework, and integrate it with the symbolic execution tool Symbolic PathFinder (SPF) and the model-counting constraint solver ABC. Our experiments show that constraint caching can significantly improve the performance of symbolic and quantitative program analyses. For instance, Cashew can normalize the 10,104 unique constraints in the SMC/Kaluza benchmark down to 394 normal forms, achieve a 10x speedup on the SMC/Kaluza-Big dataset, and an average 3x speedup in our SPF-based side-channel analysis experiments.

A crucial problem in software security is the detection of side-channels. Information gained by observing non-functional properties of program executions (such as execution time or memory usage) can enable attackers to infer secret information (such as a password). In this talk, I will discuss how symbolic execution, combined with a model counting constraint solver, can be used for quantifying side-channel leakage in Java programs. In addition to computing information leakage for a single run of a program, I will also discuss computation of information leakage for multiple runs for a type of side channels called segmented oracles. In segmented oracles, the attacker is able to explore each segment of a secret (for example each character of a password) independently. For segmented oracles, it is possible to compute information leakage for multiple runs using only the path constraints generated from a single run symbolic execution. These results have been implemented as an extension to the symbolic execution tool Symbolic Path Finder (SPF) using the SMT solver Z3 and two model counting constraint solvers LattE and ABC.

We present a code- and input-sensitive sanitization synthesis approach for repairing string vulnerabilities that are common in web applications. The synthesized sanitization patch modifies the user input in an optimal way while guaranteeing that the repaired web application is not vulnerable. Given a web application, an input pattern and an attack pattern, we use automata-based static string analysis techniques to compute a sanitization signature that characterizes safe input values that obey the given input pattern and are safe with respect to the given attack pattern. Using the sanitization signature, we synthesize an optimal sanitization patch that converts malicious user inputs to benign ones with minimal editing. When the generated patch is added to the web application, it is guaranteed that the repaired web application is no longer vulnerable. We present refinements to previous sanitization synthesis algorithms that reduce the runtime sanitization cost significantly. We evaluate our approach on open source web applications using common input and attack patterns, demonstrating the effectiveness of our approach.

Access control bugs in web applications can have dire consequences since many web applications store private and sensitive data. In this paper we present an automated verification technique for access control in Ruby on Rails (Rails) applications. Our technique starts by automatically extracting a model that captures 1) the ways the data is accessed and modified by the application, 2) the access control policy of the application, and 3) the authorization checks used for access control policy enforcement. Then, it automatically translates this model to first order logic and uses automated theorem provers to check whether the declared access control policy is correctly enforced by the implementation. We implemented our technique in a tool called CanCheck. Using CanCheck on open source Rails applications, we found numerous previously unknown exploitable access control bugs as well as several deficiencies in access control policies.

We present an automated approach for detecting and quantifying side channels in Java programs, which uses symbolic execution, string analysis and model counting to compute information leakage for a single run of a program. We further extend this approach to compute information leakage for multiple runs for a type of side channels called segmented oracles, where the attacker is able to explore each segment of a secret (for example each character of a password) independently. We present an efficient technique for segmented oracles that computes information leakage for multiple runs using only the path constraints generated from a single run symbolic execution. Our implementation uses the symbolic execution tool Symbolic PathFinder (SPF), SMT solver Z3, and two model counting constraint solvers LattE and ABC. Although LattE has been used before for analyzing numeric constraints, in this paper, we present an approach for using LattE for analyzing string constraints. We also extend the string constraint solver ABC for analysis of both numeric and string constraints, and we integrate ABC in SPF, enabling quantitative symbolic string analysis.

Modern applications use back-end data stores for persistent data. Automated verification of the code that updates the data store would prevent bugs that can cause loss or corruption of data. In this paper, we focus on the most challenging part of this problem: automated verification of code that updates the data store and contains loops. Due to dependencies between loop iterations, verification of code that contains loops is a hard problem, and typically requires manual assistance in the form of loop invariants. We present a fully automated technique that improves verifiability of loops. We first define co execution, a method for modeling loop iterations that simplifies automated reasoning about loops. Then, we present a fully automated static program analysis that detects whether the behavior of a given loop can be modeled using co execution. We provide a customized verification technique for co executable loops that results in more effective verification. In our experiments we observed that, in 45% of cases, modeling loops using co execution reduces verification time between 1 and 4 orders of magnitude. In addition, the rate of inconclusive verification results in the presence of loops is reduced from 65% down to 24%, all without requiring loop invariants or any manual intervention.

Misuse or loss of web application data can have catastrophic consequences in today's Internet oriented world. Hence, verification of web application data models is of paramount importance. We have developed a framework for verification of web application data models via translation to First Order Logic (FOL), followed by automated theorem proving. Due to the undecidability of FOL, this automated approach does not always produce a conclusive answer. In this paper, we investigate the use of many-sorted logic in data model verification in order to improve the effectiveness of this approach. Many-sorted logic allows us to specify type information explicitly, thus lightening the burden of reasoning about type information during theorem proving. Our experiments demonstrate that using many-sorted logic improves the verification performance significantly, and completely eliminates inconclusive results in all cases over 7 real world web applications, down from an 17% inconclusive rate.

Recent automated software testing techniques concentrate on achieving path coverage. We present a complexity measure that provides an upper bound for the number of paths in a program, and hence, can be used for assessing the difficulty of achieving path coverage for a given method. We define the path complexity of a program as a function that takes a depth bound as input and returns the number of paths in the control flow graph that are within that bound. We show how to automatically compute the path complexity function in closed form, and the asymptotic path complexity which identifies the dominant term in the path complexity function. Our results demonstrate that path complexity can be computed efficiently, and it is a better complexity measure for path coverage compared to cyclomatic complexity and NPATH complexity.

Most software systems nowadays are Web-based applications that are deployed over compute clouds using a three-tier architecture, where the persistent data for the application is stored in a backend datastore and is accessed and modified by the server-side code based on the user interactions at the client-side. The data model forms the foundation of these three tiers, and identifies the sets of objects (object classes) and the relations among them (associations among object classes) stored by the application. In this article, we present a set of property patterns to specify properties of a data model, as well as several heuristics for automatically inferring them. We show that the specified or inferred data model properties can be automatically verified using bounded and unbounded verification techniques. For the properties that fail, we present techniques that generate fixes to the data model that establish the failing properties. We implemented this approach for Web applications built using the Ruby on Rails framework and applied it to ten open source applications. Our experimental results demonstrate that our approach is effective in automatically identifying and fixing errors in data models of real-world web applications.

As scalable information technology evolves to a more cloud-like model, digital assets (code, data and software environments) increasingly require curation as web-accessible services. "Service-izing" digital assets consists of encapsulating assets in software that exposes them to web and mobile applications via well-defined yet flexible, network accessible, application programming interfaces (APIs). In this paper, we postulate that recent advances in cloud computing make cloud platforms as-a-service (PaaS) ideal for deployment, lifecycle management, and policy-based control i.e. API governance - for extant and future digital assets. Toward this end, we overview API governance as a PaaS technology and outline some early results generated by our investigation of a prototype we are developing, called EAGER, for implementing API governance at scale.

Modern software applications store their data in remote cloud servers. Users interact with these applications using web browsers or thin clients running on mobile devices. A key issue in dependability of these applications is the correctness of the actions that update the data store, which are triggered by user requests. In this paper, we present techniques for au- tomatically checking if the actions of an application preserve the data model invariants. Our approach first automatically extracts a data model specification, which we call an abstract data store, from a given application using instrumented exe- cution. The abstract data store identifies the sets of objects and relations (associations) used by the application, and the actions that update the data store by deleting or creating objects or by changing the relations among the objects. We show that checking invariants of an abstract data store corre- sponds to inductive invariant verification, and can be done using a mapping to First Order Logic (FOL) and using a FOL theorem prover. We implemented this approach for the Rails framework and applied it to three open source applications. We found four previously unknown bugs and reported them to the developers, who confirmed and imme- diately fixed two of them.

Web applications need to validate and sanitize user inputs in order to avoid attacks such as Cross Site Scripting (XSS) and SQL Injection. Writing string manipulation code for input validation and sanitization is an error-prone process leading to many vulnerabilities in real-world web applications. Automata-based static string analysis techniques can be used to automatically compute vulnerability signatures (represented as automata) that characterize all the inputs that can exploit a vulnerability. However, there are several factors that limit the applicability of static string analysis techniques in general: 1) undesirability of static string analysis requires the use of approximations leading to false positives, 2) static string analysis tools do not handle all string operations, 3) dynamic nature of the scripting languages makes static analysis difficult. In this paper, we show that vulnerability signatures computed for deliberately insecure web applications (developed for demonstrating different types of vulnerabilities) can be used to generate test cases for other applications. Given a vulnerability signature represented as an automaton, we present algorithms for test case generation based on state, transition, and path coverage. These automatically generated test cases can be used to test applications that are not analyzable statically, and to discover attack strings that demonstrate how the vulnerabilities can be exploited.

Correct validation and sanitization of user input is crucial in web applications for avoiding security vulnerabilities and erroneous application behavior. We present an automated differential repair technique for input validation and sanitization functions. Differential repair can be used within an application to repair client and server-side code with respect to each other, or across applications in order to strengthen the validation and sanitization checks. Given a reference and a target function, our differential repair technique strengthens the validation and sanitization operations in the target function based on the reference function. It does this by synthesizing three patches: a validation, a length, and a sanitization patch. Our automated patch synthesis algorithms are based on forward and backward symbolic string analyses that use automata as a symbolic representation. Composition of the three automatically synthesized patches with the original target function results in the repaired function, which provides stronger validation and sanitization than both the target and the reference functions.

Asynchronous communication requires message queues to store the messages that are yet to be consumed. Verification of interactions in asynchronously communicating systems is challenging since the sizes of these queues can grow arbitrarily large during execution. In fact, behavioral models for asynchronously communicating systems typically have infinite state spaces, which makes many analysis and verification problems undecidable. In this paper, we show that, focusing only on the interaction behavior (modeled as the global sequence of messages that are sent, recorded in the order they are sent) results in decidable verification for a class of asynchronously communicating systems. In particular, we present the necessary and sufficient condition under which asynchronously communicating systems with unbounded queues exhibit interaction behavior that is equivalent to their interactions over finitely bounded queues. We show that this condition can be automatically checked, ensuring existence of a finite bound on the queue sizes, and, we show that, the finite bound on the queue sizes can be automatically computed.

Nowadays many software applications are deployed over compute clouds using the three-tier architecture, where the persistent data for the application is stored in a backend datastore and is accessed and modified by the server-side code based on the user interactions at the client-side. The data model forms the foundation of these three tiers, and identifies the set of objects stored by the application and the relations (associations) among them. In this paper, we present techniques for automatically inferring properties about the data model by analyzing the relations among the object classes. We then check the inferred properties with respect to the semantics of the data model using automated verification techniques. For the properties that fail, we present techniques that generate fixes to the data model that establish the inferred properties. We implemented this approach for web applications built using the Ruby on Rails framework and applied it to five open source applications. Our experimental results demonstrate that our approach is effective in automatically identifying and fixing errors in data models of real-world web applications.

Client-side computation in web applications is becoming increasingly common due to the popularity of powerful client-side programming languages such as JavaScript. Clientside computation is commonly used to improve an application's responsiveness by validating user inputs before they are sent to the server. In this paper, we present an analysis technique for checking if a client-side input validation function conforms to a given policy. In our approach, input validation policies are expressed using two regular expressions, one specifying the maximum policy (the upper bound for the set of inputs that should be allowed) and the other specifying the minimum policy (the lower bound for the set of inputs that should be allowed). Using our analysis we can identify two types of errors 1) the input validation function accepts an input that is not permitted by the maximum policy, or 2) the input validation function rejects an input that is permitted by the minimum policy. We implemented our analysis using dynamic slicing to automatically extract the input validation functions from web applications and using automata-based string analysis to analyze the extracted functions. Our experiments demonstrate that our approach is effective in finding errors in input validation functions that we collected from real-world applications and from tutorials and books for teaching JavaScript.

Since web applications are easily accessible, and often store a large amount of sensitive user information, they are a common target for attackers. In particular, attacks that focus on input validation vulnerabilities are extremely effective and dangerous. To address this problem, we developed ViewPoints--a technique that can identify erroneous or insufficient validation and sanitization of the user inputs by automatically discovering inconsistencies between client- and server-side input validation functions. Developers typically perform redundant input validation in both the front-end (client) and the back-end (server) components of a web application. Client- side validation is used to improve the responsiveness of the application, as it allows for responding without communicating with the server, whereas server-side validation is necessary for security reasons, as malicious users can easily circumvent client-side checks. ViewPoints (1) automatically extracts client- and server-side input validation functions, (2) models them as deterministic finite automata (DFAs), and (3) compares client- and server-side DFAs to identify and report the inconsistencies between the two sets of checks. Our initial evaluation of the technique is promising: when applied to a set of real-world web applications, ViewPoints was able to automatically identify a large number of inconsistencies in their input validation functions.

The growing influence of web applications in every aspect of society makes their dependability an immense concern. A fundamental building block of web applications that use the Model-View-Controller (MVC) pattern is the data model, which specifies the object classes and the relations among them. We present an approach for unbounded, automated verification of data models that 1) extracts a formal data model from an Object Relational Mapping, 2) converts verification queries about the data model to queries about the satisfiability of formulas in the theory of uninterpreted functions, and 3) uses a Satisfiability Modulo Theories (SMT) solver to check the satisfiability of the resulting formulas. We implemented this approach and applied it to five open-source Rails applications. Our results demonstrate that the proposed approach is feasible, and is more efficient than SAT-based bounded verification.

Since software systems are becoming increasingly more concurrent and distributed, modeling and analysis of interactions among their components is a crucial problem. In several application domains, message-based communication is used as the interaction mechanism, and the communication contract among the components of the system is specified semantically as a state machine. In the service-oriented computing domain such communication contracts are called "choreography" specifications. A choreography specification identifies allowable ordering of message exchanges in a distributed system. A fundamental question about a choreography specification is determining its realizability, i.e., given a choreography specification, is it possible to build a distributed system that communicates exactly as the choreography specifies? Checking realizability of choreography specifications has been an open problem for several years and it was not known if this was a decidable problem. In this paper we give necessary and sufficient conditions for realizability of choreographies. We implemented the proposed realizability check and our experiments show that it can efficiently determine the realizability of 1) web service choreographies, 2) Singularity OS channel contracts, and 3) UML collaboration (communication) diagrams.

Service-oriented computing has emerged as a new software development paradigm that enables implementation of Web accessible software systems that are composed of distributed services which interact with each other via exchanging messages. Modeling and analysis of interactions among services is a crucial problem in this domain. Interactions among a set of services that participate in a service composition can be described from a global point of view as a choreography. Choreographies can be specified using specification languages such as Web Services Choreography Description Language (WS-CDL) and visualized using graphical formalisms such as collaboration diagrams. In this paper, we present an encoding of collaboration diagrams into the LOTOS process algebra for choreography analysis. This encoding allows us to (1) check the temporal properties of choreographies using a LOTOS verification tool set called the Construction and Analysis of Distributed Processes (CADP) toolbox, (2) check the realizability of choreographies for both synchronous communication and bounded asynchronous communication, and (3) automate the peer generation process. Realizability indicates whether peers can be generated from a given choreography specification in such a way that the interactions of the generated peers exactly match the choreography specification. If a collaboration diagram is unrealizable, our approach extends the peer generation process by adding extra communication that guarantees that the peers behave according to the choreography specification.

We present automata-based static string analysis techniques that automatically generate sanitization statements for patching vulnerable web applications. Our approach consists of three phases: Given an attack pattern we first conduct a vulnerability analysis to identify if strings that match the attack pattern can reach the security-sensitive functions. Next, we compute vulnerability signatures that characterize all input strings that can exploit the discovered vulnerability. Given the vulnerability signatures, we then construct sanitization statements that 1) check if a given input matches the vulnerability signature and 2) modify the input in a minimal way so that the modified input does not match the vulnerability signature. Our approach is capable of generating relational vulnerability signatures (and corresponding sanitization statements) for vulnerabilities that are due to more than one input.

The use of scripting languages to build web applications has increased programmer productivity, but at the cost of degrading dependability. In this paper we focus on a class of bugs that appear in web applications that are built based on the Model-View-Controller architecture. Our goal is to automatically discover data model errors in Ruby on Rails applications. To this end, we created an automatic translator that converts data model expressions in Ruby on Rails applications to formal specifications. In particular, our translator takes Active Records specifications (which are used to specify data models in Ruby on Rails applications) as input and generates a data model in Alloy language as output. We then use bounded verification techniques implemented in the Alloy Analyzer to look for errors in these formal data model specifications. We applied our approach to two open source web applications to demonstrate its feasibility.

Choreography analysis has been a crucial problem in service oriented computing. Interactions among services involve message exchanges across organizational boundaries in a distributed computing environment, and in order to build such systems in a reliable manner, it is necessary to develop techniques for analyzing such interactions. Choreography conformance involves verifying that a set of services behave according to a given choreography specification that characterizes their interactions. Unfortunately this is an undecidable problem when services interact with asynchronous communication. In this paper we present techniques that identify if the interaction behavior for a set of services remain the same when asynchronous communication is replaced with synchronous communication. This is called the synchronizability problem and determining the synchronizability of a set of services has been an open problem for several years. We solve this problem in this paper. Our results can be used to identify synchronizable services for which choreography conformance can be checked efficiently. Our results on synchronizability are applicable to any software infrastructure that supports message-based interactions.

The enforcement of navigation constraints in web applications is challenging and error prone due to the unrestricted use ofnavigation functions inweb browsers. This often leads to navigation errors, producing cryptic messages and exposinginformation thatcanbeexploitedbymalicious users. We propose a runtime enforcement mechanism that restricts the control flow of a web application to a state machine model specified by the developer, and use model checking to verify temporal properties on these state machines. Our experiments, performed on three real-world applications, show that 1) our runtime enforcement mechanism incurs negligible overhead under normal circumstances, and can even reduceserverprocessingtimeinhandlingunexpectedrequests; 2) by combining runtime enforcement with model checking, navigation correctness can be efficiently guaranteed in large web applications.

We present a modular approach for verification of synchronization behavior in concurrent programs that use reentrant locks. Our approach decouples the verification of the lock implementation from the verification of the threads that use the lock. This decoupling is achieved using lock interfaces that characterize the allowable execution order for the lock operations. We use a thread modular verification approach to check that each thread obeys the lock interface. We verify the lock implementation assuming that the threads behave according to the lock interface. We demonstrate that this approach can be used to verify synchronization behavior in Java programs that use reentrant lock implementations for synchronization.

The global interaction behavior in message-based systems can be specified as a finite-state machine defining acceptable sequences of messages exchanged by a group of peers. Realizability analysis determines if there exist local implementations for each peer, such that their composition produces exactly the intended global behavior. Although there are existing sufficient conditions for realizability, we show that these earlier results all fail for a particular class of specifications called arbitrary-initiator protocols. We present a novel algorithm for deciding realizability by computing a finite-state model that keeps track of the information about the global state of a conversation protocol that each peer can deduce from the messages it sends and receives. By searching for disagreements between each peer’s deduced states, we provide a sound analysis for realizability that correctly classifies realizability of arbitrary-initiator protocols.

Analyzing interactions among peers that interact via messages is a crucial problem due to increasingly distributed nature of current software systems, especially the ones built using the service oriented computing paradigm. In service oriented computing, interactions among peers participating to a composite service involve message exchanges across organizational boundaries in a distributed computing environment. In order to build such systems in a reliable manner, it is necessary to develop techniques for analysis and verification of interactions among services. Collaboration diagrams provide a convenient visual model for modeling service interactions. In this paper, we present a tool that (1) checks the realizability of interactions specified by the given collaboration diagram, (2) verifies the LTL properties of the interactions specified by the given collaboration diagram by automatically converting it to a state machine model, and (3) synthesizes peer state machines that realize the set of interactions specified by the given collaboration diagram.

This paper presents techniques for analyzing channel contract specifications in Microsoft Research's Singularity operating system. A channel contract is a state machine that specifies the allowable interactions between a server and a client through an asynchronous communication channel. We show that, contrary to what is claimed in the Singularity documentation, processes that faithfully follow a channel contract can deadlock. We present a realizability analysis that can be used to identify channel contracts with problems. Our realizability analysis also leads to an efficient verification approach where properties about the interaction behavior can be verified without modeling the contents of communication channels. We analyzed more than 90 channel contracts from the Singularity code distribution and documentation. Only two contracts failed our realizability condition and these two contracts allow deadlocks. Our experimental results demonstrate that realizability analysis and verification of channel contracts can be done efficiently using our approach.

Given a program and an attack pattern (specified as a regular expression), we automatically generate string-based vulnerability signatures, i.e., a characterization that includes all malicious inputs that can be used to generate attacks. We use an automata-based string analysis framework. Using forward reachability analysis we compute an over-approximation of all possible values that string variables can take at each program point. Intersecting these with the attack pattern yields the potential attack strings if the program is vulnerable. Using backward analysis we compute an over-approximation of all possible inputs that can generate those attack strings. In addition to identifying existing vulnerabilities and their causes, these vulnerability signatures can be used to filter out malicious inputs. Our approach extends the prior work on automata-based string analysis by providing a backward symbolic analysis that includes a symbolic pre-image computation for deterministic finite automata on common string manipulating functions such as concatenation and replacement.

TAV-WEB 2008 is the third in a series of workshops that focus on testing, analysis and verification of web software. The goal of these workshops has been to bring together researchers from academic, research, and industrial communities interested in the emerging area of dependable Web software development, to present and discuss their recent research results.

We propose a novel method for modular verification of web service compositions. We first use symbolic fixpoint computations to derive conditions on the incoming messages and relations among the incoming and outgoing messages of individual BPEL web services. These pre- and post-conditions are accumulated and serve as a repository of summarizations of individual web services. We then compose the summaries of the invoked BPEL services to model external invocations, resulting in a scalable verification approach for web service compositions. Our technical contributions include (1) an efficient symbolic encoding for modeling the concurrency semantics of systems having both multi-threading and message passing, and (2) a scalable method for summarizing concurrent processes that interact with each other using synchronous message passing, along with a modular framework that utilizes these summaries for scalable verification.

Verification techniques relying on state enumeration (e.g., model checking) face two important challenges: the state-space explosion, an exponential increase in the state space as the number of components increases; and environment generation, modeling components that are either not available for analysis, or that cannot be handled by the verification tool in use. We propose a semi-automated approach for attacking these problems. In our approach, interfaces for the components not under analysis are specified using a specification language based on grammars. Specifically, an interface grammar for a component specifies the sequences of method invocations that are allowed by that component. We have built an compiler that takes the interface grammar for a component as input and generates a stub for that component. The stub thus generated can be used to replace that component during state space exploration, either to moderate state space explosion, or to provide an executable environment for the component under verification. We conducted a case study by writing an interface grammar for the Enterprise JavaBeans (EJB) persistence interface, and using the resulting stub to check EJB clients using the JPF model checker. Our results show that EJB clients can be verified efficiently with JPF using our approach.

We propose an interface specification language based on grammars for modular software model checking. In our interface specification language, component interfaces are specified as context free grammars. An interface grammar for a component specifies the sequences of method invocations that are allowed by that component. Using interface grammars one can specify nested call sequences that cannot be specified using interface specification formalisms that rely on finite state machines. Moreover, our interface grammars allow specification of semantic predicates and actions, which are Java code segments that can be used to express additional interface constraints. We have built an interface compiler that takes the interface grammar for a component as input and generates a stub for that component. The resulting stub is a table-driven parser generated from the input interface grammar. Invocation of a method within the component becomes the lookahead symbol for the stub/parser. The stub/parser uses a parser stack, the lookahead, and a parse table to guide the parsing. The semantic predicates and semantic actions that appear in the right hand sides of the production rules are executed when they appear at the top of the stack. We conducted a case study by writing an interface grammar for the Enterprise JavaBeans (EJB) persistence interface. Using our interface compiler we automatically generated an EJB stub using the EJB interface grammar. We used the JPF model checker to check EJB clients using this automatically generated EJB stub. Our results show that EJB clients can be verified efficiently using our approach.

Automated verification of distributed programs is a challenging problem. Since the behavior of a distributed program encompasses the behavior of the network, possible configurations of the network have to be investigated during verification. This leads to very large state spaces, and automated verification becomes infeasible. We present a framework that addresses this problem by decoupling the behavior of distributed programs from the behavior of the network. Our framework is based on a set of stub classes that replace native methods used in network communication and enables verification of distributed Java applications by isolating their behavior from the network. The framework supports two modes of verification: unit verification and integration verification. Integration verification checks multiple interacting distributed application components by running them in a single JVM and simulating the behavior of the network within the same JVM via stub classes. Unit verification targets a single component of a distributed application and requires that the user write an event generator class that utilizes the API exported by the framework. While unit verification only checks a single application component, it benefits from a greatly reduced state space compared do that of integration verification

An essential tool in object oriented modeling is the specification of cardinalities of associations between classes. In Object Constraint Language (OCL) such constraints are expressed as conditions on the sizes of the collections that correspond to associations. In this paper we present tools and techniques for automated verification of size properties of collection types in OCL. We automatically verify invariants related to the sizes of the collections of a class with respect to the pre and post-conditions of the methods of that class. Our approach is based on a size abstraction that abstracts away the contents of the collections, but preserves the constraints on their sizes. We implemented a tool which automates this abstraction by converting OCL expressions on collections to arithmetic expressions on their sizes. Following this translation, we employ an infinite state model checker, called Action Language Verifier (ALV), for size analysis. Size abstraction reduces the state space of the system and, hence, the cost of automated verification, and by focusing on size properties, enables us to use efficient, domain specific model checking techniques for automated verification. To demonstrate the effectiveness of our approach we conducted a case study on the OCL specification of the Java Card API. The OCL specification of the Java Card API consists of 31 classes and 150 methods. Using our tool, we translated the OCL specification of each class to Action Language and verified the size properties using ALV. Verification with ALV took only a few seconds per class and we revealed errors in 26 out of the 150 method specifications.

Abstract There has been significant progress in automated verification techniques based on model checking. However, scalable software model checking remains a challenging problem. We believe that this problem can be addressed using a design for verification approach based on design patterns that facilitate scalable automated verification. In this paper, we present a design for verification approach for highly dependable concurrent programming using a design pattern for concurrency controllers. A concurrency controller class consists of a set of guarded commands defining a synchronization policy, and a stateful interface describing the correct usage of the synchronization policy. We present an assume-guarantee style modular verification strategy which separates the verification of the controller behavior from the verification of the conformance to its interface. This allows us to execute the interface and behavior verification tasks separately using specialized verification techniques. We present a case study demonstrating the effectiveness of the presented approach.

This paper investigates the application of infinite state model checking to the formal analysis of requirements specifications in the SCR (software cost reduction) tabular notation using action language verifier (ALV). After reviewing the SCR method and tools and the action language, experimental results are presented of formally analyzing two SCR specifications using ALV, The application of ALV to verify or falsify (by generating counterexamples) the state and transition invariants of SCR specifications and to check disjointness and coverage properties is described. ALV is compared with the verification techniques that have been integrated into the SCR toolset

We propose an hierarchical state machine (HSM) model for specifying behavioral interfaces of peers participating in a composite Web service. We integrate the HSM model to a design pattern which is supported by a modular verification technique that can 1) statically analyze the properties about global interactions of a composite Web service and 2) check the conformance of the Java implementations of the participant peers to their interfaces. We extend the synchronizability analysis to HSMs to efficiently identify composite Web services whose global interactions can be analyzed with respect to unbounded queues using finite state model checkers. We also discuss automated translation of behavioral interfaces specified as HSMs to BPEL specifications to be published and used by other services.

We present an experimental study which demonstrates that model checking techniques can be effective in finding synchronization errors in safety critical software when they are combined with a design for verification approach. We apply the concurrency controller design pattern to the implementation of the synchronization operations in Java programs. This pattern enables a modular verification strategy by decoupling the behaviors of the concurrency controllers from the behaviors of the threads that use them using interfaces specified as finite state machines. The behavior of a concurrency controller can be verified with respect to arbitrary numbers of threads using infinite state model checking techniques, and the threads which use the controller classes can be checked for interface violations using finite state model checking techniques. We present techniques for thread isolation which enables us to analyze each thread in the program separately during interface verification. We conducted an experimental study investigating the effectiveness of the presented design for verification approach on safety critical air traffic control software. In this study, we first reengineered the Tactical Separation Assisted Flight Environment (TSAFE) software using the concurrency controller design pattern. Then, using fault seeding, we created 40 faulty versions of TSAFE and used both infinite and finite state verification techniques for finding the seeded faults. The experimental study demonstrated the effectiveness of the presented modular verification approach and resulted in a classification of faults that can be found using the presented approach.

Although research in automated verication has produced very promising results, the question of how to effectively integrate these results into the software and hardware development processes is still unresolved. Typically, fully automated verication techniques are not scalable, and scalable verication techniques require substantial user guidance. Alternatively, developers could facilitate scalable verication by constructing software and hardware systems in ways that make them easier to verify. In this panel we will discuss the idea of design for verication.

Action language verifier (ALV) is an infinite-state symbolic model checker. ALV can verify (or falsify, by generating counter-examples) temporal logic properties of systems that can be modeled using a combination of Boolean logic and linear arithmetic expressions on Boolean, enumerated and (possibly unbounded) integer variables and parameterized integer constants. In this paper, we apply ALV to the verification of parameterized hierarchical state machine specifications. We extend the standard notation for hierarchical state machines by introducing primitives for explicit specification of asynchronous processes and their finite and parameterized instantiations. We define the formal semantics of these primitives, where the states of the parameterized processes are mapped to integer variables using the counting abstraction technique. We apply the presented approach to the specification and analysis of an airport ground traffic controller and verify several correctness properties of this specification using ALV.

We present a design for verification approach to developing reliable web services. We focus on composite web services which consist of asynchronously communicating peers. Our goal is to automatically verify properties of interactions among such peers. We propose a design pattern that eases the development of such web services and enables a modular, assume-guarantee style verification strategy. In the proposed design pattern, each peer is associated with a behavioral interface description which specifies how that peer will interact with other peers. Using these peer interfaces we automatically generate BPEL specifications to publish for interoperability. Assuming that the participating peers behave according to their interfaces, we verify safety and liveness properties about the global behavior of the composite web service during behavior verification. During interface verification, we check that each peer implementation conforms to its interface. Using the modularity in the proposed design pattern, we are able to perform the interface verification of each peer and the behavior verification as separate steps. Our experiments show that, using this modular approach, one can automatically and efficiently verify web service implementations.

We present a framework for analyzing interactions among Web services that communicate with asynchronous messages. We model the interactions among the peers participating in a composite Web service as conversations, the global sequences of messages exchanged among the peers. This naturally leads to the following model checking problem: Given an LTL property and a composite Web service, do the conversations generated by the composite Web service satisfy the property? We show that asynchronous messaging leads to state space explosion for bounded message queues and undecidability of the model checking problem for unbounded message queues. We propose a technique called synchronizability analysis to tackle this problem. If a composite Web service is synchronizable, its conversation set remains the same when asynchronous communication is replaced with synchronous communication. We give a set of sufficient conditions that guarantee synchronizability and that can be checked statically. Based on our synchronizability results, we show that a large class of composite Web services with unbounded message queues can be verified completely using a finite state model checker such as SPIN. We also show that synchronizability analysis can be used to check the reliability of top-down conversation specifications and we contrast the conversation model with the Message Sequence Charts. We integrated synchronizability analysis to a tool we developed for analyzing composite Web services.

A conversation protocol is a top-down specification framework which specifies desired global behaviors of a Web service composition. In our earlier work (Fu et al., 2003) we studied the problem of realizability, i.e., given a conversation protocol, can a Web service composition be synthesized to generate behaviors as specified by the protocol. Several sufficient realizability conditions were proposed by Fu et al. (2003) to ensure realizability. Conversation protocols studied by Fu et al. (2003), however, are essentially abstract control flows without data semantics. This paper extends the work by Fu et al. (2003) and achieves more accurate analysis by considering data semantics: to overcome the state-space explosion caused by the data content, we propose a symbolic analysis technique for each realizability condition. In addition, we show that the analysis of the autonomy condition can be done using an iterative refinement approach.

The use of XML as the de facto data exchange standard has allowed integration of heterogeneous web based software systems regardless of implementation platforms and programming languages. On the other hand, the rich tree-structured data representation, and the expressive XML query languages (such as XPath) make formal specification and verification of software systems that manipulate XML data a challenge. In this paper, we present our initial efforts in automated verification of XML data manipulation operations using the SPIN model checker. We present algorithms for translating (bounded) XML data and XPath expressions to Promela, the input language of SPIN. The techniques presented in this paper constitute the basis of our Web Service Analysis Tool (WSAT) which verifies LTL properties of composite web services.

This industrial panel is organized to discuss the views, experiences and opinions of formal methods practitioners frclni desigri automation, hardware and sofhyare industries, in order to understand rlie industrial needs ar7d trends in rising fnmial methods. In particulas we discuss the currertt tlinist or1 application of fnmlal verificntion in software duveekopnient, and what liurdware fomiai verification experiences bring to bear forfim” sofhvare verification.

This paper presents a set of tools and techniques for analyzing interactions of composite web services which are specified in BPEL and communicate through asynchronous XML messages. We model the interactions of composite web services as conversations, the global sequence of messages exchanged by the web services. As opposed to earlier work, our tool-set handles rich data manipulation via XPath expressions. This allows us to verify designs at a more detailed level and check properties about message content. We present a framework where BPEL specifications of web services are translated to an intermediate representation, followed by the translation of the intermediate representation to a verification language. As an intermediate representation we use guarded automata augmented with unbounded queues for incoming messages, where the guards are expressed as XPath expressions. As the target verification language we use Promela, input language of the model checker SPIN. Since SPIN model checker is a finite-state verification tool we can only achieve partial verification by fixing the sizes of the input queues in the translation. We propose the concept of synchronizability to address this problem. We show that if a composite web service is synchronizable, then its conversation set remains same when asynchronous communication is replaced with synchronous communication. We give a set of sufficient conditions that guarantee synchronizability and that can be checked statically. Based on our synchronizability results, we show that a large class of composite web services with unbounded input queues can be completely verified using a finite state model checker such as SPIN.

This paper introduces a framework for modeling and specifying the global behavior of e-service compositions. Under this framework, peers (individual e-services) communicate through asynchronous messages and each peer maintains a queue for incoming messages. A global "watcher" keeps track of messages as they occur. We propose and study a central notion of a "conversation", which is a sequence of (classes of) messages observed by the watcher. We consider the case where the peers are represented by Mealy machines (finite state machines with input and output). The sets of conversations exhibit unexpected behaviors. For example, there exists a composite e-service based on Mealy peers whose set of conversations is not context free (and not regular). (The set of conversations is always context sensitive.) One cause for this is the queuing of messages; we introduce an operator "prepone" that simulates queue delays from a global perspective and show that the set of conversations of each Mealy e-service is closed under prepone. We illustrate that the global prepone fails to completely capture the queue delay effects and refine prepone to a "local" version on conversations seen by individual peers. On the other hand, Mealy implementations of a composite e-service will always generate conversations whose "projections" are consistent with individual e-services. We use projection-join to reflect such situations. However, there are still Mealy peers whose set of conversations is not the local prepone and projection-join closure of any regular language. Therefore, we propose conversation specifications as a formalism to define the conversations allowed by an e-service composition. We give two technical results concerning the interplay between the local behaviors of Mealy peers and the global behaviors of their compositions. One result shows that for each regular language, its local prepone and projection-join closure corresponds to the set of conversations by some Mealy peers effectively constructed from . The second result gives a condition on the shape of a composition which guarantees that the set of conversations that can be realized is the local prepone and projection-join closure of a regular language.

Run-time errors in concurrent programs are generally due to the wrong usage of synchronization primitives such as monitors. Conventional validation techniques such as testing become ineffective for concurrent programs since the state space increases exponentially with the number of concurrent processes. In this paper, we propose an approach in which 1) the concurrency control component of a concurrent program is formally specified, 2) it is verified automatically using model checking, and 3) the code for concurrency control component is automatically generated. We use monitors as the synchronization primitive to control access to a shared resource by multipleconcurrent processes. Since our approach decouples the concurrency control component from the rest of the implementation it is scalable. We demonstrate the usefulness of our approach by applying it to a case study on Airport Ground Traffic Control.We use the Action Language to specify the concurrency control component of a system. Action Language is a specification language for reactive software systems. It is supported by an infinite-state model checker that can verify systems with boolean, enumerated and udbounded integer variables. Our code generation tool automatically translates the verified Action Language specification into a Java monitor. Our translation algorithm employs symbolic manipulation techniques and the specific notification pattern to generate an optimized monitor class by eliminating the context switch overhead introduced as a result of unnecessary thread notification. Using counting abstraction, we show that we can automatically verify the monitor specifications for arbitrary number of threads.

Action Language is a specification language for reactive software systems. We present the Action Language Verifier which consists of: 1) a compiler that converts Action Language specifications to composite symbolic representations, and 2) an infinite-state symbolic model checker which verifies (or falsifies) CTL properties of Action Language specifications. Our symbolic manipulator (Composite Symbolic Library) combines a BDD manipulator (for boolean and enumerated types) and a Presburger arithmetic manipulator (for integers) to handle multiple variable types. Since we allow unbounded integer variables, model checking queries become undecidable. We present several heuristics used by the Action Language Verifier to achieve convergence.

We present a specification language called Action Language for model checking software specifications. Action Language forms an interface between transition system models that a model checker generates and high level specification languages such as Statecharts, RSML and SCR—similar to an assembly language between a microprocessor and a programming language. We show that Action Language translations of Statecharts and SCR specifications are compact and they preserve the structure of the original specification. Action Language allows specification of both synchronous and asynchronous systems. It also supports modular specifications to enable compositional model checking.

There has been a surge of progress in automated verification methods based on state exploration. In areas like hardware design, these technologies are rapidly augmenting key phases of testing and validation. To date, one of the most successful of these methods has been symbolic model-checking, in which large finite-state machines are encoded into compact data structures such as Binary Decision Diagrams (BDDs), and are then checked for safety and liveness properties. However, these techniques have not realized the same success on software systems. One limitation is their inability to deal with infinite-state programs, even those with a single unbounded integer. A second problem is that of finding efficient representations for various variable types. We recently proposed a model-checker for integer-based systems that uses arithmetic constraints as the underlying state representation. While this approach easily verified some subtle, infinite-state concurrency problems, it proved inefficient in its treatment of boolean and (unordered) enumerated types—which are not efficiently representable using arithmetic constraints. In this article we present a new technique that combines the strengths of both BDD and arithmetic constraint representations. Our composite model merges multiple type-specific symbolic representations in a single model-checker. A system's transitions and fixpoint computations are encoded using both BDD (for boolean and enumerated types) and arithmetic constraints (for integers) representations, where the choice depends on the variable types. Our composite model-checking strategy can be extended to other symbolic representations provided that they support operations such as intersection, union, complement, equivalence checking, and relational image computation. We also present conservative approximation techniques for composite representations to address the undecidability of model-checking on infinite-state systems. We demonstrate the effectiveness of our approach by analyzing two example software specifications which include a mixture of booleans, integers, and enumerated types. One of them is a requirements specification for the control software of a nuclear reactor's cooling system, and the other one is a protocol specification.

Model checking is a powerful technique for analyzing large, finite-state systems. In an infinite state system, however, many basic properties are undecidable. In this article, we present a new symbolic model checker which conservatively evaluates safety and liveness properties on programs with unbounded integer variables. We use Presburger formulas to symbolically encode a program's transition system, as well as its model-checking computations. All fixpoint calculations are executed symbolically, and their convergence is guaranteed by using approximation techniques. We demonstrate the promise of this technology on some well-known infinite-state concurrency problems.

Symbolic mode, checking has proved highly successful for large finite-state systems, in which states can be compactly encoded using binary decision diagrams (BDDs) or their variants. The inherent limitation of this approach is that it cannot be applied to systems with an infinite number of states --- even those with a single unbounded integer.Alternatively, we recently proposed a model checker for integer-based systems that uses Presburger constraints as the underlying state representation. While this approach easily verified some subtle, infinite-state concurrency problems, it proved inefficient in its treatment of Boolean and (unordered) enumerated types --- which possess no natural mapping to the Euclidean coordinate space.In this paper we describe a model checker which combines the strengths of both approaches. We use a composite model, in which a formula's valuations are encoded in a mixed BDD-Presburger form, depending on the variables used. We demonstrate our technique's effectiveness on a nontrivial requirements specification, which includes a mixture of Booleans, integers and enumerated types.

Many concurrent systems are required to maintain certain safety and liveness properties. One emerging method of achieving confidence in such systems is to statically verify them using model checking. In this approach an abstract, finite-state model of the system is constructed; then an automatic check is made to ensure that the requirements are satisfied by the model. In practice, however, this method is limited by the state space explosion problem.We have developed a compositional method that directly addresses this problem in the context of multi-tasking programs. Our solution depends on three key space-saving ingredients: (1) checking for counter-examples, which leads to simpler search algorithms; (2) automatic extraction of interfaces, which allows a refinement of the finite model --- even before its communicating partners have been compiled; and (3) using propositional "strengthening assertions" for the sole purpose of reducing state space.In this paper we present our compositional approach, and describe the software tools that support it.