IMDEA initiative

Home > Events > Software Seminar Series

Software Seminar Series - Winter 2017

German Delbianco

Tuesday, February 28, 2017

10:45am Meeting room 302 (Mountain View), level 3

German Delbianco, PhD Student, IMDEA Software Institute

Concurrent Data Structures Linked in Time

Abstract:

Arguments about correctness of a concurrent data structure are typically carried out by using the notion of linearizability and specifying the linearization points of the data structure's procedures. Such arguments are often cumbersome as the linearization points' position in time can be dynamic (depend on the interference, run-time values and events from the past, or even future), non-local (appear in procedures other than the one considered), and whose position in the execution trace may only be determined after the considered procedure has already terminated. In this talk I will present a new method, based on a separation-style logic, for reasoning about concurrent objects with such linearization points. We embrace the dynamic nature of linearization points, and encode it as part of the data structure's auxiliary state, so that it can be dynamically modified in place by auxiliary code, as needed when some appropriate run-time event occurs. We have named the idea linking-in-time, because it reduces temporal reasoning to spatial reasoning. For example, modifying a temporal position of a linearization point can be modelled similarly to a pointer update in separation logic. Furthermore, the auxiliary state provides a convenient way to concisely express the properties essential for reasoning about clients of such concurrent objects. In order to illustrate our approach, I will illustrate its application to verify (mechanically in Coq) an intricate optimal snapshot algorithm, due to Jayanti.


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


Arthur Blot

Tuesday, February 21, 2017

10:45am Meeting room 302 (Mountain View), level 3

Arthur Blot, Research Intern, IMDEA Software Institute

Compositional Synthesis of Leakage Resilient Programs

Abstract:

A promising approach to defend against side channel attacks is to build programs that are leakage resilient, in a formal sense. One such formal notion of leakage resilience is the n-threshold-probing model proposed in the seminal work by Ishai et al. In a recent work, Eldib and Wang have proposed a method for automatically synthesizing programs that are leakage resilient according to this model, for the case n = 1. In this paper, we show that the n-threshold-probing model of leakage resilience enjoys a certain compositionality property that can be exploited for synthesis. We use the property to design a synthesis method that efficiently synthesizes leakage-resilient programs in a compositional manner, for the general case of n > 1. We have implemented a pro- totype of the synthesis algorithm, and we demonstrate its effectiveness by synthesizing leakage-resilient versions of benchmarks taken from the literature.


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


Srdjan Matic

Tuesday, February 14, 2017

10:45am Lecture hall 1, level B

Srdjan Matic, PhD Student, IMDEA Software Institute

Active Techniques for Revealing and Analyzing the Security of Hidden Servers

Abstract:

In the last years we have witnessed a boom in the use of techniques and tools that provide anonymity. Such techniques and tools are used by clients that want their communication to stay anonymous or to access censored content, as well as by administrators to hide the location of their servers. All those activities can be easily performed with the support of an anonymity network. An important component of an anonymity network is the hidden server, a machine whose IP address is kept secret. Such hidden servers are the target of research of this dissertation; more specifically, we focus on different types of hidden servers used in the Tor anonymity network. Our work comprises two parts, one dealing with Tor hidden services and the other one about bridges. In the first part we illustrated novel approaches that we developed for analyzing the security and revealing the location of hidden servers. We demonstrate our technique by implementing it in a tool, that later we used for deanonymizing over 100 real hidden services. In the second part, we perform the first systematic study of the Tor bridge infrastructure. Our study covers both the public bridge infrastructure available to all Tor users, and the previously unreported private bridge infrastructure, comprising private nodes for the exclusive use of those who know about their existence. Our results show how the public bridge ecosystem with clients is stable and those bridges rarely change their IP address. Furthermore we discuss the security implication of public datasets that can be leverage for recovering addresses of bridges, and how track a bridge across IP changes.


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


Pedro Valero

Tuesday, January 31, 2017

10:45am Lecture hall 1, level B

Pedro Valero, PhD Student, IMDEA Software Institute

A Language-theoretic View on Network Protocols

Abstract:

Input validation is the first line of defense against malformed or malicious inputs. It is therefore critical that the validator (which is often part of the parser) is free of bugs. To build dependable input validators, we propose using parser generators for context-free languages. In the context of network protocols, various works have pointed at context-free languages as falling short to specify precisely or concisely common idioms found in protocols. We review those assessments and perform a rigorous, language-theoretic analysis of several common protocol idioms. We then demonstrate the practical value of our findings by developing a modular, robust, and efficient input validator for HTTP relying on context-free grammars and regular expressions.


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


Joaquín Arias Herrero

Tuesday, January 24, 2017

10:45am Lecture hall 1, level B

Joaquín Arias Herrero, PhD Student, IMDEA Software Institute

Tabled CLP for Reasoning over Stream Data

Abstract:

The interest in reasoning over stream data is growing as quickly as the amount of data generated. Our intention is to change the way stream data is analyzed. This is an important problem because we constantly have new sensors collecting information, new events from electronic devices and/or from customers and we want to reason about this information. For example, information about traffic jams and customer orders could be used to define a deliverer route. When there is a new order or a new traffic jam, we usually restart from scratch in order to recompute the route. However, if we have several deliveries and we analyze the information from thousands of sensors, we would like to reduce the computation requirements, e.g. reusing results from the previous computation. Nowadays, most of the applications that analyze stream data are specialized for specific problems (using complex algorithms and heuristics) and combine a computation language with a query language. As a result, when the problems become more complex (in e.g. reasoning requirements), in order to modify the application complex and error prone coding is required. We propose a framework based on a high-level language rooted in logic and constraints that will be able to provide customized services to different problems. The framework will discard wrong solutions in early stages and will reuse previous results that are still consistent with the current data set. The use of a constraint logic programming language will make it easier to translate the problem requirements into the code and will minimize the amount of re-engineering needed to comply with the requirements when they change.


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


Luca Nizzardo

Tuesday, January 17, 2017

10:45am Lecture hall 1, level B

Luca Nizzardo, PhD Student, IMDEA Software Institute

Multi-Key Homomorphic Authenticators

Abstract:

Homomorphic authenticators (HAs) enable a client to authenticate a large collection of data elements $m_1, ... , m_t$ and outsource them, along with the corresponding authenticators, to an untrusted server. At any later point, the server can generate a short authenticator $\sigma_{f,y}$ vouching for the correctness of the output $y$ of a function $f$ computed on the outsourced data, i.e., $y = f(m_1, ... , m_t)$. Recently researchers have focused on HAs as a solution, with minimal communication and interaction, to the problem of delegating computation on outsourced data. The notion of HAs studied so far, however, only supports executions (and proofs of correctness) of computations over data authenticated by a single user. Motivated by realistic scenarios (ubiquitous computing, sensor networks, etc.) in which large datasets include data provided by multiple users, we study the concept of multi-key homomorphic authenticators. In a nutshell, multi-key HAs are like HAs with the extra feature of allowing the holder of public evaluation keys to compute on data authenticated under different secret keys. In this paper, we introduce and formally define multi-key HAs. Secondly, we propose a construction of a multi-key homomorphic signature based on standard lattices and supporting the evaluation of circuits of bounded polynomial depth. Thirdly, we provide a construction of multi-key homomorphic MACs based only on pseudorandom functions and supporting the evaluation of low-degree arithmetic circuits. Albeit being less expressive and only secretly verifiable, the latter construction presents interesting efficiency properties.


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