Hybrid information flow analysis of web tracking (invited talk)

Thomas Jensen

INRIA and University of Copenhagen

Motivated by the problem of stateless web tracking (fingerprinting), we propose a novel approach to hybrid information flow monitoring by tracking the knowledge about secret variables using logical formulae. This knowledge representation helps to compare and improve precision of hybrid information flow monitors.

We define a generic hybrid monitor parametrised by a static analysis and derive sufficient conditions on the static analysis for soundness and relative precision of hybrid monitors.

We instantiate the generic monitor with a combined static constant and dependency analysis. Several other hybrid monitors including those based on well-known hybrid techniques for information flow control are formalised as instances of our generic hybrid monitor. These monitors are organised into a hierarchy that establishes their relative precision.

The talk is based on joint work with Nataliia Bielova and Frederic Besson

Sparse Dataflow Analysis with Pointers and Reachability

Magnus Madsen

Aarhus University

Many static analyzers exploit sparseness techniques to reduce the amount of information being propagated and stored during analysis. Although several variations are described in the literature, no existing technique is suitable for analyzing JavaScript code. In this paper, we point out the need for a sparse analysis framework that supports pointers and reachability. We present such a framework, which uses static single assignment form for heap addresses and computes def-use information on-the-fly. We also show that essential information about dominating definitions can be maintained efficiently using quadtrees. The framework is presented as a systematic modification of a traditional dataflow analysis algorithm.

Our experimental results demonstrate the effectiveness of the technique for a suite of JavaScript programs. By also comparing the performance with an idealized staged approach that computes pointer information with a pre-analysis, we show that the cost of computing def-use information on-the-fly is remarkably small.

Joint work with Anders Møller

Toolchain for High Performance Synthesizable Processors

Pascal Schleuniger


Field programmable gate arrays, FPGAs, have become an attractive implementation technology for a broad range of computing systems. The inherently parallel structure of FPGAs allows for an efficient implementation of parallel algorithms. Sequential algorithms, on the other hand, are easier to implement on a microprocessor. However, for many applications it is convenient to have both a microprocessor to execute sequential tasks and dedicated hardware circuits to accelerate parallel sections of an algorithm. Thus, synthesizable processor cores are an attractive design choice for many FPGA designs. The use of synthesizable processor cores typically leads to a simpler board layout, removes some problems with signal integrity and electromagnetic interference, and reduces system costs.

We recently proposed a processor architecture, Tinuso, which optimizes performance by moving complexity from hardware to the compiler toolchain. For example, Tinuso assumes that implementations use superpipelining to attain a high clock frequency. Furthermore, it leverages predicated execution to circumvent costly pipeline stalls due to branches and all types of pipeline hazards are exposed to the compiler to keep the hardware complexity low. As a result we obtain a highly optimized processor pipeline that can be clocked with up to 376 MHz on modern state-of-the-art FPGAs.

However, it is not clear if current production compilers can successfully use predicated execution and schedule instructions so as to mitigate the hazards. In this presentation, we share our experiences developing a toolchain including compiler backend using the GNU Compiler Collection, GCC. For a set of C benchmarks, we show that a Tinuso implementation with our toolchain reaches an average performance improvement of 56% over a similar Xilinx MicroBlaze configuration while using 25% fewer hardware resources. While our experiences are overall positive, we expose some limitations in GCC that need to be addressed to achieve the full performance potential of Tinuso.

Joint work with Nicklas Bo Jensen, Andreas Hindborg and Sven Karlsson

Convex polyhedral abstractions, specialisation and property-based predicate splitting in Horn clause verification

John P. Gallagher

Roskilde University

We present an approach to constrained Horn clause (CHC) verification combining three techniques: abstract interpretation over a domain of convex polyhedra, specialisation of the constraints in CHCs using abstract interpretation of query-answer transformed clauses, and refinement by splitting predicates. The purpose of the work is to investigate how analysis and transformation tools developed for constraint logic programs (CLP) can be applied to the Horn clause verification problem. Abstract interpretation over convex polyhedra is capable of deriving sophisticated invariants and when used in conjunction with specialisation for propagating constraints it can frequently solve challenging verification problems. This is a contribution in itself, but refinement is needed when it fails, and the question of how to refine convex polyhedral analyses has not been studied much. We present a refinement technique based on interpolants derived from a counterexample trace; these are used to drive a property-based specialisation that splits predicates, leading in turn to more precise convex polyhedral analyses. The process of specialisation, analysis and splitting can be repeated, in a manner similar to the CEGAR and iterative specialisation approaches.

Joint work with Bishoksan Kafle

Multi-Core Model Checking as an Abstract Interpretation Engine

Mads Chr. Olesen

Aalborg University

The relationship between model checking and abstract interpretation has been explored many times. In this talk we present an automata-based approach to abstract interpretation, by augmenting the finite automaton given by the control-flow graph with abstract transformers over a lattice.

The automaton is used as input for a model checker, in this case LTSmin, which can exploit multi-core processors for a scalable computation.

Furthermore, the use of a modelling formalism as intermediary format allows the program analyst to simulate, combine and alter models to perform ad-hoc experiments, such as trying various trace partitionings.

QuickChecking Static Analysis Properties

Jan Midtgaard

A static analysis can check programs for potential errors. A natural question that arises is therefore: who checks the checker? Researchers have given this question varying attention, ranging from basic testing techniques, informal monotonicity arguments, thorough soundness proofs by hand, to automated fixed point checking.

We demonstrate how quickchecking can be used to test a range of static analysis properties with limited effort. Our approach is twofold:

(1) we show how we can check a range of algebraic lattice properties --- to help ensure that an implementation follows the formal specification of a lattice, and

(2) we offer a number of generic, type-safe combinators to check transfer functions and operators between lattices --- to help ensure that these are, e.g., monotone, strict, or invariant.

We substantiate our claims by quickchecking a non-trivial type analysis for the Lua programming language.

Correctness and Performance Analysis of Distributed High Performance Programs in Scala

Felix P. Hargreaves

University of Southern Denmark

This talk briefly presents the Functional object-oriented Parallel framework (FooPar) for high-level high-performance computing in Scala. Central to this framework are Distributed Memory Parallel Data structures (DPDs), i.e., collections of data distributed in a shared nothing system together with parallel operations on these data. The framework was developed with emphasis on analyzability in terms of correctness and asymptotic running time.

We show how higher order functions in FooPar can modularize proofs of correctness and running time analysis. We go on to the correctness and safety of one communication algorithm and show how specification testing (via ScalaCheck) can be used to bridge the gap between proof and implementation.