arXiv subjects

Thomas Wies

Publications and source records attributed to Thomas Wies.

28 records · Page 2Linked to original sources

arXiv2017

Go with the Flow: Compositional Abstractions for Concurrent Data Structures (Extended Version)

Concurrent separation logics have helped to significantly simplify correctness proofs for concurrent data structures. However, a recurring problem in such proofs is that data structure abstractions that work well in the sequential setting are much harder to reason about in a concurrent setting due to complex sharing and overlays. To solve this problem, we propose a novel approach to abstracting regions in the heap by encoding the data structure invariant into a local condition on each individual node. This condition may depend on a quantity associated with the node that is computed as a fixpoint over the entire heap graph. We refer to this quantity as a flow. Flows can encode both structural properties of the heap (e.g. the reachable nodes from the root form a tree) as well as data invariants (e.g. sortedness). We then introduce the notion of a flow interface, which expresses the relies and guarantees that a heap region imposes on its context to maintain the local flow invariant with respect to the global heap. Our main technical result is that this notion leads to a new semantic model of separation logic. In this model, flow interfaces provide a general abstraction mechanism for describing complex data structures. This abstraction mechanism admits proof rules that generalize over a wide variety of data structures. To demonstrate the versatility of our approach, we show how to extend the logic RGSep with flow interfaces. We have used this new logic to prove linearizability and memory safety of nontrivial concurrent data structures. In particular, we obtain parametric linearizability proofs for concurrent dictionary algorithms that abstract from the details of the underlying data structure representation. These proofs cannot be easily expressed using the abstraction mechanisms provided by existing separation logics.

cs.LO↗

arXiv2017

The VACCINE Framework for Building DLP Systems

Conventional Data Leakage Prevention (DLP) systems suffer from the following major drawback: Privacy policies that define what constitutes data leakage cannot be seamlessly defined and enforced across heterogeneous forms of communication. Administrators have the dual burden of: (1) manually self-interpreting policies from handbooks to specify rules (which is error-prone); (2) extracting relevant information flows from heterogeneous communication protocols and enforcing policies to determine which flows should be admissible. To address these issues, we present the Verifiable and ACtionable Contextual Integrity Norms Engine (VACCINE), a framework for building adaptable and modular DLP systems. VACCINE relies on (1) the theory of contextual integrity to provide an abstraction layer suitable for specifying reusable protocol-agnostic leakage prevention rules and (2) programming language techniques to check these rules against correctness properties and to enforce them faithfully within a DLP system implementation. We applied VACCINE to the Family Educational Rights and Privacy Act and Enron Corporation privacy regulations. We show that by using contextual integrity in conjunction with verification techniques, we can effectively create reusable privacy rules with specific correctness guarantees, and check the integrity of information flows against these rules. Our experiments in emulated enterprise settings indicate that VACCINE improves over current DLP system design approaches and can be deployed in enterprises involving tens of thousands of actors.

cs.CR↗

arXiv2016

Error Invariants for Concurrent Traces

Error invariants are assertions that over-approximate the reachable program states at a given position in an error trace while only capturing states that will still lead to failure if execution of the trace is continued from that position. Such assertions reflect the effect of statements that are involved in the root cause of an error and its propagation, enabling slicing of statements that do not contribute to the error. Previous work on error invariants focused on sequential programs. We generalize error invariants to concurrent traces by augmenting them with additional information about hazards such as write-after-write events, which are often involved in race conditions and atomicity violations. By providing the option to include varying levels of details in error invariants-such as hazards and branching information-our approach allows the programmer to systematically analyze individual aspects of an error trace.We have implemented a hazard-sensitive slicing tool for concurrent traces based on error invariants and evaluated it on benchmarks covering a broad range of real-world concurrency bugs. Hazard-sensitive slicing significantly reduced the length of the considered traces and still maintained the root causes of the concurrency bugs.

cs.SE↗

arXiv2016

Crowdsourced, Actionable and Verifiable Contextual Informational Norms

There is often a fundamental mismatch between programmable privacy frameworks, on the one hand, and the ever shifting privacy expectations of computer system users, on the other hand. Based on the theory of contextual integrity (CI), our paper addresses this problem by proposing a privacy framework that translates users' privacy expectations (norms) into a set of actionable privacy rules that are rooted in the language of CI. These norms are then encoded using Datalog logic specification to develop an information system that is able to verify whether information flows are appropriate and the privacy of users thus preserved. A particular benefit of our framework is that it can automatically adapt as users' privacy expectations evolve over time. To evaluate our proposed framework, we conducted an extensive survey involving more than 450 participants and 1400 questions to derive a set of privacy norms in the educational context. Based on the crowdsourced responses, we demonstrate that our framework can derive a compact Datalog encoding of the privacy norms which can in principle be directly used for enforcing privacy of information flows within this context. In addition, our framework can automatically detect logical inconsistencies between individual users' privacy expectations and the derived privacy logic.

cs.CY↗

arXiv2015

On Practical SMT-Based Type Error Localization

Compilers for statically typed functional programming languages are notorious for generating confusing type error messages. When the compiler detects a type error, it typically reports the program location where the type checking failed as the source of the error. Since other error sources are not even considered, the actual root cause is often missed. A more adequate approach is to consider all possible error sources and report the most useful one subject to some usefulness criterion. In our previous work, we showed that this approach can be formulated as an optimization problem related to satisfiability modulo theories (SMT). This formulation cleanly separates the heuristic nature of usefulness criteria from the underlying search problem. Unfortunately, algorithms that search for an optimal error source cannot directly use principal types which are crucial for dealing with the exponential-time complexity of the decision problem of polymorphic type checking. In this paper, we present a new algorithm that efficiently finds an optimal error source in a given ill-typed program. Our algorithm uses an improved SMT encoding to cope with the high complexity of polymorphic typing by iteratively expanding the typing constraints from which principal types are derived. The algorithm preserves the clean separation between the heuristics and the actual search. We have implemented our algorithm for OCaml. In our experimental evaluation, we found that the algorithm reduces the running times for optimal type error localization from minutes to seconds and scales better than previous localization algorithms.

cs.PL↗

arXiv2015

On Deciding Local Theory Extensions via E-matching

Satisfiability Modulo Theories (SMT) solvers incorporate decision procedures for theories of data types that commonly occur in software. This makes them important tools for automating verification problems. A limitation frequently encountered is that verification problems are often not fully expressible in the theories supported natively by the solvers. Many solvers allow the specification of application-specific theories as quantified axioms, but their handling is incomplete outside of narrow special cases. In this work, we show how SMT solvers can be used to obtain complete decision procedures for local theory extensions, an important class of theories that are decidable using finite instantiation of axioms. We present an algorithm that uses E-matching to generate instances incrementally during the search, significantly reducing the number of generated instances compared to eager instantiation strategies. We have used two SMT solvers to implement this algorithm and conducted an extensive experimental evaluation on benchmarks derived from verification conditions for heap-manipulating programs. We believe that our results are of interest to both the users of SMT solvers as well as their developers.

cs.LO↗

arXiv2015

Learning Invariants using Decision Trees

The problem of inferring an inductive invariant for verifying program safety can be formulated in terms of binary classification. This is a standard problem in machine learning: given a sample of good and bad points, one is asked to find a classifier that generalizes from the sample and separates the two sets. Here, the good points are the reachable states of the program, and the bad points are those that reach a safety property violation. Thus, a learned classifier is a candidate invariant. In this paper, we propose a new algorithm that uses decision trees to learn candidate invariants in the form of arbitrary Boolean combinations of numerical inequalities. We have used our algorithm to verify C programs taken from the literature. The algorithm is able to infer safe invariants for a range of challenging benchmarks and compares favorably to other ML-based invariant inference techniques. In particular, it scales well to large sample sets.

cs.PL↗

arXiv2014

Dynamic Package Interfaces - Extended Version

A hallmark of object-oriented programming is the ability to perform computation through a set of interacting objects. A common manifestation of this style is the notion of a package, which groups a set of commonly used classes together. A challenge in using a package is to ensure that a client follows the implicit protocol of the package when calling its methods. Violations of the protocol can cause a runtime error or latent invariant violations. These protocols can extend across different, potentially unboundedly many, objects, and are specified informally in the documentation. As a result, ensuring that a client does not violate the protocol is hard. We introduce dynamic package interfaces (DPI), a formalism to explicitly capture the protocol of a package. The DPI of a package is a finite set of rules that together specify how any set of interacting objects of the package can evolve through method calls and under what conditions an error can happen. We have developed a dynamic tool that automatically computes an approximation of the DPI of a package, given a set of abstraction predicates. A key property of DPI is that the unbounded number of configurations of objects of a package are summarized finitely in an abstract domain. This uses the observation that many packages behave monotonically: the semantics of a method call over a configuration does not essentially change if more objects are added to the configuration. We have exploited monotonicity and have devised heuristics to obtain succinct yet general DPIs. We have used our tool to compute DPIs for several commonly used Java packages with complex protocols, such as JDBC, HashSet, and ArrayList.

cs.SE↗

arXiv2013

A Notion of Dynamic Interface for Depth-Bounded Object-Oriented Packages

Programmers using software components have to follow protocols that specify when it is legal to call particular methods with particular arguments. For example, one cannot use an iterator over a set once the set has been changed directly or through another iterator. We formalize the notion of dynamic package interfaces (DPI), which generalize state-machine interfaces for single objects, and give an algorithm to statically compute a sound abstraction of a DPI. States of a DPI represent (unbounded) sets of heap configurations and edges represent the effects of method calls on the heap. We introduce a novel heap abstract domain based on depth-bounded systems to deal with potentially unboundedly many objects and the references among them. We have implemented our algorithm and show that it is effective in computing representations of common patterns of package usage, such as relationships between viewer and label, container and iterator, and JDBC statements and cursors.

cs.SE↗

arXiv2006

On Verifying Complex Properties using Symbolic Shape Analysis

One of the main challenges in the verification of software systems is the analysis of unbounded data structures with dynamic memory allocation, such as linked data structures and arrays. We describe Bohne, a new analysis for verifying data structures. Bohne verifies data structure operations and shows that 1) the operations preserve data structure invariants and 2) the operations satisfy their specifications expressed in terms of changes to the set of objects stored in the data structure. During the analysis, Bohne infers loop invariants in the form of disjunctions of universally quantified Boolean combinations of formulas. To synthesize loop invariants of this form, Bohne uses a combination of decision procedures for Monadic Second-Order Logic over trees, SMT-LIB decision procedures (currently CVC Lite), and an automated reasoner within the Isabelle interactive theorem prover. This architecture shows that synthesized loop invariants can serve as a useful communication mechanism between different decision procedures. Using Bohne, we have verified operations on data structures such as linked lists with iterators and back pointers, trees with and without parent pointers, two-level skip lists, array data structures, and sorted lists. We have deployed Bohne in the Hob and Jahob data structure analysis systems, enabling us to combine Bohne with analyses of data structure clients and apply it in the context of larger programs. This report describes the Bohne algorithm as well as techniques that Bohne uses to reduce the ammount of annotations and the running time of the analysis.

cs.PL↗