IMDEA Software

IMDEA initiative

Home > Events > Software Seminar Series (S3)

Software Seminar Series (S3)

Joakim Öhman

Tuesday, December 7, 2021

11:00am Lecture hall 1 & Zoom3 https://zoom.us/j/3911012202 (pass: 5551337)

Joakim Öhman, PhD Student, IMDEA Software Institute

Visibility Reasoning for Concurrent Snapshot Algorithms

Abstract:

Visibility relations have been proposed by Henzinger et al. as an abstraction for proving linearizability of concurrent algorithms that obtains modular and reusable proofs. This is in contrast to the customary approach based on exhibiting the algorithm's linearization points.

In this talk I will show how to apply visibility relations to develop modular proofs for three elegant concurrent snapshot algorithms of Jayanti. The proofs are divided by signatures into components of increasing level of abstraction; the components at higher abstraction levels are shared, i.e., they apply to all three algorithms simultaneously. Importantly, the interface properties mathematically capture Jayanti's original intuitions that have previously been given only informally.


Time and place:
11:00am Lecture hall 1 & Zoom3 https://zoom.us/j/3911012202 (pass: 5551337)
IMDEA Software Institute, Campus de Montegancedo
28223-Pozuelo de Alarcón, Madrid, Spain


Nicolas Mazzocchi

Tuesday, November 30, 2021

11:00am Lecture hall 1 & Zoom3 https://zoom.us/j/3911012202 (pass: 5551337)

Nicolas Mazzocchi, Post-doctoral Researcher, IMDEA Software Institute

FORQ-based Language Inclusion Formal Testing

Abstract:

We provide a simple and efficient in practice algorithm to decide the language inclusion between (nondeterministic) Büchi automata, a PSpace-complete problem. Our approach, like others before, leverage a notion of quasiorder to prune the search for a counterexample by discarding candidates which are subsumed by others for the quasiorder. Discarded candidates are guaranteed to not compromise the completeness of the algorithm. The novelty of our work lies in the quasiorder used to discard candidates. We introduce FORQs (family of right quasiorders) that we obtain by adapting the notion of family of right congruences put forward by Maler and Staiger in 1993. We define a FORQ-based inclusion algorithm which we prove correct and instantiate it for a specific FORQ called structural FORQ induced by the Büchi automata to the right of the inclusion sign. The resulting implementation, called Forklift, almost always outperforms the state-of-the-art on a variety of benchmarks including benchmarks from program verification and theorem proving for word combinatorics.


Time and place:
11:00am Lecture hall 1 & Zoom3 https://zoom.us/j/3911012202 (pass: 5551337)
IMDEA Software Institute, Campus de Montegancedo
28223-Pozuelo de Alarcón, Madrid, Spain


Hernan Ponce de Leon

Tuesday, November 23, 2021

11:00am Zoom3 - https://zoom.us/j/3911012202 (pass: s3)

Hernan Ponce de Leon, Post-doctoral Researcher, Bundeswehr University Munich, Germany

Cats vs. Spectre: An Axiomatic Approach to Modelling Speculative Execution Attacks

Abstract:

The Spectre family of speculative execution attacks have required a rethinking of formal methods for security. Approaches based on operational speculative semantics have made initial inroads towards finding vulnerable code and validating defenses. However, with each new attack grows the amount of microarchitectural detail that has to be integrated into the underlying semantics. We propose an alternative, light-weight and axiomatic approach to specifying speculative semantics that relies on insights from memory models for concurrency. We use the CAT modeling language for memory consistency to specify execution models that capture speculative control flow, store-to-load forwarding, predictive store forwarding, and memory ordering machine clears. We present a bounded model checking framework parametrized by our speculative CAT models and evaluate its implementation against the state of the art. Due to the axiomatic approach, our models can be rapidly extended to allow our framework to detect new types of attacks and validate defenses against them.


Time and place:
11:00am Zoom3 - https://zoom.us/j/3911012202 (pass: s3)
IMDEA Software Institute, Campus de Montegancedo
28223-Pozuelo de Alarcón, Madrid, Spain


Lukas Aumayr

Tuesday, November 16, 2021

11:00am Lecture hall 1 & Zoom3 https://zoom.us/j/3911012202 (pass: s3)

Lukas Aumayr, PhD Student, Vienna University of Technology, Austria

Beyond Payments in Payment Channel Networks

Abstract:

Bitcoin and many other cryptocurrencies suffer from scalability issues. Payment Channel Networks (PCNs) are the most prominent approach to overcome these issues. The main idea is to reduce the transactions on the blockchain by establishing payment channels between users and allowing any two users connected via a path of channels to perform payments. PCN are already deployed in practice, e.g., the Lightning Network currently has 80k channels, 30k users and 200M USD locked. However, the current state-of-the-art in PCNs (i) is limited to payments, (ii) has security issues (i.e., wormhole attacks), (iii) is costly (i.e., funds are locked for a time proportional to the payment path length), (iv) is inefficient (i.e., it takes two rounds to complete payments) and (v) has a dependency on specific scripting language functionality (e.g., hash time lock contracts).

In this talk, I will show some recent protocols that overcome some of these challenges. I first present Blitz, a new multi-hop payment scheme that aims to improve on security and efficiency. Second, I present Donner, a Virtual Channel scheme that allows to connect any 2 endpoints in a PCN for the purpose of direct payments. Finally, I would shortly overview some of the open challenges in this setting.


Time and place:
11:00am Lecture hall 1 & Zoom3 https://zoom.us/j/3911012202 (pass: s3)
IMDEA Software Institute, Campus de Montegancedo
28223-Pozuelo de Alarcón, Madrid, Spain


Niki Vazou

Tuesday, November 2, 2021

11:00am Lecture hall 1 & Zoom3 https://zoom.us/j/3911012202 (pass: s3)

Niki Vazou, Assistant Research Professor, IMDEA Software Institute

Refinement Types

Abstract:

Refinement types are a type-based, static verification technique designed to be practical. They enrich the types of an existing programming language with logical predicates to specify program properties and automatically validate these specifications using SMT solvers. Refinement types are a promising verification technology that in the last decade has spread to mainstream languages (e.g., Haskell, C, Ruby, Scala, and the ML-family) to verify sophisticated properties of real world applications, e.g., safety of cryptographic protocols, memory and resource usage, and web security. But, the weakness of refinement types is that they do not meet the soundness standards set by theorem provers.

In this talk, we will see a brief overview of refinement types, the consequences of their practical design, and the presenter's future goals on the establishment of soundness.


Time and place:
11:00am Lecture hall 1 & Zoom3 https://zoom.us/j/3911012202 (pass: s3)
IMDEA Software Institute, Campus de Montegancedo
28223-Pozuelo de Alarcón, Madrid, Spain


István András Seres

Tuesday, October 26, 2021

11:00am Zoom3 - https://zoom.us/j/3911012202 (pass: s3)

István András Seres, PhD Student, Eötvös Loránd University

The Cambrian Explosion of Private Message Detection Schemes

Abstract:

Private Message Detection (PMD) as a new cryptographic primitive has been identified lately. A PMD protocol aims to allow users to efficiently and privately detect and retrieve their recipient-anonymous messages from a public bulletin board or an untrusted server. Such protocols have promising applications in anonymous messaging (e.g., Signal, Niwl) and privacy-preserving payment systems (Zcash, Monero, stealth payments for Bitcoin, Ethereum, and other privacy-enhancing overlays). A private but inherently inefficient solution would be downloading all the ciphertexts from the bulletin board or the server. Afterwards, users try to decrypt each ciphertext, and eventually, they'll find all their pertinent messages. PMD protocols aim to improve the efficiency of this naive approach without sacrificing recipient anonymity. Very recently, three works have been published as pre-prints (Fuzzy Message Detection (FMD) by Beck et al. (CCS'21), Private Signaling by Madathil et al. (under submission), and Oblivious Message Retrieval by Liu and Tromer (under submission)) proposing efficient and private message detection schemes under various privacy and security assumptions.

In this talk, we will briefly introduce and describe the three proposed PMD schemes. We make a comparison of the schemes, highlighting interesting trade-offs between them. Subsequently, we will give a privacy and anonymity analysis of the Fuzzy Message Detection (FMD) scheme proposed by Beck et al. (CCS'21). We will show how FMD fails to provide information-theoretic privacy guarantees (recipient unlinkability and relationship anonymity) and how it achieves weak notions of differential privacy. We describe a game-theoretical analysis of the incentives underlying the FMD scheme. We report our simulation of the FMD scheme on real-world communication networks. Finally, we conclude with open questions and future directions in the PMD field.


Time and place:
11:00am Zoom3 - https://zoom.us/j/3911012202 (pass: s3)
IMDEA Software Institute, Campus de Montegancedo
28223-Pozuelo de Alarcón, Madrid, Spain


Thaleia Dimitra Doudali

Tuesday, October 19, 2021

11:00am Zoom3 - https://zoom.us/j/3911012202 (pass: s3)

Thaleia Dimitra Doudali, Assistant Research Professor, IMDEA Software Institute

Building smart and fast systems using Machine Learning and Computer Vision

Abstract:

Nowadays, computing platforms use a mix of different hardware technologies, as a way to scale application performance, resource capacities and achieve cost effectiveness. However, this heterogeneity, along with the greater irregularity in the behavior of emerging workloads, render existing resource management approaches ineffective. In the first part of this talk, I will describe how we can use machine learning methods at the operating system-level, in order to make smarter resource management decisions and speed up application performance. In the second part of the talk, I will present how we can accelerate certain components of such systems using visualization and computer vision methods. Finally, I will conclude with my vision of coupling machine learning and computer vision at the system-level and present open questions that make this research area exciting to work on!


Time and place:
11:00am Zoom3 - https://zoom.us/j/3911012202 (pass: s3)
IMDEA Software Institute, Campus de Montegancedo
28223-Pozuelo de Alarcón, Madrid, Spain


Software Seminar Series (S3) - Spring 2021