IMDEA initiative

Home > Events > Invited Talks

Invited Talks

Giulia De Santis

Tuesday, November 21, 2017

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

Giulia De Santis, PhD Student, INRIA Nancy-Grand Est., France

Classifying Internet-wide scanners using Gaussian Mixture and Hidden Markov Models

Abstract:

Internet-wide scanning techniques and services, like Zmap, Shodan, NMap, Masscan, etc. are heavily used for malicious activities. To enable early identification of advanced threats, this work models scanners from the scanned software system point of view. More in detail, three of the network scanning activities features are modeled: intensity, spatial and temporal movements. Intensity is related to the number of packets received by the scanned system within a given (fixed) window of time. The latter two features are respectively related to the difference of successive scanned IP addresses and timestamps. Based on real logs of incoming IP packets collected from a darknet, hidden Markov models (HMMs) are used to assess what scanning technique is operating. Furthermore, only spatial or temporal movements of the scanning technique can be used to fingerprint, with an accuracy up to 98%, what network scanner originated the perceived darknet traffic.


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


Borzoo Bonakdarpour

Tuesday, October 31, 2017

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

Borzoo Bonakdarpour, Assistant Research Professor, McMaster University, Canada

Automated Fine-Tuning of Probabilistic Self-Stabilizing Algorithms

Abstract:

Although randomized algorithms have widely been used in distributed computing as a means to tackle impossibility results, it is currently unclear what type of randomization leads to the best performance in such algorithms. In this talk, I propose automated techniques to find the probability distribution that achieves minimum average recovery time for an input randomized distributed self-stabilizing protocol without changing the behavior of the algorithm. Our first technique is based on solving symbolic linear algebraic equations in order to identify fastest state reachability in parametric discrete-time Markov chains. The second approach applies parameter synthesis techniques from probabilistic model checking to compute the rational function describing the average recovery time and then uses dedicated solvers to find the optimal parameter valuation. The third approach computes over- and under-approximations of the result for a given parameter region and iteratively refines the regions with minimal recovery time up to the desired precision. The latter approach finds sub-optimal solutions with negligible errors, but it is significantly more scalable in orders of magnitude as compared to the other approaches.


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


Vasilios Mavroudis

Thursday, September 28, 2017

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

Vasilios Mavroudis, PhD Student, University College London, United Kingdom

Cryptographic Hardware from Untrusted Components

Abstract:

The current consensus within the security industry is that high-assurance systems cannot tolerate the presence of compromised hardware components. In this talk, we challenge this perception and demonstrate how trusted, high-assurance hardware can be built from untrusted and potentially malicious components. The majority of IC vendors outsource the fabrication of their designs to facilities overseas, and rely on post-fabrication tests to weed out deficient chips. However, such tests are not effective against: 1) subtle unintentional errors (e.g., malfunctioning RNGs) and 2) malicious circuitry (e.g., stealthy Hardware Trojans). Such errors are very hard to detect and require constant upgrades of expensive forensics equipment, which contradicts the motives of fabrication outsourcing. In this session, we introduce a high-level architecture that can tolerate multiple, malicious hardware components, and outline a new approach in hardware compromises risk management. We first demo our backdoor-tolerant Hardware Security Module built from low-cost commercial off-the-shelf components, benchmark its performance, and delve into its internals. We then explain the importance of "component diversification" and "non-overlapping supply chains", and finally discuss how "mutual distrust" can be exploited to further reduce the capabilities of the adversaries. This talk is based on our CCS 2017 paper and the project website is: https://trojantolerance.org


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


Danil Annenkov

Tuesday, September 26, 2017

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

Danil Annenkov, PhD Student, DIKU University of Copenhagen, Denmark

Reasoning Techniques for the Module System Formalisation in Coq.

Abstract:

In this talk we present a number of techniques that allow for formal reasoning with nested and mutually inductive structures built up from finite maps and sets (also called semantic objects), and at the same time allow for working with binding structures over sets of variables. The techniques, which build on the theory of nominal sets combined with the ability to work with multiple isomorphic representations of finite maps, make it possible to give a formal treatment, in Coq, of a higher-order module system, including the ability to eliminate entirely, at compile time, abstraction barriers introduced by the module system. The development is based on earlier work on static interpretation of modules and provides the foundation for a higher-order module language for Futhark, an optimising compiler targeting data-parallel architectures, such as GPGPUs.


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


Veelasha Moonsamy

Friday, September 15, 2017

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

Veelasha Moonsamy, Post-doctoral Researcher, Radboud University, The Netherlands

Side-channel attacks on mobile devices and future research directions

Abstract:

Side-channel attacks on mobile devices have gained increasing attention since their introduction in 2007. While traditional side-channel attacks, such as power analysis attacks and electromagnetic analysis attacks, required physical presence of the attacker as well as expensive equipment, an (unprivileged) application is all it takes to exploit the leaking information on modern mobile devices. Given the vast amount of sensitive information that are stored on smartphones, the ramifications of side-channel attacks affect both the security and privacy of users and their devices. In this talk, I will present our latest work on how an adversary can exploit side-channel information, in this case power from the phone battery, to maliciously control a public charging station in order to exfiltrate data from a smartphone via a USB charging cable (i.e. without using the data transfer functionality). In the second part of my talk, I will briefly present an overview of existing side-channel attacks on mobile devices and argue for the need of a new categorization system as side-channel attacks have evolved significantly since their introduction during the smartcard era. I will explain how our proposed categorization system will help to facilitate the development of novel countermeasures and provide insights into possible future research directions.


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


Gregory Chockler

Tuesday, September 12, 2017

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

Gregory Chockler, Professor, Royal Holloway, University of London (RHUL),

The Space Complexity of Reliable Storage Services

Abstract:

Although reliable distributed and cloud storage systems have attracted significant attention over the past decade, until recently, relatively little has been known about fundamental space tradeoffs involved in their implementations. In this talk, I will review the results of our recent study where we explored these tradeoffs in the context of two most commonly used implementation techniques: replication and error-correction coding. Our results reveal that concurrent writing along with failures and asynchrony pose formidable obstacles for realizing space-efficient storage systems using either technique, even for the simplest read/write storage services. The talk will be self-contained and accessible for general CS audience though some familiarity with distributed systems will be an advantage. Based on the joint work with Yuval Cassuto, Idit Keidar, and Sasha Spiegelman, Technion, published in PODC'16 and PODC'17.


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


Filippo Bonchi

Monday, September 11, 2017

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

Filippo Bonchi, Research Scientist, École normale supérieure (ENS), Lyon, France

Full Abstraction for Signal Flow Graphs

Abstract:

Signal Flow Graphs (SFGs) were introduced in the 1940s by Shannon as a formal circuit model of a class of simple analog computing machines. They are a common abstraction in control theory, signal processing and engineering, used for modelling physical systems and their controllers. Nowadays, cyber-physical systems are modelled, simulated and analysed in graphical environments such as Simulink and Modelica that can be seen as great-grandchildren of SFGs. In this talk, we introduce a graphical syntax for signal flow graphs based on the language of string diagrams. Using universal constructions, we provide a denotational semantics and a sound and complete axiomatisation. The terms can be executed using a structural operational semantics. The problem of full abstraction raises novel and unexpected semantics issues.


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


Monir Azraoui

Wednesday, September 06, 2017

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

Monir Azraoui, Post-doctoral Researcher, EURECOM, France

Secure Operations in the Cloud

Abstract:

Cloud computing is perceived as the "holy grail" to cope with the handling of tremendous amounts of data collected every day from sensors, social networks, mobile devices, etc. However, many organizations are reluctant to resort to cloud technologies. Indeed, the inherent transfer of control over storage and computation to untrusted cloud servers raises various security challenges. In this regard, verifying cloud operations can help users have more control over their resources and can reduce the impact of mistrust in the cloud. Besides, allowing some operations over the data, such as search functionalities, while ensuring the privacy of the data and the queries, can reduce the doubts of using cloud technologies. This talk presents new cryptographic protocols that enable cloud users to verify (i) the correct storage of outsourced data and (ii) the correct execution of outsourced computation. I will first describe a cryptographic protocol that generates proofs of retrievability, which enable data owners to verify that the cloud correctly stores their data. I will then present cryptographic schemes for verifiable computation by focusing on three operations frequent in data processing routines, namely polynomial evaluation, matrix multiplication and conjunctive keyword search. I will finally focus on the problem of searchable encryption that allows users to search over encrypted data outsourced at a cloud server.


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


William Suski

Thursday, July 27, 2017

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

William Suski, Science Director, Office of Naval Research Global, USA

ONR Global Basic Research Funding Opportunities

Abstract:

Dr. William Suski from the US Navy's Office of Naval Research Global (ONRG) will be presenting a description of his organization along with the various basic research funding and collaboration opportunities offered by ONRG.


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


Ana Sokolova

Monday, July 17, 2017

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

Ana Sokolova, Associate Professor, University of Salzburg, Austria

Concurrent Data Structures: Semantics and Relaxations

Abstract:

The semantics of concurrent data structures is usually given by a sequential specification and a consistency condition. It has been noticed that strong semantics might result in poor performance and scalability which initiated the work on relaxed semantics of concurrent objects, in particular concurrent data structures.

Relaxing the semantics can be done in both dimensions: (1) by relaxing the sequential specification and/or (2) by relaxing the consistency condition. I will present quantitative relaxations that result in (1) as well as local linearizability that provides (2). This is joint work with many coauthors published at POPL'13 and CONCUR'16.


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


Christian Hammer

Monday, June 26, 2017

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

Christian Hammer, Full Professor, University of Potsdam, Germany

WebPol: Fine-grained Information Flow Policies for Web Browsers

Abstract:

In the standard browser programming model, third-party scripts included in an application execute with the same privilege as the hosting page's own code. This leaves the application's confidential data vulnerable to theft and leakage by malicious code and inadvertent bugs in the third-party scripts. Security mechanisms in modern browsers (the same-origin policy, cross-origin resource sharing and content security policies) are too coarse to suit this programming model. All these mechanisms (and their extensions) describe whether or not a script can access certain data, whereas the meaningful requirement is to allow untrusted scripts access to confidential data that they need and to prevent the scripts from leaking the data on the side. Motivated by this gap, we propose WebPol, a policy mechanism that allows a website developer to include fine-grained policies on confidential application data in the familiar syntax of the JavaScript programming language. The policies can be associated with any webpage element, and specify what aspects of the element can be accessed by which third-party domains. A script can access data that the policy allows it to, but it cannot pass the data (or data derived from it) to other scripts or remote hosts in contravention of the policy. To specify the policies, we expose a small set of new native APIs in JavaScript. Our policies can be enforced using any of the numerous existing proposals for information flow tracking in web browsers. We have integrated our policies into one such proposal that we use to evaluate performance overheads and test our examples.


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


Grigory Fedyukovich

Friday, June 23, 2017

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

Grigory Fedyukovich, Post-doctoral Researcher, University of Washington, USA

Synchronizing Constraint Horn Clauses

Abstract:

The goal of unbounded program verification is to discover an inductive invariant that over-approximates all reachable program states and is strong enough to exclude all bad states. Invariant synthesis is often addressed by 1) encoding the program to a system of Constrained Horn clauses (CHC) and 2) employing an SMT-based procedure to check satisfiability of CHCs. However, a solution of such a system is often inexpressible in the constraint language, especially if the program suffers of multiple recursive calls operating on the shared data. This talk presents a technique to synchronize recurrent computations, thus increasing the chances for an invariant to be found.

Our novel notion of the CHC product gives rise to a lightweight iterative algorithm of merging recurrent computations into groups and its applications to automated program synthesis. In particular, we applied the CHC-product transformation to certify solutions delivered by our automatic parallelization tool, called GraSSP. Given an arbitrary segmentation of the input array, GraSSP synthesizes a code to determine a new segmentation of that array which allows computing and merging individual computation results for all segments. The talk focuses on the verification aspect of GraSSP, in which the given serial and synthesized parallel programs are encoded to CHCs, transformed with the CHC-product, and efficiently verified for equivalence using a state-of-the-art CHC solver.


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


Julian Dolby

Friday, June 23, 2017

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

Julian Dolby, Research Staff Member, IBM T. J. Watson Research Center, USA

WALA Everywhere

Abstract:

The Watson Libraries for Analysis (WALA) started life as analysis for Java bytecode, but soon grew to include JavaScript and .NET bytecode as well. I shall briefly summarize this history and the design decisions that grew out of it, because those decisions enabled further expansion after WALA became open source: from Android to nodejs, WALA handles more systems, much of the work being done by the community and contributed to the open source project. I shall talk about 3 of those expansions. The first is analysis of hybrid mobile applications, in which Android bytecode and JavaScript source code are analyzed together to create a cross-language analysis result; I shall present the WALA architecture that enables such analysis and talk about how such analysis has been used so far. The second is WALA Client, in which much of WALA is run in a Web browser, including a version of our JavaScript analysis, potentially enabling live analysis of visited Web sites. I shall discuss how this is accomplished technically, and I shall show it running as part of the talk. Third, I shall discuss our ongoing work building analysis of Apple's Swift language. Throughout this talk, I shall try to bring out how WALA design decisions made in the beginning have enabled this expansion, and how an increasing community of researchers have made it possible.


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


Daniel Benarroch

Thursday, June 15, 2017

10:45am Lecture hall 1, level B

Daniel Benarroch, Lead Cryptographer, QED-it, Israel

Computing on Private Data with Zero-Knowledge Proofs and the Blockchain

Abstract:

Blockchain technology has become of great interest for major multinationals, creating a need to close the gap between the industry and academia. The applications of this peer-to-peer decentralized and immutable data base are countless, yet most of these applications lack a privacy component, which is why only "public blockchains" (mainly cryptocurrencies) actualize into usable applications. At QED-it we are developing a privacy platform on top of any blockchain that uses cryptographic Zero-Knowledge Proofs (ZKPs) in order to prove properties or attributes of private data. These properties are defined as functions computed on the data. Instead of sharing your data on the blockchain, allowing everybody to see it, you can now share the result of a computation and a Zero-Knowledge Proof attesting to the correctness of the computation. We will go over the "Pay to Sudoku" example to understand how to use ZKPs (on the blockchain) and we will overview the main components of zk-SNARKs, one of the better constructions of ZKPs.


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


Ilya Sergey

Tuesday, June 13, 2017

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

Ilya Sergey, Lecturer, University College London, United Kingdom

Programming and Proving with Distributed Protocols

Abstract:

Distributed systems play a crucial role in modern infrastructure, but are notoriously difficult to implement correctly. This difficulty arises from two main challenges: (a) correctly implementing core system components (e.g., two-phase commit), so all their internal invariants hold, and (b) correctly composing standalone system components into functioning trustworthy applications (e.g., persistent storage built on top of a two-phase commit instance). Recent work has developed several approaches for addressing (a) by means of mechanically verifying implementations of core distributed components, but no methodology exists to address (b) by composing such verified components into larger verified applications. As a result, expensive verification efforts for key system components are not easily reusable, which hinders further verification efforts.

In my talk, I will present Disel, the first framework for implementation and compositional verification of distributed systems and their clients, all within the mechanized, foundational context of the Coq proof assistant. In Disel, users implement distributed systems using a domain specific language shallowly embedded in Coq and providing both high-level programming constructs as well as low-level communication primitives. Components of composite systems are specified in Disel as protocols, which capture system-specific logic and disentangle system definitions from implementation details. By virtue of Disel's dependent type system, well-typed implementations always satisfy their protocols' invariants and never go wrong, allowing users to verify system implementations interactively using Disel's Hoare-style program logic, which extends state-of-the-art techniques for concurrency verification to the distributed setting.


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


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


Rebekah Overdorf

Wednesday, March 29, 2017

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

Rebekah Overdorf, PhD Student, Drexel University, USA

How Unique is Your .onion? An Analysis of the Fingerprintability of Tor Onion Services

Abstract:

Website fingerprinting attacks aim to uncover which webpage a user is visiting by monitoring the incoming and outgoing packets on a network. These attacks apply supervised classifiers to network traffic traces to identify patterns that are unique to a website. Even anonymous communication systems such as Tor are vulnerable to this type of attack. The adversary first records traffic from visits to a set of known websites of interest and extracts a website fingerprint for each one. The adversary has access to the communication between the client and the entry node to the Tor network, so he can record the unlabeled traffic and try to classify it based on the known fingerprints.

We aim to better inform defenses against these attacks. We perform multi-level feature analysis of website fingerprinting attacks using three state-of-the-art website fingerprinting methods on 482 Tor onion (hidden) services, the largest analysis of this kind completed on hidden services to date. Recent studies have shown that Tor hidden service websites are particularly vulnerable to website fingerprinting attacks due to their limited number and sensitive nature. We further show that certain sites are more vulnerable to such attacks than others. We use a number of methods to rank the features used by three state-of-the-art website fingerprinting methods from prior work to determine what makes a hidden service site more or less easily unveiled by a website fingerprinting attack. Further, we analyze web-level features to determine which correlate to sites that are more or less fingerprintable and present an analysis of misclassifications to inform guidelines for reducing the fingerprintability of a hidden service website. Our analysis provides insight into designing defenses against website fingerprinting 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


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