IMDEA initiative

Home > Events > Software Seminar Series (S3) - Fall 2016

Software Seminar Series (S3) - Fall 2016

Miguel Ambrona

Tuesday, December 13, 2016

11:00 Lecture hall 1, level B

Miguel Ambrona, PhD Student, IMDEA Software Institute

Generic Transformations of Predicate Encodings: Constructions and Applications

Abstract:

Predicate encodings are information-theoretic primitives that can be transformed generically into predicate encryption schemes for a broad class of predicates (Wee, TCC 2014; Chen, Gay, Wee, Eurocrypt 2015). Starting from the observation that predicate encodings admit a purely algebraic characterization equivalent to the original notion, we obtain several new results about predicate encodings. First, we propose two generic optimizations that improve their efficiency. Second, we propose new transformations for boolean combinations of predicate encodings. Third, we develop several new predicate encodings for boolean formulas and arithmetic span programs. In the important case of boolean formulas, our encodings are more efficient and attribute-hiding; moreover, they support revocation and delegation. Finally, we implement our approach and experimentally validate its efficiency gains.


Time and place:
11:00 Lecture hall 1, level B
IMDEA Software Institute, Campus de Montegancedo
28223-Pozuelo de Alarcón, Madrid, Spain


Pepe Vila

Tuesday, November 22, 2016

11:00 Lecture hall 1, level B

Pepe Vila, PhD Student, IMDEA Software Institute

Loophole: Timing Attacks on Shared Event Loops in Chrome

Abstract:

Event-driven programming (EDP) is the prevalent paradigm for graphical user interfaces, web clients, and it is rapidly gaining importance for server-side and network programming. Central components of EDP are event loops, which act as FIFO queues that are used by processes to store and dispatch messages received from other processes. In this talk we demonstrate that shared event loops are vulnerable to side-channel attacks, where a spy process monitors the loop usage pattern of other processes by enqueueing events and measuring the time it takes for them to be dispatched. Specifically, we exhibit attacks against two central event loops in Google's Chrome web browser: that of the I/O thread of the host process, which multiplexes all network events and user actions, and that of the main thread of the renderer processes, which handles rendering and Javascript tasks. For each of these event loops, we demonstrate how the usage pattern can be monitored with high resolution and low overhead, and we show how the extracted information can be leveraged for (1) identifying a web page during the loading phase (where we achieve recognition rates of up to 65% among 500 main pages from Alexa's Top sites), for (2) implementing cross origin covert channels (where we achieve transmission rates of up to 200 bit/s), and for (3) visually identifying user behavior such as mouse movements or keystrokes.


Time and place:
11:00 Lecture hall 1, level B
IMDEA Software Institute, Campus de Montegancedo
28223-Pozuelo de Alarcón, Madrid, Spain


Pablo Cañones

Tuesday, November 15, 2016

11:00 Lecture hall 1, level B

Pablo Cañones, PhD Student, IMDEA Software Institute

To Share or Not to Share: Security Analysis of Cache Replacement Policies

Abstract:

Modern computer architectures share physical resources between different programs in order to increase area-, energy-, and cost-efficiency. Unfortunately, sharing often gives rise to side channels that can be exploited for extracting or transmitting sensitive information. We currently lack techniques for systematic reasoning about this interplay between efficiency and performance. In particular, there is no established way for quantifying security properties of shared caches.

In this talk, we present a model that enables us to characterise important security properties of caches. Our model encompasses two aspects: (1) The amount of information that is absorbed by a cache, and (2) the amount of information that can effectively be extracted from the cache by an adversary. We use our model to compute both quantities for common cache replacement policies (FIFO, LRU, and PLRU) and to compare their isolation properties. We further show how our model for information extraction leads to an algorithm which we used to improve the bounds delivered by the CacheAudit static analyser.


Time and place:
11:00 Lecture hall 1, level B
IMDEA Software Institute, Campus de Montegancedo
28223-Pozuelo de Alarcón, Madrid, Spain


Srdjan Matic

Tuesday, November 8, 2016

11:00 Lecture hall 1, level B

Srdjan Matic, PhD Student, IMDEA Software Institute

Dissecting Tor Bridges: a Security Evaluation of Their Private and Public Infrastructures

Abstract:

Bridges are onion routers in the Tor Network whose IP addresses are not public. So far, no global security analysis of Tor bridges has been performed. Leveraging public data sources, and two known Tor issues, we perform the first systematic study on the security of the Tor bridges infrastructure. Our study covers both the public infrastructure available to all Tor users, and the previously unreported private infrastructure, comprising private nodes for the exclusive use of those who know their existence.

Our analysis of the public infrastructure is twofold. First, we examine the security implications of the public data in the CollecTor service, identifying several pieces of data that may be detrimental for the security of bridges. Then, we measure security relevant properties of public bridges. Our results show that the 55% of public bridges that carry clients are vulnerable to aggressive blocking; that 90% of bridge clients use default bridges that are trivial to identify; that the concurrent deployment of Pluggable Transports in bridges reduces the security of the most secure transports; and that running non-Tor services in the same host as a bridge may harm its anonymity.

To study the private infrastructure, we use an approach to discover 694 private bridges on the Internet and a novel technique to track bridges across IP changes. We are first to measure the size of the private bridge population (35% discovered bridges are private) and to report existence of infrastructures that use private proxies to forward traffic to backend bridges or relays. We use a novel clustering approach to analyze the different infrastructures using proxies and bridges, examining its hosting and security properties. We provide an extensive discussion on the security implications of our findings.


Time and place:
11:00 Lecture hall 1, level B
IMDEA Software Institute, Campus de Montegancedo
28223-Pozuelo de Alarcón, Madrid, Spain


Artem Khyzha

Thursday, November 3, 2016

11:00 Lecture hall 1, level B

Artem Khyzha, PhD Student, IMDEA Software Institute

Proving linearizability using partial orders

Abstract:

Linearizability is the commonly accepted notion of correctness for concurrent data structures. It requires that any execution of the data structure is justified by a linearization - a linear order on operations satisfying the data structure's sequential specification. Proving linearizability is often challenging because an operation's position in the linearization order may depend on future operations. This makes it very difficult to incrementally construct the linearization in a proof.

This talk will describe a proof technique that can handle data structures with such future-dependent linearizations. Our key idea is to incrementally construct not a single linear order of operations, but a partial order that describes multiple linearizations satisfying the sequential specification. This allows decisions about the ordering of operations to be delayed, mirroring the behaviour of data structure implementations. To illustrate our idea, I will describe the Time-Stamped queue algorithm and explain how to reason about its (future-dependent) linearizations in terms of partial orders.


Time and place:
11:00 Lecture hall 1, level B
IMDEA Software Institute, Campus de Montegancedo
28223-Pozuelo de Alarcón, Madrid, Spain


Maria Garcia De La Banda

Tuesday, October 25, 2016

11:00 Lecture hall 1, level B

Maria Garcia De La Banda, Visiting Faculty Professor, IMDEA Software Institute

Learning from learning solvers

Abstract:

Modern constraint programming solvers incorporate SAT-style learning, where the decisions that lead to a failure are recorded and used to reduce the search. While this can yield dramatic reductions in solving time, there are also cases where learning does not improve or even hinders performance. Unfortunately, the reasons for these differences in behaviour are not well understood in practice.

This talk describes some of the techniques we have used to cast some light on the practical behaviour of learning solvers, mainly by profiling their execution to measure the impact of the learnt clauses. I will show that analysing a solver's execution in this way can be useful not only to better understand its behaviour --- opening what is typically a black box --- but also to infer modifications to the original constraint model that can improve the performance of both learning and non-learning solvers.


Time and place:
11:00 Lecture hall 1, level B
IMDEA Software Institute, Campus de Montegancedo
28223-Pozuelo de Alarcón, Madrid, Spain


Bogdan Kulynych

Tuesday, October 18, 2016

11:00 Meeting room 302 (Mountain View), level 3

Bogdan Kulynych, Predoctoral Researcher, IMDEA Software Institute

Privacy-preserving statistics and machine learning

Abstract:

In this talk, Bogdan will discuss his experience as an intern at Google. The first part of the talk is going to be about the data science projects he was working on with Google Play and Ads, specifically, improving performance of uncertainty estimation in large-scale linear model predictions. In the second part, Bogdan is going to talk about some of the privacy-preserving technologies for statistics and machine learning that Google has published research on, like federated on-device learning and differential privacy.


Time and place:
11:00 Meeting room 302 (Mountain View), level 3
IMDEA Software Institute, Campus de Montegancedo
28223-Pozuelo de Alarcón, Madrid, Spain


John Gallagher

Tuesday, October 4, 2016

11:00 Meeting room 302 (Mountain View), level 3

John Gallagher, Professor, Roskilde University, Denmark and IMDEA Software Institute, Spain

Finite tree automata in Horn clause analysis and verification

Abstract:

Successful Horn clause derivations are finite trees and this leads to a straightforward correspondence between a set of Horn clauses and a finite tree automaton. In the talk the role of this connection in Horn clause analysis and verification is explained, including elimination of failing derivations and refinement of abstractions. We also briefly outline an optimised algorithm for determinisation of finite tree automata, which plays a role in this work.


Time and place:
11:00 Meeting room 302 (Mountain View), level 3
IMDEA Software Institute, Campus de Montegancedo
28223-Pozuelo de Alarcón, Madrid, Spain


Software Seminar Series (S3) - Spring 2016