Abstract:

In our project we are working on a framework that provides holistic security guarantees for web-based systems in which information flows heavily but not all flows should be allowed. As a case study we developed CoCon, a conference management system with verified document confidentiality. In my talk, I will start with a demo of CoCon, show which properties of the system we verified in the interactive theorem prover Isabelle and explain how we technically capture the intuitive idea that an attacker cannot learn any secrets of the system. A discussion of limitations of our approach will follow together with a summary of our experience with deployment of CoCon for real-life conferences. At the end, I will shortly mention future work.

Abstract:

We introduce a graphical syntax for signal flow diagrams based on the language of symmetric monoidal categories. Using universal categorical constructions, we provide a stream semantics and a sound and complete axiomatisation. A certain class of diagrams captures the orthodox notion of signal flow graph used in control theory; we show that any diagram of our syntax can be realised, via rewriting in the equational theory, as a signal flow graph.

Abstract:

Communication and synchronization are two main challenges in

designing and implementing concurrent programs, and consequently the main sources of

concurrency bugs. Concurrency bugs may lead to unintended program behavior as the

result of a particular ordering of actions in different threads at runtime.

Communication mechanisms for concurrent programs are generally based on either shared

memory or message passing. In the shared memory mechanism, concurrency bugs may manifest

at runtime as unexpected order in accessing shared data. Similarly, in

the message passing mechanism, unexpected order in sending and receiving messages

may result in a failure such as a deadlock.

We present a general framework for understanding the cause of

failure in concurrent programs by isolating from concurrent traces the

problematic or unexpected order of events which may cause a failure.

In devising our dynamic techniques for bug explanation,

we follow two different approaches, namely anomaly detection and slicing.

Our anomaly detection approach is based on statistical analysis and pattern mining.

In a completely different approach, we use a proof-based technique to construct

semantics-aware slices from failing traces.

We evaluate the efficiency and effectiveness of our proposed techniques

on benchmarks covering a broad range of real-world concurrency bugs. Moreover, we

compare the strengths and limitations of the anomaly detection technique with

the proof-based slicing technique.

Abstract:

We consider data automata in the form of finite automata equipped with variables (counters or registers) ranging over infinite data domains. A trace of such a data automaton is an alternating sequence of alphabet symbols and values taken by the counters during an execution of the automaton. We address the problem of checking the inclusion between the sets of traces (data languages) recognized by such automata. Since the problem is undecidable in general, we give a semi-algorithm based on abstraction refinement, which is proved to be sound and complete modulo termination. Due to the undecidability of the trace inclusion problem, our procedure is not guaranteed to terminate. We have implemented our technique in a prototype tool and show promising results on several non-trivial examples.

Abstract:

Unsatisfiability proofs in the DRAT format became the de

facto standard to increase the reliability of contemporary SAT solvers.

We consider the problem of generating proofs for the XOR reasoning

component in SAT solvers and propose two methods: direct translation

transforms every XOR constraint addition inference into a DRAT proof,

whereas T-translation avoids the exponential blow-up in direct transla-

tions by using fresh variables. T-translation produces DRAT proofs from

Gaussian elimination records that are polynomial in the size of the input

CNF formula. Experiments show that a combination of both approaches

with a simple prediction method outperforms the BDD-based method.

Abstract:

Security vulnerabilities plague modern systems because writing secure systems code is hard. Promising approaches can retrofit security automatically via runtime checks that implement the desired security policy; these checks guard critical operations, like memory accesses. Alas, the induced slowdown usually exceeds by a wide margin what system users are willing to tolerate in production, so these tools are hardly ever used. As a result, the insecurity of real-world systems persists. We present an approach in which developers/operators can specify what level of overhead they find acceptable for a given workload (e.g., 5%); our proposed tool ASAP then automatically instruments the program to maximize its security while staying within the specified “overhead budget.” Two insights make this approach effective: most overhead in existing tools is due to only a few “hot” checks, whereas the checks most useful to security are typically “cold”and cheap. We evaluate ASAP on programs from the Phoronix and SPEC benchmark suites. It can precisely select the best points in the security-performance spectrum. Moreover, we analyzed existing bugs and security vulnerabilities in RIPE, OpenSSL, and the Python interpreter, and found that the protection level offered by the ASAP approach is sufficient to protect against all of them. Joint work with Jonas Wagner, Volodymyr Kuznetsov and George Candea (EPFL), presented at IEEE S&P (Oakland) 2015.

Abstract:

Difference constraints have been used for termination analysis in the literature, where they denote relational inequalities of the form x ≤ y + c, and describe that the value of x in the current state is at most the value of y in the previous state plus some integer constant c. We believe that difference constraints are also a good choice for complexity and resource bound analysis because the complexity of imperative programs typically arises from counter increments and resets, which can be modeled naturally by difference constraints. In this article we propose a bound analysis based on difference constraints. We make the following contributions:

(1) Our analysis handles bound analysis problems of high practical relevance which current approaches cannot handle: We extend the range of bound analysis to a class of challenging but natural loop iteration patterns which typically appear in parsing and string-matching routines.

(2) We advocate the idea of using bound analysis to infer invariants: Our soundness proven algorithm obtains invariants through bound analysis, the inferred invariants are in turn used for obtaining bounds. Our bound analysis therefore does not rely on external techniques for invariant generation.

(3) We demonstrate that difference constraints are a suitable abstract program model for automatic complexity and resource bound analysis: We provide efficient abstraction techniques for obtaining difference constraint programs from imperative code.

(4) We report on a thorough experimental comparison of state-of-the-art bound analysis tools.