IMDEA Software

Iniciativa IMDEA

Inicio > Eventos > Charlas Invitadas

Charlas Invitadas

Aastha Mehta

Monday, April 13, 2020

11:00am Online via Zoom: Zoom5 - https://zoom.us/j/5911012202

Aastha Mehta, PhD Student, Max Planck Institute for Software Systems, Alemania

Policy Compliance in Online Services

Abstract:

In response to incidents of unintended disclosure and misuse of user data by online services, modern data protection regulations require service providers to restrict their collection, processing, sharing and storage of sensitive user data. However, ensuring compliance with such regulation in today's complex and rapidly evolving systems is technically challenging. In my research, I have developed practical systems to prevent unintended disclosures and misuse of data in the face of two broad classes of threats: software bugs and misconfiguration, and side channels. In this talk, I will describe Pacer, a compliance system designed to prevent indirect inference of sensitive data via side channels in shared network links in the Cloud. Pacer shapes the outbound traffic of a Cloud tenant to make it independent of the tenant's secrets. At the same time, Pacer does allow variations in the traffic shape based only on public (non-secret) aspects of the tenants' workloads, thus enabling efficient sharing of network resources and incurring moderate overhead. Implementing Pacer requires modest changes to the Cloud hypervisor and the guest OS, and minimal changes to the guest application.


Time and place:
11:00am Online via Zoom: Zoom5 - https://zoom.us/j/5911012202
IMDEA Software Institute, Campus de Montegancedo
28223-Pozuelo de Alarcón, Madrid, Spain


Leonidas Lampropoulos

Friday, April 03, 2020

3:00pm Online via Zoom: Zoom5 - https://zoom.us/j/5911012202

Leonidas Lampropoulos, Post-doctoral Researcher, U. of Maryland and U. of Pennsylvania, USA

Software Correctness at Scale through Testing and Verification

Abstract:

Software correctness is becoming an increasingly important concern as our society grows more and more reliant on computer systems. Even the simplest of software errors can have devastating financial or security consequences. How can we find errors in real-world applications? How can we guarantee that such errors don't exist? To even begin to answer these questions we need a specification: a description of what it means for a piece of code to be correct, stated either explicitly (e.g. my private data are never leaked to third parties) or implicitly (e.g. this code will not terminate with an uncaught exception). In this talk, I will discuss efficient ways to debug and reason about software and specifications, focusing on two techniques and their interplay: property-based testing and mechanized formal verification. Testing can quickly uncover errors in complex software, but it cannot guarantee their absence. Formal verification provides strong correctness guarantees, but is still very expensive in time and effort. Together, they are a match made in heaven.


Time and place:
3:00pm Online via Zoom: Zoom5 - https://zoom.us/j/5911012202
IMDEA Software Institute, Campus de Montegancedo
28223-Pozuelo de Alarcón, Madrid, Spain


Arpan Gujarati

Tuesday, March 31, 2020

11:00am Online via Zoom: Zoom5 - https://zoom.us/j/5911012202

Arpan Gujarati, Post-doctoral Researcher, Max Planck Institute for Software Systems, Alemania

Towards Ultra-Reliable Cyber-Physical Systems: Reliability Analysis of Distributed Real-Time Systems

Abstract:

Fully-autonomous cyber-physical systems (CPS) such as autonomous vehicles, drones, and robots today are not engineered as rigorously as aircraft, and thus are not as reliable. In fact, these CPS will likely experience more failures in the future, since they will have a cumulative operation time several orders of magnitude more than that of airplanes. Thus, it is essential that we bring the reliability of today’s commercial aircraft systems (“ultra-reliability”) to the next generation of fully-autonomous CPS. One of the main challenges that needs to be addressed in this regard is ensuring high reliability with minimal cost in the presence of environmental disturbance sources such as electro-magnetic interference and thermal effects. To this end, I will present the first provably safe reliability analysis of Ethernet-based distributed real-time systems in the presence of environmentally-induced Byzantine errors. The analysis helps quantify and systematically evaluate the reliability tradeoffs involved when using different replication schemes. In this talk, I will discuss the key features of our analysis, including how we tackle reliability anomalies and how we quantify a CPS application's inherent robustness to occasional failures, and my plans for future research.


Time and place:
11:00am Online via Zoom: Zoom5 - https://zoom.us/j/5911012202
IMDEA Software Institute, Campus de Montegancedo
28223-Pozuelo de Alarcón, Madrid, Spain


Cristian-Alexandru Staicu

Wednesday, March 25, 2020

11:00am Online via Zoom: Zoom5 - https://zoom.us/j/5911012202

Cristian-Alexandru Staicu, Post-doctoral Researcher,

Code Reuse Gone Rogue: The Dangers of Overrelying on Third-Party JavaScript Code

Abstract:

Traditionally, the server-side code of websites was written in languages such as PHP or Java for which security issues are well-studied and well-understood. Recently, though, full-stack JavaScript web applications emerged, which have both their client-side and server-side code written in this language. The benefits of such an approach are obvious, e.g., easy knowledge transfer across tiers and uniform usage of tools. However, JavaScript was designed as a scripting language with a thin API and it was expected to run in a tightly-controlled environment, e.g., a sandbox. Taking JavaScript outside of the browser and using it as a general purpose programming language represents a paradigm shift for the web community and, thus, the npm ecosystem emerged to support this change. Npm is supposedly the largest software repository in the world with more than a million reusable packages. Nevertheless, the lack of code isolation and code vetting, the various ways to abuse the JavaScript language, and the plethora of reported vulnerabilities and malware incidents make npm a dangerous ecosystem with unique challenges for the security community. In this talk, we start by analyzing the attack surface of npm, showing that transitive dependencies and the large number of human agents in the ecosystem represent an important risk. We then continue with showing that vulnerabilities in npm packages affect real-world websites and that a motivated attacker can craft exploits against production websites by analyzing third-party, open-source code. Finally, we present a technique for boosting the recall of existing security analyses on JavaScript code that heavily relies on third-party libraries. More precisely, our approach extracts taint specifications for npm packages by using dynamic analysis and by leveraging test suites available in clients of the target package.


Time and place:
11:00am Online via Zoom: Zoom5 - https://zoom.us/j/5911012202
IMDEA Software Institute, Campus de Montegancedo
28223-Pozuelo de Alarcón, Madrid, Spain


Pedro Moreno Sánchez

Monday, March 16, 2020

11:00am Online via Zoom: Zoom9 - https://zoom.us/j/9911012202

Pedro Moreno Sánchez, Post-doctoral Researcher, Vienna University of Technology, Austria

Security, Privacy and Scalability in Blockchain Technologies

Abstract:

Blockchain technologies have rapidly acquired popularity and promise to become one of the pillars of the digital society. They, however, are not immune from open challenges in terms of security, privacy and scalability. First, the complexity of blockchain applications makes their security analysis prohibitive, which may lead to coin losses by honest users. Second, the fundamental requirement of including every single transaction in the blockchain for transparency is at odds with the privacy of transactions and users. Last, but not least, storing all data in the blockchain creates severe scalability issues: currently, blockchain technologies typically support a dozen transactions per second, which is far from the throughput of other payment systems available today. In this talk, I will present my research on security, privacy and scalability in blockchain technologies. In particular, I will focus our findings on the security and privacy issues with currently deployed scalability solutions such as the Lightning Network that affected to all its users in practice. Moreover, I will overview the cryptographic protocols that we have designed to mitigate the aforementioned issues. They have been implemented and tested for the Lightning Network and other currently deployed solutions. I will finish this talk with an overview of some of the open problems with current blockchain technologies.


Time and place:
11:00am Online via Zoom: Zoom9 - https://zoom.us/j/9911012202
IMDEA Software Institute, Campus de Montegancedo
28223-Pozuelo de Alarcón, Madrid, Spain


Alberto Ros

Thursday, March 05, 2020

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

Alberto Ros, Associate Research Professor, Universidad de Murcia

Non-Speculative and Invisible Reordering of Memory Operations

Abstract:

High-performance multicores providing strong consistency guarantees speculatively reorder memory operations. If a memory reordering is seen by other cores, speculative operations are squashed and re-executed. This talk presents the concept of non-speculative and invisible reordering of memory operations, the foundation on which the ECHO project (an ERC Consolidator Grant) is based on. The talk offers a background about memory-level speculation in current multicores. Then, it shows that, for the case of the load-load reordering, is not necessary to squash and re-execute reordered loads to guarantee the load-load order. It also presents a case for store-store ordering, which allows for the first time cost-effective store coalescing with strong consistency. Finally, it discusses solutions for secure speculative execution.


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, February 25, 2020

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

Borzoo Bonakdarpour, Assistant Research Professor, Iowa State University

Synthesis of Parametrized Distributed Self-stabilizing Protocols

Abstract:

Program synthesis is often called the "holy grail" of computer science, as it enables users to refrain from error-prone software development process and focus on only analyzing the intended behavior of the system. Thus, program synthesis exhibits its power in automatic generation of intricate and complex parts of a system as well as in repetitive programming tasks, and bringing the power of programming to the average computer user who may not possess sophisticated programming skills. A particular area where program synthesis can play a central role is in distributed systems due to their inherent complex nature. This talk will present our recent results and breakthroughs in synthesizing parameterized distributed self-stabilizing algorithms.


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


Carsten Baum

Monday, February 24, 2020

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

Carsten Baum, Post-doctoral Researcher, Aarhus University, Denmark

Efficient Constant-Round MPC with Identifiable Abort and Public Verifiability

Abstract:

Recent years have seen a tremendous growth in the interest in secure multiparty computation (MPC) and its applications. While much progress has been made concerning its efficiency, many current, efficient protocols are vulnerable to Denial of Service attacks, where a cheating party may prevent the honest parties from learning the output of the computation, whilst remaining anonymous. The security model of identifiable abort aims to prevent these attacks, by allowing honest parties to agree upon the identity of a cheating party, who can then be excluded in the future. Several existing MPC protocols offer security with identifiable abort against a dishonest majority of corrupted parties. However, all of these protocols have a round complexity that scales linearly with the depth of the circuit, so are unsuitable for use in high latency networks. In this work, we present the first efficient MPC protocols with identifiable abort in the dishonest majority setting, which run in a constant number of rounds and make only black-box use of cryptographic primitives. Our main construction is built from highly efficient primitives in a careful way to achieve identifiability at a low cost. In particular, we avoid the use of public-key operations outside of a setup phase, incurring a relatively low overhead on top of the fastest currently known constant-round MPC protocols based on garbled circuits. In addition, we show how to upgrade our protocol to achieve public verifiability using a public bulletin board, allowing any external party to verify correctness of the computation and identify a cheating party.


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


Jaron Skvosted Gundersen

Thursday, February 20, 2020

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

Jaron Skvosted Gundersen, PhD Student, Aalborg University, Denmark

Improved Bounds on the Threshold Gap in Ramp Secret Sharing

Abstract:

In secret sharing a dealer holds a secret and wants to distribute it among several parties in such a way that the individuals do not learn the secret. However, if several of the parties unite their shares they are able to reconstruct the secret. Secret sharing has several applications such as distributed storage and secure multiparty computation. For different applications it is desired to have different properties for the secret sharing scheme used. Such properties can be linearity, low share size compared to the secret size, low reconstruction, and high privacy. In this talk, I will present some bounds connecting some of these properties. These bounds give some restrictions on what we can achieve for secret sharing schemes. The talk is based on results from the paper "Improved Bounds on the Threshold Gap in Ramp Secret Sharing" by Ignacio Cascudo, Jaron Skovsted Gundersen and Diego Ruano, published in IEEE Transactions on Information Theory.


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


Roberto Di Cosmo

Thursday, February 13, 2020

3:15pm Lecture hall 1, level B

Roberto Di Cosmo, Research Professor, INRIA Paris, France

Archiving, assessing and attributing research software: towards software as a first class citizen in the scholarly world

Abstract:

Software is a fundamental pillar of modern scientific research, across all fields and disciplines. However, there is a general lack of adequate means to archive, reference and cite software. In this talk, we will survey the main issues that make this task difficult, ranging from the specificity of the persistent identifiers needed for reproducibility to the complexity of determining software authorship and authority, especially for long running projects, which are needed for proper software attribution and credit. We report on recent contributions to the ongoing efforts to develop proper processes, guidelines and recommendations for software reference and software citation, building upon the internal experience of Inria and the emerging Software Heritage infrastructure.


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


Ida Tucker

Wednesday, January 15, 2020

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

Ida Tucker, PhD Student,

Distributing the elliptic curve digital signature algorithm both securely and efficiently

Abstract:

The Elliptic Curve Digital Signature Algorithm (ECDSA) is a widely adopted digital signature standard; in particular it is employed to validate bitcoin transactions. In this context, the theft of a secret signing key results in an immediate financial loss, thereby creating a single point of failure. An interesting solution to reduce the risk of key theft is that of sharing the secret signing key among various devices, such that a signature can only be produced if these devices collaborate to jointly produce a signature, thereby distributing the signature protocol. In this talk I will focus on the two party case, which allows for instance to share a secret key between a mobile phone and a laptop. Unfortunately, efficient distributed variants of ECDSA are notoriously hard to achieve and prior to our work, solutions required expensive zero knowledge proofs to deal with malicious adversaries (MacKenzie et al. (Crypto’01)), relied on non standard interactive assumptions (Lindell (Crypto’17)) or induced a high communication cost (Doerner et al. (IEEE S&P’18)). I will explain how, in a recent article from Crypto’19 we overcome all of the above drawbacks, and — using class groups of imaginary quadratic fields — provide a provably secure two party ECDSA protocol, relying only on standard assumptions, which is the most efficient to date in terms of bandwidth consumption while remaining competitive in terms of timings. I will further justify that — by resorting to two recently introduced computational assumptions on class groups — we can dramatically improve the efficiency of the zero knowledge proofs needed by our protocol (and thereby that of the overall protocol).


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


Samira Briongos

Tuesday, January 14, 2020

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

Samira Briongos, Post-doctoral Researcher, UPM

RELOAD+REFRESH: Abusing Cache Replacement Policies to Perform Stealthy Cache Attacks

Abstract:

Caches have become the prime method for unintended information extraction across logical isolation boundaries. They are widely available on all major CPU platforms and, as a side-channel, caches provide great resolution, making them the most convenient channel for Spectre and Meltdown. As a consequence, several methods to stop cache attacks by detecting them have been proposed. Detection is strongly aided by the fact that observing cache activity of co-resident processes is not possible without altering the cache state and thereby forcing evictions on the observed processes. In this work, we show that this widely held assumption is incorrect. Through clever usage of the cache replacement policy, it is possible to track cache accesses of a victim's process without forcing evictions on the victim' s data. Hence, online detection mechanisms that rely on these evictions can be circumvented as they would not detect the introduced RELOAD+REFRESH attack. The attack requires a profound understanding of the cache replacement policy. We present a methodology to recover the replacement policy and apply it to the last five generations of Intel processors. We further show empirically that the performance of RELOAD+REFRESH on cryptographic implementations is comparable to that of other widely used cache attacks, while detection methods that rely on L3 cache events are successfully thwarted.


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


Charlas Invitadas - 2019