Anonymity networks such as Tor are a critical privacy-enabling technology. Tor's hidden services protect the location of the server hosting the service and provide encryption at every hop from a client to the hidden server. This presentation we will introduce CARONTE, a platform to measure the prevalence of content leaks in hidden services, i.e., information in the content or configuration of the hidden service that gives away the location of the hidden server. Compared to prior approaches that deanonymize hidden services CARONTE implements a novel approach that does not rely on flaws on the Tor protocol and assumes an open-world, i.e., it does not assume a short list of candidate servers is known in advance. CARONTE finds content leaks leading to deanonymization in 4.7% of hidden services. It also uncovers that 84% of the deanonymized hidden services are not trying to hide their location and that 21% of hidden services are running on Tor relays.

We study systems consisting of a leader process and arbitrarily many anonymous and identical contributors. Processes communicate through a shared, bounded-value register. While each operation on the register is atomic, there is no synchronization primitive to execute a sequence of operations atomically. We analyze the complexity of the safety verification problem. We consider the cases where leader and contributors are in turn modeled by finite-state machines, pushdown machines, and Turing machines. Our proofs use a mix of combinatorial properties of the model and some language-theoretic constructions of independent interest. We will also present preliminary results about the liveness verification problem.

We study the task of verifiable delegation of computation on encrypted data. We improve previous definitions in order to tolerate adversaries that learn whether or not clients accept the result of a delegated computation. In this strong model, we construct a scheme for arbitrary computations and highly efficient schemes for delegation of various classes of functions, such as linear combinations, high-degree univariate polynomials, and multivariate quadratic polynomials. Notably, the latter class includes many useful statistics. Using our solution, a client can store a large encrypted dataset on a server, query statistics over this data, and receive encrypted results that can be efficiently verified and decrypted.

As a key contribution for the efficiency of our schemes, we develop a novel homomorphic hashing technique that allows us to efficiently authenticate computations, at the same cost as if the data were in the clear, avoiding a 10⁴ overhead which would occur with a naive approach. We support our theoretical constructions with extensive implementation tests that show the practical feasibility of our schemes.

We introduce a model for mixed syntactic/semantic approximation of programs based on symbolic finite automata (SFA). The edges of SFA are labeled by predicates whose semantics specifies the denotations that are allowed by the edge. We introduce the notion of abstract symbolic finite automaton (ASFA) where approximation is made by abstract interpretation of symbolic finite automata, acting both at syntactic (predicate) and semantic (denotation) level. We investigate in the details how the syntactic and semantic abstractions of SFA relate to each other and contribute to the determination of the recognized language. Then we introduce a family of transformations for simplifying ASFA. We apply this model to prove properties of commonly used tools for similarity analysis of binary executables. Following the structure of their control flow graphs, disassembled binary executables are represented as (concrete) SFA, where states are program points and predicates represent the (possibly infinite) I/O semantics of each basic block in a constraint form. Known tools for binary code analysis (such as BinJuice and BinDiff) are viewed as specific choices of symbolic and semantic abstractions in our framework, making symbolic finite automata and their abstract interpretations a unifying model for comparing and reasoning about soundness and completeness of analyses of low-level code.

In the past decade, significant progress has been made towards design and development of efficient fine-grained (i.e., lock-free) concurrent data structures and algorithms, which take full advantage of parallel computations. Due to sophisticated interference scenarios and a large number of possible interactions between concurrent threads, working over the same shared data structures and employing fine-grained synchronization primitives (e.g., compare-and-swap command), ensuring correctness of fine-grained concurrent programs is challenging and error-prone.

In my talk, through a series of examples, I will describe recent advances in Fine-grained Concurrent Separation Logic (FCSL) - a mechanized logical framework for implementing and verifying fine-grained concurrent programs.

FCSL models effects of concurrent threads, manipulating shared resources, via two basic mathematical structures: state-transition systems (STSs) and partial commutative monoids (PCMs). Being simple enough, this model of concurrent resources, in combination with a small number of program and proof-level commands, is sufficient to give useful specifications and verify a large class of state-of-the-art concurrent libraries. By employing expressive type theory as a way to ascribe specifications to effectful programs, FCSL achieves scalability: even though the proofs for libraries might be large, they are done just once.

FCSL was proven sound with respect to the denotational semantic of action trees and implemented as a monadic embedding in Coq, a general-purpose mechanized framework for formal proofs. That is, concurrent programs written in FCSL's language are also Coq programs, so they can make use of all Coq's features as a programming language. As a part of my talk, I will demonstrate how proofs about concurrent programs in FCSL can be done directly in Coq, taking advantage of Coq's interactive proof construction machinery.

Efficient implementations of concurrent objects such as semaphores, locks, and atomic collections are essential to modern computing. Programming such objects is error prone: in minimizing the synchronization overhead between concurrent object invocations, one risks the conformance to their abstract data types (ADTs) — or in formal terms, one risks violating observational refinement. Precisely testing this refinement even within a single execution is intractable. Existing approaches are thus either limited to executions with very few object invocations, or rely on programmer interaction.

We develop scalable and effective algorithms for detecting refinement violations. Our algorithms are founded on incremental, symbolic reasoning, and exploit foundational insights into the refinement-checking problem. Our approach is sound, in that we detect only actual violations, and scales far beyond existing violation-detection algorithms. Furthermore, our approach does not require programmer interaction, for instance, in identifying linearization points. Empirically, we find that our approach is practically complete, in that we detect the violations arising in actual executions.

FIWARE is an open platform which integrates advanced OpenStack-based Cloud capabilities and a library of Generic Enablers making it easier to develop innovative applications in multiple sectors. The Orion Context Broker is a Generic Enabler used to manage context information that makes applications context-aware. The Policy Manager is a Generic Enabler that allows estimating the needed of an operation (e.g. horizontal scalability) based on monitoring data.

I propose a process calculus to model high-level distributed systems, whose topology is described by a digraph. The calculus enjoys interesting features, such as probabilistic behaviour and broadcast communication. I first focus on the problem of composing distributed systems, then I present a compositional theory based on a probabilistic generalisation of the de Nicola's and Hennessy's testing preorders.

Also, I define an extensional semantics for our calculus, which will be used to define both simulation and deadlock simulation preorders for distributed systems. I prove that the simulation preorder is sound with respect to the may-testing preorder; similarly, the deadlock simulation preorder is sound with respect to the must-testing preorder, for a large class of networks. I also provide a counterexample showing that completeness of the may testing preorder does not hold. I conclude the presentation with two simple applications of the developed theory: a probabilistic routing protocol and a virtual shared memory system.

Masking schemes transform circuits such that even adversaries that may learn the value of some intermediate wires do not learn any information about the circuit's secret input or state. Formal treatments of masking have been proposed but are limited to adversaries that may probe only one intermediate value, or perhaps two for small circuits. We first propose a characterization of threshold probing security as a probabilistic non-interference problem and propose a simple algorithm to prove it. We then propose an algorithm to avoid having to prove one instance of probabilistic non-interference for each possible set of adversary probes (of which there may be many). This allows us to prove the security of core circuits (AES SBox) at orders up to 5. However, practical applications are still out of reach. Therefore, we also propose simple notions of simulatability for gadgets and a simple type-based well-formedness condition on masked circuits that ensures that simulatability composes. Based on these observations, we propose a modular, optimizing and proof-producing masking compiler.

How do we know a program does what it claims to do? In this talk I will present CHABADA, our technique to detect suspicious behavior in Android apps. After clustering Android apps by their description topics, we identify outliers in each cluster with respect to their API usage. A "weather" app that sends messages thus becomes an anomaly; likewise, a "messaging" app would typically not be expected to access the current location. Applied on a set of 22,500+ Android applications, CHABADA identified several anomalies; additionally, it flagged over 70% of novel malware as such, without requiring any training on known malware patterns.