IMDEA initiative

Home > Events > Invited Talks

Invited Talks

Romain Gay

Wednesday, April 19, 2017

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

Romain Gay, PhD Student, ENS Paris

Improved Dual System ABE in Prime-Order Groups via Predicate Encodings

Abstract:

We present a modular framework for the design of efficient adaptively secure attribute-based encryption (ABE) schemes for a large class of predicates under the standard k-Lin assumption in prime-order groups; this is the first uniform treatment of dual system ABE across different predicates and across both composite and prime-order groups. Via this framework, we obtain concrete efficiency improvements for several ABE schemes. Our framework has three novel components over prior works: (i) new techniques for simulating composite-order groups in prime-order ones, (ii) a refinement of prior encodings framework for dual system ABE in composite-order groups, (iii) an extension to weakly attribute-hiding predicate encryption (which includes anonymous identity-based encryption as a special case). The talk will include some details and intuition from a previous work on the same topic: "Communication Complexity of Conditional Disclosure of Secrets and Attribute-Based Encryption".


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


Azalea Raad

Thursday, March 30, 2017

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

Azalea Raad, PhD Student, Imperial College, London

Local Reasoning for Concurrency, Distribution and Web Programming

Abstract:

In this talk I will present my research in developing local reasoning techniques in both concurrent and sequential settings. On the concurrency side, I’ll present my work on the program logic of CoLoSL (Concurrent Local Subjective Logic) and its application to various fine-grained concurrent algorithms. A key difficulty in verifying concurrent programs is reasoning compositionally about each thread in isolation. CoLoSL is the first program logic to introduce the general composition and framing of interference relations (describing how shared resources may be manipulated by each thread) in the spirit of resource composition and framing in separation logic. This in turn enables local reasoning and allows for more concise specifications and proofs. I will then present preliminary work on extending CoLoSL to reason about distributed database applications running under the snapshot isolation (SI) consistency model. SI is a commonly used consistency model for transaction processing, implemented by most distributed databases. The existing work focuses on the SI semantics and verification techniques for client-side applications remain unexplored. To fill this gap, I look into extending CoLoSL towards a program logic for client-side reasoning under SI. On the sequential side, I’ll briefly discuss my work on specification and verification of web programs. My research in this area include: a compositional specification of the DOM (Document Object Model) library in separation logic; integrating this DOM specification with the JaVerT (JavaScript Verification Toolchain) framework for automated DOM/JavaScript client verification; as well as ongoing work towards extending JaVerT to reason about higher-order JavaScript programs.


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


Andreas Rossberg

Friday, March 24, 2017

11:00am Lecture hall 1, level B

Andreas Rossberg, Software Engineer, Google

Bringing the Web up to Speed with WebAssembly

Abstract:

The maturation of the Web platform has given rise to sophisticated and demanding Web applications such as interactive 3D, audio and video software, and games. Efficiency and security of mobile code on the Web has become more important than ever. Yet JavaScript as the universal language of the Web is poorly equipped to meet these requirements, especially as a compilation target. Engineers from all major browser vendors have risen to the challenge and collaboratively designed a portable low-level byte code called WebAssembly. It offers compact representation, efficient validation and compilation, and safe low-overhead execution. Rather than committing to a specific programming model, WebAssembly is an abstraction over modern hardware, making it language-, hardware-, and platform-independent, with use cases beyond just the Web. WebAssembly is the first industrial-strength language that has been designed with a formal semantics from the start. This talk will present the motivation, design and formal semantics of WebAssembly and preliminary experience with implementations.


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


Sebastian Mödersheim

Thursday, March 23, 2017

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

Sebastian Mödersheim, Associate Professor, Technical University of Denmark

Alpha-Beta-Privacy -- Defining Privacy is Supposed to be Easy

Abstract:

So far, formally specifying privacy goals is not trivial. The most widely used approach in formal methods is based on the static equivalence of frames in the applied pi-calculus, basically asking whether or not the intruder is able to distinguish two given worlds. A subtle question is how we can be sure that we have specified all pairs of worlds to properly reflect our intuitive privacy goal. To address this problem, we introduce a novel and declarative way to specify privacy goals, called "alpha-beta privacy", and relate it to static equivalence. Our approach is based on specifying two formulae alpha and beta in first-order logic with Herbrand universes, where alpha reflects the intentionally released information and beta includes the actual cryptographic ("technical") messages the intruder can see. Alpha-beta privacy means that the intruder cannot derive any "non-technical" statement from beta that he cannot derive from alpha already. We describe by a variety of examples how this notion can be used in practice. Even though alpha-beta privacy does not directly contain a notion of distinguishing between worlds, there is a close relationship to static equivalence of frames that we investigate formally. This allows us to justify (and criticize) the specifications that are currently used in verification tools, and obtain partial tool support for alpha-beta privacy. Finally this gives a fresh look at privacy as classical safety properties (i.e., reachability problems) of a system. (Joint work with Luca Viganò and Thomas Gross)


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


Alberto Lopez

Wednesday, March 15, 2017

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

Alberto Lopez, General Secretary, Escuela Universitaria de Diseño, Innovación y Tecnología

Software research activities in Design at ESNE

Abstract:

Research activities in design, often end up in complex software development tasks. Security related with User eXperience in bank applications, usability in new electronic devices (some of them wearable), ethic issues in vehicle active safety systems, advanced render presentations of clothes for e-commerce purposes or AI algorithms in video games software are some examples of it. ESNE is currently working in several áreas of design (Fashion, Interior, Video Games, Graphic, Multimedia and Product Design) with some research activities is these fields. This presentation will review them, focussing on software related problems.


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 Riofrio

Friday, March 10, 2017

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

Daniel Riofrio, Post-doctoral Researcher, University of New Mexico, USA

The Presidential Elections in Ecuador during the digital era

Abstract:

In his talk, Daniel will go over the motivations that lead to this research, the protocol he has been following to measure elections, the tools been used to collect data, some initial findings and future work.


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


Ignacio Fabregas

Thursday, March 09, 2017

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

Ignacio Fabregas, Post-doctoral Researcher, Universidad Complutense de Madrid, Spain

Logics for Process Semantics

Abstract:

In the setting of the modal logic that characterizes modal refinement over modal transition systems, Boudol and Larsen showed in 1992 that the formulae for which model checking can be reduced to preorder checking, that is, the characteristic formulae, are exactly the consistent and prime ones. This talk present the extension of that classical result from a purely logical point of view, but with an eye over the behavioural preorders in van Glabbeek’s linear-time branching-time spectrum. It will be shown general and sufficient conditions guaranteeing that characteristic formulae are exactly the consistent and prime ones will be shown. As a first step towards the general result, the property is translated to the scenario of covariant-contravariant simulations over label transition systems. Finally, there will be a look into a promising direction that the speaker is exploring based in one recent paper of Legay and Fahrenberg also inspired by the foundational paper of Boudol and Larsen.


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


Alfredo Pironti

Friday, March 03, 2017

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

Alfredo Pironti, Researcher, IOActive

15 Years of Broken Encrypted Emails... and We're Still Doing It Wrong

Abstract:

Starting from a research paper of 2001, we show how OpenPGP encryption of emails is fundamentally broken. We show how an attacker can get hold of sensitive email content by tampering with email data that the user would expect to be protected. We apply this attack against PGP-enabled email addresses used to report vulnerabilities to software vendors -- and we get more than 50% of the submitted reports. Based on currently available information, we believe that recent End-to-End secure email projects still suffer from these same known issues.


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


Rupak Majumdar

Friday, February 24, 2017

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

Rupak Majumdar, Scientific Director, Max Planck Institute for Software Systems

Hitting families of schedules

Abstract:

We consider the following basic task in the testing of concurrent systems. The input to the task is a partial order of events, which models actions performed on or by the system and specifies ordering constraints between them. The task is to determine if some scheduling of these events can result in a bug. The number of schedules to be explored can, in general, be exponential. Empirically, many bugs in concurrent programs have been observed to have small bug depth; that is, these bugs are exposed by every schedule that orders some d specific events in a particular way, irrespective of how the other events are ordered, and d is small compared to the total number of events. To find all bugs of depth $d$, one needs to only test a d-hitting family of schedules: we call a set of schedules a $d$-hitting family if for each set of d events, and for each allowed ordering of these events, there is some schedule in the family that executes these events in this ordering. The size of a d-hitting family may be much smaller than the number of all possible schedules, and a natural question is whether one can find $d$-hitting families of schedules that have small size. In general, finding the size of optimal d-hitting families is hard, even for d=2. We show, however, that when the partial order is a tree, one can explicitly construct d-hitting families of schedules of small size. When the tree is balanced, our constructions are polylogarithmic in the number of events. (Joint work with Dmitry Chistikov and Filip Niksic)


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


Hongseok Yang

Monday, February 13, 2017

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

Hongseok Yang, Professor, University of Oxford, UK

Probabilistic Programming

Abstract:

Probabilistic programming refers to the idea of using standard programming constructs for specifying probabilistic models and employing generic inference algorithms for answering various queries on these models. Although this idea itself is not new and was, in fact, explored by several programming-language researchers in the early 2000, it is only in the last few years that probabilistic programming has gained a large amount of attention among researchers in machine learning and programming languages, and that serious probabilistic programming languages (such as Anglican, Church, Infer.net, PyMC, Stan, and Venture) started to appear and have been taken up by a nontrivial number of users. My talk has two goals. One is to introduce probabilistic programming to the programming-language audience. The other is to explain a few lessons that I learnt about probabilistic programming from my machine learning colleagues in Oxford. They have been developing a high-order call-by-value probabilistic programming language called Anglican, and through many discussions and close collaborations, they taught me why people in machine learning cared about probabilistic programming and pointed out new interesting research directions. These lessons had huge influence on how I think about probabilistic programming. I will try to explain the lessons through their influence on my ongoing projects, which aim at optimising probabilistic programs using techniques from programming languages and providing denotational semantics of high-order probabilistic programs. My talk will be based on joint work with Sam Staton, Jan-Willem van de Meent, Frank Wood (Oxford), Diane Gallois-Wong (ENS), Chris Heunen (Edinburgh), Ohad Kammar (Cambridge) and David Tolpin (Paypal).


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


Goran Doychev

Tuesday, February 07, 2017

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

Goran Doychev, Researcher, Independent Researcher

Rigorous Analysis of Software Countermeasures against Cache Attacks

Abstract:

CPU caches introduce variations into the execution time of programs that can be exploited by adversaries to recover private information about users or cryptographic keys. Establishing the security of countermeasures against this threat often requires intricate reasoning about the interactions of program code, memory layout, and hardware architecture and has so far only been done for restricted cases. In this talk, I will present novel techniques that provide support for bit-level and arithmetic reasoning about memory accesses in the presence of dynamic memory allocation. I will report on a case study which uses these techniques to perform the first rigorous analysis of widely deployed software countermeasures against cache attacks on modular exponentiation, based on executable code. The countermeasures are from different versions of libgcrypt and OpenSSL from the last 4 years, and our analysis measures their vulnerability to a hierarchy of attacks.


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


Miguel Á. Carreira-Perpiñán

Wednesday, January 11, 2017

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

Miguel Á. Carreira-Perpiñán, Professor, University of California at Merced, USA

Learning binary hash functions for information retrieval applications

Abstract:

Searching for the most similar images to a query image in a large database is a high-dimensional nearest-neighbour problem that must be approximated in practice in order to make the search fast. A standard approach, binary hashing, consists of mapping each image to a short bit string and searching in this binary space instead. A good mapping should be such that Hamming distances in the binary space approximate well the original image similarities. This mapping, the binary hash function, is learned from a training set of image similarities. We discuss two ways to learn the binary hash function. The first, more traditional one, defines a suitable objective function and optimises it over the hash function. This is a nonconvex nonsmooth problem, typically NP-complete. We show how this can be conveniently optimised using the method of auxiliary coordinates. The resulting algorithm finds better solutions than relaxation or other approximate algorithms, introduces parallelism and allows the user to learn a different type of hash function easily (say, a linear function vs a deep neural net). The second way replaces much of the optimisation mechanism with a diversity mechanism, using techniques from ensemble learning. We learn each output bit of the hash function independently from the others, each on a different training set. Surprisingly, this is not only much simpler, faster and scalable, but it also works better in terms of information retrieval measures such as precision/recall. This is joint work with my student Ramin Raziperchikolaei.


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


Invited Talks - 2016