IMDEA initiative

Home > Events > - Previous Invited Talks

Invited Talks - 2016

Emanuele D'Osualdo

Thursday, December 15, 2016

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

Emanuele D'Osualdo, Post-doctoral Researcher, TU Kaiserslautern, Germany

Automatic Analysis of Message Passing Concurrency

Abstract:

In this talk I will give an overview of my current research. The focus is on automatic analysis for message passing based concurrent systems, with an emphasis on dynamic communication topologies, i.e. systems where the components can connect and disconnect with each other dynamically. The distinctive trait of our approach to this problem is that the methods make full use of both, the structure of the programs as terms in a language, and the graph structure of the communication topology. This point of view unlocks the fruitful interaction of techniques from process algebra, type systems, automata theory and logics. I will present in some detail part of my PhD thesis work, which resulted in the type-theoretic definition of a fragment of the pi-calculus for which safety properties can be proved automatically. The types use novel techniques to reason about the shape that the communication topology can take at runtime. I will then give a brief account of ongoing projects pushing the approach further. The theme underlying all these projects is studying concurrent systems by analysing dynamic graphical structures capturing some salient aspect of their behaviour.


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


Fernando Pedone

Monday, December 12, 2016

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

Fernando Pedone, Professor, Università della Svizzera Italiana, Lugano, Switzerland

Scaling State Machine Replication

Abstract:

State machine replication (SMR) is a well-established approach to developing highly available services. In essence, the idea is that replicas deterministically execute the same sequence of client commands in the same order and in doing so transition through the same sequence of states and produce the same results. While SMR provides configurable fault tolerance, it does not scale performance: since every replica added to the system needs to execute all requests, throughput does not improve with the number of replicas. In this talk, I will present Scalable SMR (S-SMR), our efforts towards extending SMR to support both configurable fault tolerance and configurable performance (i.e., scaling out with the number of replicas). We have used S-SMR to develop a number of distributed services, including a scalable Zookeeper clone and a scalable social network application.


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


Avinash Sudhodanan

Friday, December 2, 2016

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

Avinash Sudhodanan, Junior researcher, Fondazione Bruno Kessler, Italy

Attack Patterns for Black-Box Security Testing of Multi-Party Web Applications

Abstract:

The advent of Software-as-a-Service (SaaS) has led to the development of Multi-Party Web Applications (MPWAs). MPWAs rely on core trusted third-party systems (e.g., payment servers, identity providers) and protocols such as Single Sign-On and Cashier-as-a-Service, to deliver business services to users. Motivated by the large number of attacks discovered in MPWAs and by the lack of a single, general-purpose, application-agnostic technique to support their discovery, we propose an automatic technique based on attack patterns for black-box security testing of MPWAs. Our approach stems from the observation that attacks against MPWAs share a number of similarities, even if the underlying protocols and services are different. First, we present a methodology in which security experts can create attack patterns from known attacks. Second, we present a security testing framework that leverages attack patterns to automatically generate attack test cases against a target MPWA. We created 7 attack patterns (targeting 6 different replay attacks and a CSRF attack) that corresponds to 13 prominent attacks from the literature, implemented our security testing framework on top of OWASP ZAP (a popular, open-source penetration testing tool) and discovered 21 previously-unknown vulnerabilities in many prominent MPWAs (e.g., developer.linkedin.com, pinterest.com, stripe checkout).


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


Daniel Larraz

Wednesday, November 30, 2016

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

Daniel Larraz, PhD Researcher, Universitat Politècnica de Catalunya (UPC), Spain

Scalable Program Analysis using Max-SMT

Abstract:

Recent developments on SMT solvers have become crucial to make program analysis techniques effective in practice. Despite their success, scalability is still an issue when applying these methods to large fragments of code. In order to address this problem, we propose a template-based (also known as constraint-based) approach using Max-SMT solvers. In particular, we present an automated compositional program verification technique for safety properties based on conditional inductive invariants. Our bottom-up program verification framework synthesizes and propagates preconditions of small program parts as postconditions for preceding program parts. The method recovers from failures when some precondition is not proved. In this talk we will provide an overview of the Max-SMT solving techniques and their application to compositional program analysis. These techniques have successfully been implemented within the VeryMax tool which currently can check safety, reachability and termination properties of C++ code.


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


Antonio Nappa

Tuesday, November 29, 2016

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

Antonio Nappa, Research Scientist, StealthSec Inc., España

RevProbe: Detecting Silent Reverse Proxies in Malicious Server Infrastructures

Abstract:

Web service operators set up reverse proxies to interpose the com- munication between clients and origin servers for load-balancing traffic across servers, caching content, and filtering attacks. Silent reverse proxies, which do not reveal their proxy role to the client, are of particular interest since malicious infrastructures can use them to hide the existence of the origin servers, adding an indi- rection layer that helps protecting origin servers from identification and take-downs. We present RevProbe, a state-of-the-art tool for automatically detecting silent reverse proxies and identifying the server infras- tructure behind them. RevProbe uses active probing to send re- quests to a target IP address and analyzes the responses looking for discrepancies indicating that the IP address corresponds to a reverse proxy. We extensively test RevProbe showing that it significantly outperforms existing tools. Then, we apply RevProbe to perform the first study on the usage of silent reverse proxies in both benign and malicious Web services. RevProbe identifies that 12% of mali- cious IP addresses correspond to reverse proxies, furthermore 85% of those are silent (compared to 52% for benign reverse proxies).


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


Francesco Zappa Nardelli

Friday, October 21, 2016

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

Francesco Zappa Nardelli, Research Scientist, INRIA Paris, France

Programming Languages and Concurrency: Still Tricky

Abstract:

We will review the possible approaches to defining memory models for programming languages, and will describe the C11 memory model. But we will go further: by leveraging the semantics of C11 low-level relaxed atomic accesses (which allows programmers to take full advantage of weakly-ordered memory operations) we will show that, among other dreadful consequences, the C11 standard does not permit many common source-to-source program transformations (such as expression linearisation and “roach motel” reorderings) that modern compilers perform and that are deemed to be correct. We will consider and evaluate a number of possible local fixes, some strengthening and some weakening the model. We will conclude with the remarkable and disturbing observation that, currently, there is no really satisfactory proposal for the semantics of a general-purpose shared-memory concurrent programming language.


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


Narseo Vallina-Rodriguez

Thursday, October 20, 2016

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

Narseo Vallina-Rodriguez, Assistant Research Professor and Research Scientist, IMDEA Networks, Spain and International Computer Science Institute (ICSI), USA

The ICSI Haystack: A Tool to Illuminate the Mobile Ecosystem

Abstract:

As a society we have come to rely upon our mobile phones for myriad daily tasks. It is striking how little insight we, as mobile users and researchers, have into the operation of our devices, apps and network, into how (or whether) they protect the information we entrust to them, and with whom they share it. The research community (including the speaker) have energetically used a variety of approaches to gain empirical understanding of the mobile device/network ecosystem; however, these techniques have had to make tradeoffs that affect either the scale, scope or granularity of measurements. This talk describes how we leverage ideas from this prior work to design and develop the ICSI Haystack: a user-space mobile traffic measurement platform that is comprehensive and localized to the device so that it overcomes the barriers of previous research efforts. The talk will demonstrate its utility to researchers and average users alike by discussing future research lines and providing three case studies: privacy leak detection, identifying previously unreported third-party tracking and advertising services, and characterizing how mobile apps use TLS in the wild.


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


Matthieu Perrin

Thursday, October 13, 2016

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

Matthieu Perrin, Post-doctoral Researcher, Technion, Israel Institute of Technology

Specification of shared objects in wait-free distributed systems

Abstract:

In large scale distributed systems, strong consistency criteria like sequential consistency and linearizability are often very expensive or even unachievable. This talk investigates the best ways to specify the objects that are still possible to implement in these systems. We assert that it is still possible to separate their specification in two complementary facets: an abstract data type that specifies the functional aspect of the operations and a weak consistency criterion that describes the level of quality of service ensured by the object in its distributed environment. We illustrate these concepts by an implementation in the D programming language: abstract data types are described by classes in the program and consistency criteria are taken from a list in the CODS library. We also draw up a map of the space of weak consistency criteria, organised around three families of primary criteria (state locality, eventual consistency and validity) and three families of secondary criteria (update consistency, pipelined consistency and serializability). Each secondary criterion strenghtens two primary criteria, but the three criteria can not be implemented together in considered systems. We also study the effects of causality on these families.


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


Valter Balegas

Tuesday, October 11, 2016

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

Valter Balegas, PhD Student, Universidade Nova de Lisboa, Portugal

IPA: Invariant-Preserving Applications for Weakly-consistent Replicated Databases

Abstract:

Storage systems based on Weak Consistency provide better availability and lower latency than systems that use Strong Consistency, especially in geo-replicated settings. However, under Weak Consistency, it is harder to ensure correctness of applications, because concurrent operations may conflict and lead to invariant violations. Recent proposals identify which operations can cause conflicts and coordinate their execution, but this can still result in high latency and low availability for these operations. We propose an alternative approach: invariant-preserving applications by design. It consists in tweeking operations in such a way that they run correctly under Weak Consistency. Our methodology is backed by a tool that allows application programmers to identify invariant violations and correct them, during development period. The evaluation of the approach shows that the modified operations incur in a small penalty during runtime, in comparison to their original unsafe implementation, but still outperform the state of the art solutions that use coordination for operations that may violate invariants.


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


Jesús Díaz Vico

Friday, October 7, 2016

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

Jesús Díaz Vico, Research Scientist, BEEVA, Spain

Anonymization and De-anonymization: With Great Power Comes Great Responsibility... or not?

Abstract:

As every aspect of our lives gets more dependent on technology and the Internet, it is becoming more necessary to protect our privacy. Very robust anonymity systems have been designed and developed towards this end. They are being adopted by a high number of users and are endorsed and enhanced by a large body of academic research. However, and regrettably, robust and irrevocable anonymity can be (and is being) used for dishonest purposes too. Besides the ethical controversy that this arises, it also penalizes people who really need and/or make good use of anonymity. In this talk, we review systems that attempt to address this issue without penalizing privacy, both as domain specific and general solutions, making use of cryptographic primitives like group signatures and blind signatures. In addition, and in order to maximize the practicality of these systems, we review proposals such as standard-like definitions and cryptographic libraries that could serve as technological foundation to build them. Finally, we point out interesting challenges for future research. One such line is the study of objective blacklisting for preventing abuse of authority when anonymity revocation is enabled. Other seemingly independent line is trust decentralization; however, its connection becomes apparent when realizing that decentralization may be essential to ensure that no abuse of power is possible.


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


Mooly Sagiv

Tuesday, September 27, 2016

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

Mooly Sagiv, Professor, Tel Aviv University, Israel

Ivy: Safety Verification by Interactive Generalization

Abstract:

Despite several decades of research, the problem of formal verification of infinite-state systems has resisted effective automation. We describe a system, Ivy, for interactively verifying safety of infinite-state systems. Ivy's key principle is that whenever verification fails, Ivy graphically displays a concrete counterexample to induction. The user then interactively guides generalization from this counterexample. This process continues until an inductive invariant is found. Ivysearches for universally quantified invariants, and uses a restricted modeling language. This ensures that all verification conditions can be checked algorithmically. All user interactions are performed using graphical models, easing the user's task. We describe our initial experience with verifying several distributed protocols. Joint work with Oded Padon, Ken McMillan, Aurojit Panda, and Sharon Shoham. Preliminary version appeared at PLDI'16.


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


Yuri Meshman

Monday, September 19, 2016

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

Yuri Meshman, PhD Student, Technion, Israel Institute of Technology

Pattern-based Synthesis of Synchronization for the C++ Memory Model

Abstract:

The C++ relaxed memory model is very challenging. The crucial task of writing correct and efficient low-level concurrent programs for C++ under this model is known to be very challenging: the model's complexity is such that it eludes even veteran systems programmers and requires the attention of formal semantics experts. To maintain efficiency, the programmer wants the most relaxed synchronization required to preserve correctness, and nothing more (even when it simplifies reasoning). Unfortunately, manually finding the right synchronization is extremely difficult, as it requires the programmer to reason about subtle interactions of the memory model. Our goal is to assist the programmer by automatically synthesizing the required synchronization. We will show an algorithm that exhaustively explores the traces of an input program $P$ under the C++ relaxed memory model, and looks for error traces --- traces which do not satisfy the correctness criteria. If our algorithm finds an error trace, it searches it for instances of \emph{violation patterns}, behaviors that may occur under C++ RMM but not under SC and that we know how to avoid, and then use \emph{Avoidance templates} which are strategies to synthesize \emph{memory order annotations} of memory instructions such as \code{load}, \code{store}, and \code{cas}. We successfully synthesized nontrivial memory order synchronization for several challenging concurrent algorithms, including a state of the art Read-Copy-Update (RCU) algorithm.


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


Svetlana Jakšić

Monday, September 12, 2016

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

Svetlana Jakšić, PhD Student, University of Novi Sad, Serbia

Types for Privacy and Memory Control

Abstract:

Type systems are a widely used techniques for programming languages analysis. They are used to avoid undesired behaviours (run-time type errors), which are specific for each language. In this talk I will show how types can be used to avoid errors in two languages. The first language is modelling distributed network with RDF data. Even though such data is meant for public exposure and its availability brings a great advantage to users of such data, not all data are produced for public usage. For example, RDF is often used to represent personal information and data from social networks. This gives rise to the question of privacy of data, since the lack of privacy protection mechanisms often discourages people from publishing RDF data. A type system can be used to verify absence of some privacy violations. The second language is modelling a core language of processes that communicate and synchronize through the copyless message passing paradigm and can throw exceptions. In this context, where the sharing of data and explicit memory allocation require controlled policies on the ownership of heap-allocated objects, special care must be taken when exceptions are thrown to prevent communication errors (arising from misaligned states of channel endpoints) and memory leaks (resulting from messages forgotten in endpoint queues). We have studied a type system guaranteeing some safety properties, in particular that well-typed processes are free from communication errors and do no leak memory even in presence of (caught) exceptions. The talk is based on the results presented in my thesis.


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


Michael Pradel

Wednesday, September 7, 2016

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

Michael Pradel, Research Group Leader, TU Darmstadt, Germany

Scalable Program Analyses for JavaScript-based Web Applications

Abstract:

JavaScript not only makes it easy to write concise code in short time, but also to introduce programming errors, many of which are hard to detect with traditional analyses. This talk presents two approaches to detect such errors. First, we present EventBreak, a performance-guided test generation technique to identify and analyze event handlers whose execution time gradually increases while using the application, making the application unresponsive. The key idea is to systematically search for pairs of events where triggering one event increases the execution time of the other event. Second, we present DLint, a dynamic analysis approach to check code quality rules in JavaScript. DLint consists of a generic framework and an extensible set of checkers that each address a particular rule. So far, we have formally described and implemented 28 checkers that address problems missed by state-of-the-art static approaches. Applying EventBreak and DLint to real-world web applications reveals various problems, including responsiveness and scalability problems that make applications unusable, and visible bugs on the web sites of IKEA, Hilton, eBay, and CNBC.


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


Antonio Faonio

Tuesday, September 6, 2016

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

Antonio Faonio, Post-doctoral Researcher, Aarhus University, Denmark

Fully Leakage-Resilient Signatures with Graceful Degradation

Abstract:

We construct new leakage-resilient signature schemes. Our schemes remain unforgeable against an adversary leaking arbitrary (yet bounded) information on the entire state of the signer (sometimes known as fully leakage resilience).
The main feature of our constructions, is that they offer a graceful degradation of security in situations where standard existential unforgeability is impossible. This property was recently put forward by Nielsen et al. (PKC 2014) to deal with settings in which the secret key is much larger than the size of a signature.


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


Wouter Lueks

Thursday, September 1, 2016

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

Wouter Lueks, PhD Student, Nijmegen, Netherlands

Distributed encryption and applications

Abstract:

Governments increasingly store and process huge quantities of data to combat crime, fraud, and terrorism with the aim of increasing security. However, the price is a loss of privacy. Fortunately, in some cases, it is possible to build cryptographic systems that achieve the security goals and at the same time protect the privacy of `the innocent'. One such system is distributed encryption.
Distributed encryption allows observers to record parties that behave suspiciously by creating ciphertext shares of their identities. These shares by themselves give no information about the party to whom they refer. They can only be combined to recover the identity of the recorded party when sufficient shares are available. This system can, for example, be used to find high-way truck-stop robbers without affecting the privacy of regular innocent road users.
In this talk, I will introduce the problem of uniting security and privacy, and describe our 2014 distributed encryption scheme, including a batched variant that is faster for small plaintext domains -- like license plates. I will also highlight some recent work that makes recovering encrypted identities several orders of magnitudes faster.


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


Peter Stuckey

Tuesday, July 19, 2016

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

Peter Stuckey, Professor, The University of Melbourne, Australia

Optimization Modelling for Software Developers, or How to convert procedural code to constraints!

Abstract:

Software developers are an ideal channel for the distribution of discrete optimization (DO) technology. Unfortunately, including even basic optimisation functionality in an application currently requires the use of an entirely separate paradigm with which most software developers are not familiar. We suggest an alternative interface to DO designed to overcome this barrier. The interface allows an optimisation problem to be defined in terms of procedures rather than decision variables and constraints. Optimisation is seamlessly integrated into a wider application through automatic conversion between this definition and a conventional model solved by an external solver.
The core of the method is translating procedural object oriented code into constraints. This translation is also useful for other applications such as symbolic execution of the code, e.g. in Congolic testing. We discuss how to create the best translation of procedural code, better than existing DO and SMT approaches, and how we can translate bounded loops more effectively. Finally we briefly describe a global constraint for reaching definitions, which encapsulates the essential problem of converting procedural code to constraints.
This work is joint with Kathryn Francis.


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


Toby Murray

Tuesday, July 5, 2016

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

Toby Murray, Lecturer, The University of Melbourne, Australia

Building Highly-Secure Systems at Reasonable Cost -- Branching Out with Formal Verification

Abstract:

The past decade has witnessed a sea change in the perception of formal software verification. For instance, the microkernel seL4, whose correctness and security have been formally verified, is routinely cited to argue the improving power of verification for critical software. However, formal verification remains a long way from influencing software development practice, not least because it remains poorly integrated with programming languages.
In this talk I argue that, just as domain specific programming languages improve programmer productivity, verification can be greatly simplified by programming critical software in special purpose languages designed for verification. I present some recent work applying this idea to develop formally verified file systems code, where we developed the Cogent, a purely functional language with a self-certifying compiler to C. I will also present some early work applying these ideas to develop security-critical systems in collaboration with the Australian Government's Defence Science and Technology Group. Here, by carefully designing the programming language to make security a first-class concern, we aim to reduce the cost of verifying system security to near-zero, while achieving unprecedented security guarantees. Finally, I draw on this collaboration to explain the surprising interplay between security verification and human factors that we are only just beginning to understand.


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


Jens Grossklags

Wednesday, June 1, 2016

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

Jens Grossklags, Assistant Research Professor, University of Pennsylvania, USA

Given Enough Eyeballs, All Bugs Are Shallow? An Empirical Study of the Wooyun and HackerOne Web Vulnerability Discovery Ecosystems

Abstract:

In recent years, many organizations have established bounty programs that attract white hat hackers who contribute vulnerability reports of web systems. In this talk, I will present findings about two representative web vulnerability discovery ecosystems (Wooyun and HackerOne) and discuss their characteristics, trajectory, and impact. Both ecosystems include large and continuously growing white hat communities which have provided significant contributions to organizations from a wide range of business sectors. I will also present results about vulnerability trends, response and resolve behaviors, and reward structures of participating organizations. The analysis based on the HackerOne dataset reveals that a considerable number of organizations exhibit decreasing trends for reported web vulnerabilities. With a regression study, I will also show that monetary incentives have a significantly positive correlation with the number of vulnerabilities reported. Finally, I will make recommendations aimed at increasing participation by white hats and organizations in such ecosystems. (The talk is based on joint work with Mingyi Zhao, Aron Laszka, Thomas Maillart, and Peng Liu.)


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


Alessio Gambi

Friday, May 27, 2016

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

Alessio Gambi, Post-doctoral Researcher, Saarland University, Germany

O!Snap: Cost-Efficient Testing in the Cloud

Abstract:

Porting a software testing execution environment to a cloud-based infrastructure can lead to significant test speedup and cost savings. However, distributing tests to new machines requires costly environment setup, and cloud infrastructures may have complex cost models. Ignoring these issues may lead to limited speedup or to unexpected cost increase. In this talk, I present “O!Snap”, a novel technique to automatically deploy and schedule tests on the cloud in a cost-efficient way. O!Snap uses a pipeline of opportunistic snapshotting, which reduces the effort to setup the testing environment, and test schedule planning, which schedules test executions according to their dependencies and optimizes the resources consumption to limit costs


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


Patrick Cousot

Tuesday, May 24, 2016

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

Patrick Cousot, Full Professor, New York University

The hierarchy of analytic semantics of weakly consistent parallelism

Abstract:

Most definitions of weak consistency models (WCM) in the literature are specific to one style of semantics description (e.g. transition systems), one language (e.g. x86 assembly), and one computer architecture (e.g. ARM). This makes generality a difficult goal: each verification, static analysis, or transformation technique has to be reinvented if any of these three parameters changes.
In contrast, our work provides a wide variety of semantics definitions, all under the same framework. More precisely, we view the semantics of a parallel program P under a WCM as two-fold:
- a computation part, i.e., an architecture and language independent instruction semantics;
- a communication part, i.e., a set of constraints on communications.
More precisely a WCM is the intersection (in the formal sense) of its computation and communication parts. Its computation part is said to be anarchic since it imposes no constraint on communications. To describe its communication part, we choose to use the cat domain specific language, which allows a user to list a set of constraints on communication in a concise manner.
We define a hierarchy of computation semantics from ground valued to (un)interpreted symbolic execution, from interleaved to true parallelism, from event to state-based, from trace to transition-based, etc. Each level of the hierarchy is an abstraction of the bottom computation semantics.
Although the abstractions in the hierarchy do lose information in general (for example w.r.t. program termination), they do not loose any information w.r.t. the bottom semantics. Moreover, all the abstractions preserve the cat specification of communications, viz. a given cat specification forbids exactly the same behaviours on any two abstractions.
This allows us to provide a wide variety of semantics definitions: each and every computation semantics (whether state-based or not, trace-based or not) can be married to any communication semantics as described by a cat specification. Thus we can provide, for example, two (or more) definitions of TSO, Power, or ARM, adjusted to the taste of the user, or the practicality w.r.t. verification techniques.


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


Christopher Meiklejohn

Wednesday, May 18, 2016

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

Christopher Meiklejohn, PhD Student, KU Leuven, Belgium

Lasp: A Language For Distributed, Declarative, Edge Computation

Abstract:

Consistency is hard and coordination is expensive. As we move into the world of connected 'Internet of Things' style applications, or large-scale mobile applications, devices have less power, periods of limited connectivity, and operate over unreliable asynchronous networks. This poses a problem with shared state: how do we handle concurrent operations over shared state, while clients are offline, and ensure that values converge to a desirable result without making the system unavailable?
We look at a new programming model, called Lasp. This programming model combines distributed convergent data structures with a dataflow execution model designed for distribution over large-scale applications. This model supports arbitrary placement of processing node: this enables the user to author applications that can be distributed across data centers and pushed to the edge. In this talk, we will focus on the design of the language and show a series of sample applications.


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


Aishwarya Thiruvengadam

Friday, May 6, 2016

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

Aishwarya Thiruvengadam, PhD Student, University of Maryland, USA

10-round Feistel is indifferentiable from an ideal cipher

Abstract:

We revisit the question of constructing an ideal cipher from a random oracle. Coron et al.~(Journal of Cryptology, 2014) proved that a 14-round Feistel network using random, independent, keyed round functions is indifferentiable from an ideal cipher, thus demonstrating the feasibility of such a construction. Left unresolved is the best possible efficiency of the transformation. We improve upon the result of Coron et al. and show that 10 rounds suffice. This is joint work with Dana Dachman-Soled and Jonathan Katz.


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


Reinhard Wilhelm

Tuesday, April 26, 2016

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

Reinhard Wilhelm, Professor, Saarland University, Germany

Toward Compact Abstract Domains for Pipelines

Abstract:

Hard real-time systems require programs to react on time. Static timing analysis derives timing guarantees by analyzing the behavior of programs running on the underlying execution platform. Efficient abstractions have been found for the analysis of caches. Unfortunately, this is not the case for the analysis of processor pipelines. Pipeline analysis typically uses an expensive powerset domain of concrete pipeline states. Therefore, pipeline analysis is the most complex part of timing analysis. We propose a compact abstract domain for pipeline analysis. This pipeline analysis determines the minimal progress of instructions in the program through the pipeline.
We give a concrete semantics for an in-order pipeline, which forms the basis for an abstract semantics. On the way, we found out that in-order pipelines are not guaranteed to be free of timing anomalies, i.e. local worst decisions do not lead to the global worst case. We prove this by giving an example. A major problem is how to find an abstract semantics that guarantees progress on the abstract side. It turns out that monotonicity on the partial progress order is sufficient to guarantee this.
Joint work with Sebastian Hahn and Jan Reineke.


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


Hugo Krawczyk

Tuesday, March 29, 2016

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

Hugo Krawczyk, Research Scientist, IBM T. J. Watson Research Center, USA

Protecting our Protectors: Armoring Passwords Against Server Compromise (Or: How to Protect Your Bitcoin Wallet Online)

Abstract:

The amount and value of information we store in computers, servers or the collective cloud keeps growing while the ways of protecting it are mostly limited by the strength of a memorizable password. Even when the valuable information is stored with strong security, retrieval authorization often boils down to knowing a weak password. In spite of some protection being added against online attacks via two-factor authentication tools, the main vulnerability of passwords, and of the information they protect, remains offline dictionary attacks against compromised servers. Indeed, loss of millions of passwords to such attacks are common news nowadays. A natural approach to strengthening the protection of data against server compromise is to distribute storage among a set of servers, for example using a secret sharing scheme. However, how does the user access these servers? Using the same password in each of these servers makes the off-line password recovery attack even worse (as it can be performed against any of these servers) while memorizing a different password for each server is impractical and further weakens the password. In this talk I will describe a practical (t,n)-PPSS (Password-Protected Secret Sharing) scheme in which a user Alice stores secret information among n servers so that she can later recover the information solely based on her password. The security requirement is similar to a (t,n)-threshold secret sharing, i.e., Alice can recover her secret as long as she can communicate with t+1 honest servers but an attacker gaining access to t servers cannot learn any information about the secret (and the password). In particular, the system is secure against offline password attacks by an attacker controlling up to t servers. The presented PPSS scheme is round-optimal, requiring just one message from user to server and from server to user, is computationally very efficient and is proved secure in the password-only setting where users are not assumed to carry, or have access to, an authenticated public key. As an important application we build the first single-round password-only Threshold-PAKE protocol in the CRS and ROM models for arbitrary (t,n) parameters with no PKI requirements for any party (clients or servers) and no inter-server communication. Time permitting I will mention some other recent work on two-factor authentication where an auxiliary device is used to strengthen password authentication not only against on-line attacks but also against server compromise (without assuming PKI). The talk is based on works with co-authors Stas Jarecki, Aggelos Kiayas, Jiayu Xu, Nitesh Saxena and Maliheh Shirvanian.


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


Reynald Affeldt

Thursday, March 17, 2016

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

Reynald Affeldt, Senior Research Scientist, National Institute of Advanced Industrial Science and Technology, Japan

Formalization of Error-correcting Codes: from Hamming to Modern Coding Theory

Abstract:

By adding redundancy to transmitted data, error-correcting codes(ECCs) make it possible to communicate reliably over noisy channels. Minimizing redundancy and (de)coding time has driven much research, culminating with Low-Density Parity-Check (LDPC) codes. At first sight, ECCs may be considered as a trustful piece of computer systems because classical results are well-understood. But ECCs are also performance-critical so that new hardware calls for new implementations whose testing is always an issue. Moreover, research about ECCs is still flourishing with papers of ever-growing complexity. In order to provide means for implementers to perform verification and for researchers to firmly assess recent advances, we have been developing a formalization of ECCs using the Coq proof-assistant and the Mathematical Components library. We report on the formalization of linear ECCs, duly illustrated with a theory about the celebrated Hamming codes and the verification of the sum-product algorithm for decoding LDPC codes. (Joint work with Jacques Garrigue, Nagoya University)


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


Adam Morrison

Tuesday, February 16, 2016

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

Adam Morrison, Post-doctoral Researcher, Technion, Israel Institute of Technology

Limitations of Highly-Available Eventually-Consistent Data Stores

Abstract:

Modern replicated data stores aim to provide high availability, by immediately responding to client requests, often by implementing objects that expose concurrency. Such objects, for example, multi-valued registers (MVRs), do not have sequential specifications. This talk explores a recent model for replicated data stores that can be used to precisely specify causal consistency for such objects, and liveness properties like eventual consistency, without revealing details of the underlying implementation. The model is used to prove the following results: - An eventually consistent data store implementing MVRs cannot satisfy a consistency model strictly stronger than observable causal consistency (OCC). OCC is a model somewhat stronger than causal consistency, which captures executions in which client observations can use causality to infer concurrency of operations. This result holds under certain assumptions about the data store. - Under the same assumptions, an eventually consistent and causally consistent replicated data store must send messages of size linear in the size of the system: If S objects, each Ω(lg K)-bit in size, are supported by N replicas, then there is an execution in an Ω(min{N,S} K)-bit message is sent. (Based on joint work with Hagit Attiya and Faith Ellen.)


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


Fernando Pérez González

Monday, February 8, 2016

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

Fernando Pérez González, Full Professor, University of Vigo, Spain

Adversarial Signal Processing

Abstract:

Signal Processing has successfully become an instrumental discipline in addressing the challenges posed by the digital world. An enormous array of applications have emerged that make use of the theory and algorithms developed in several decades of research. However, most of those applications were developed having honest users in mind. Due to rising concerns about security and privacy, and the popularity of cloud-centric services, it has only been recently that different communities in the field have started rethinking designs to account for the presence of a (malicious) adversary. Interestingly, research in these communities has frequently been carried out with little or no mutual interactions. It is not surprising then that similar problems have been solved independently in contiguous areas, with a lack of a unifying view that could benefit from the power of generalization. The aim of this talk is to present the basic theory of adversarial signal processing, with motivating examples taken from the fields of watermarking, multimedia forensics, traffic analysis, intrusion detection, biometrics, cognitive radio, etc. We will focus on adversarial hypothesis testing, which is arguably the best understood topic. As a fundamental approach we will show how to use game theory to model the available strategies to both defender and adversary. In some cases of interest, it is possible to find an equilibrium of the game which gives the optimum strategies for both parties and the performance that each can achieve. One interesting instance where such equilibrium exists is the so-called “source identification game”, which has applications in media forensics, biometrics, network traffic analysis and fraud detection, to name a few. One of the drawbacks of designing an information processing system under the assumption that an adversary is present is that the solutions generally lead to very conservative designs, which in turn yield a bad performance when the adversary is not there. A possibility, to overcome such a problem, is to run a detection meta-test, aiming at detecting the presence of the adversary. We will present some recent results in the design of a meta-detector aiming at distinguishing malicious queries which are submitted as part of a sensitivity attack, from normal queries submitted by non-malevolent users.


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


Jacques-Henri Jourdan

Thursday, January 14, 2016

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

Jacques-Henri Jourdan, PhD Student, INRIA

Verasco: A Formally Verified C Static Analyzer

Abstract:

This talk will present the design and soundness proof of Verasco, a formally verified static analyzer for most of the ISO C99 language (excluding recursion and dynamic allocation), developed using the Coq proof assistant. Verasco aims at establishing the absence of run-time errors in the analyzed programs. It enjoys a modular architecture that supports the extensible combination of multiple abstract domains, both relational and non-relational. It include a memory abstract domain, an abstract domain of arithmetical symbolic equalities, an abstract domain of intervals, an abstract domain of arithmetical congruences and an octagonal abstract domain.
Verasco integrates with the CompCert formally-verified C compiler so that not only the soundness of the analysis results is guaranteed with mathematical certitude, but also the fact that these guarantees carry over to the compiled code.


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


Pablo Picazo-Sanchez

Tuesday, January 12, 2016

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

Pablo Picazo-Sanchez, PhD Student, U Carlos III

Secure Publish-Subscribe Protocols for Heterogeneous Medical Wireless Networks

Abstract:

Security and privacy issues in medical Wireless Body Area Networks (WBANs) constitute a major unsolved concern because of the challenges posed by the scarcity of resources in WBAN devices and the usability restrictions imposed by the healthcare domain. In this talk, a recent published proposal for WBAN architecture based on the well-known publish-subscribe paradigm is presented. On this architecture, sensors are able to encrypt and decrypt personal data using both private cryptography and Attribute Based Encryption (ABE) and thus guarantee confidentiality and fine-grained access control.


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


Invited Talks - 2015