IMDEA Software

Iniciativa IMDEA

Inicio > Eventos > Charlas Invitadas

Charlas Invitadas

Nikos Vasilakis

Tuesday, November 29, 2022

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

Nikos Vasilakis, Assistant Professor,

PaSh: Light-Touch, Practically Correct, Just-in-Time Shell Script Parallelization

Abstract:

Unix / Linux shell scripting is ubiquitous, partly due to the simplicity in which it allows combining third-party components (commands) written in any programming language. Unfortunately, this language-agnostic composition hinders automated parallelization, often forcing developers to manually rewrite shell scripts and their third-party components in other languages that support these features. In this talk I will present PaSh, a system for parallelizing Unix/Linux shell scripts. PaSh combines a just-in-time transcompiler that blends static pre-processing with dynamic interposition, a high-level annotation framework for expressing partial command specifications, and a collection of runtime primitives that support the execution of parallel shell scripts. PaSh achieves order-of-magnitude speedups on unmodified shell scripts, all while requiring no modifications to the system's underlying shell interpreter and while remaining virtually indistinguishable from Bash across the entire POSIX test suite. PaSh is worked on by several institutions, has received multiple awards, and is open-source software available by the Linux Foundation.


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


Nico Lehmann

Tuesday, October 4, 2022

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

Nico Lehmann, PhD Student, UC San Diego

Flux: Liquid Types for Rust

Abstract:

Low-level pointer-manipulating programs are hard to verify, requiring complex spatial program logics that support reasoning about aliasing and separation. Worse, when working over collections, these logics burden the programmer with annotating loops with quantified invariants that describe the contents of the collection. In this talk, I will give a demo of Flux, a static verifier for Rust that shows how logical refinements can work hand in glove with Rust's ownership mechanisms to yield ergonomic type-based verification for low-level imperative code. By factoring complex invariants into type constructors and simple refinements, Flux can efficiently synthesize loop annotations via liquid inference. We use a suite of vector-manipulating programs to demonstrate the advantages of Flux's refinement types over program logics, as implemented in the state-of-the-art Prusti verifier.


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


Wednesday, September 7, 2022

11:00am Zoom4 - https://zoom.us/j/4911012202 (pass: 123)

Gregory Boddin & Danny Willems, Researcher, LeakIX

Exploring Internet services mis-configuration at scale

Abstract:

In this talk we will demonstrate that not only vulnerabilities in exposed services can be dangerous, but also the issue with leaving those services un-configured or with default credentials. We will also touch on the Devops side and talk about left over deployment artifacts that can disclose information and credentials about an infrastructure.

In this talk we will demonstrate that not only vulnerabilities in exposed services can be dangerous, but also the issue with leaving those services un-configured or with default credentials. We will also touch on the Devops side and talk about left over deployment artifacts that can disclose information and credentials about an infrastructure.


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


Patrick Cousot

Tuesday, May 31, 2022

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

Patrick Cousot, Professor, Instituto Courant de Ciencias Matemáticas, Universidad de Nueva York, EE.UU.

Asynchronous Correspondences Between Hybrid Trajectory Semantics

Abstract:

We study abstraction correspondences between hybrid trajectory semantics for verification and refinement, including discretization and state-based homomorphisms, simulations, bisimulations, preservations with progress, and show that they are all Galois connections. We investigate the problematic composition of hybrid state-based abstractions.


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


Tuesday, May 17, 2022

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

Gordon Pace, PhD Student, Universidad de Malta

Smart Contracts and Runtime Verification

Abstract:

Smart contracts running on blockchains have been hailed as trustless platforms for carrying out agreements between parties without the risk of interference by the parties themselves or others. The immutability of such agreements is assumed to be a desirable feature, that is until the first bugs appear. In this talk, I will present ongoing work in building runtime verification tools for smart contracts, with a particular focus on recovery from discovered errors. In particular, I will discuss the use of runtime verification for smart contracts to handle (i) immutable specifications for mutable smart contracts; and (ii) recovery through smart contract design as long-lived transaction engines.


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


Friday, May 6, 2022

12:00am Meeting room 202 (Hill View), level 2

Sunjay Cauligi, Post-doctoral Researcher, Instituto Max Planck

Practical Foundations for Software Spectre Defenses

Abstract:

Spectre vulnerabilities violate our fundamental assumptions about programming abstractions, allowing attackers to steal sensitive data despite previously state-of-the-art countermeasures. To defend against Spectre, developers of verification tools and compiler-based mitigations are forced to reason about low-level hardware details such as speculative execution. I will explain the tradeoffs inherent in formal frameworks for Spectre, the complexity of defense tools, and the resulting security guarantees. I will also propose practical choices for developers of analysis and mitigation tools and identify interesting open problems in this area for future work.


Time and place:
12:00am Meeting room 202 (Hill View), level 2
IMDEA Software Institute, Campus de Montegancedo
28223-Pozuelo de Alarcón, Madrid, Spain


Martin Leucker

Wednesdady, April 6, 2022

12:00pm Zoom5 - https://zoom.us/j/5911012202 (pass: 5551337)

Martin Leucker, Professor, U of Luebeck

Formal Verification of Neural Networks?

Abstract:

Machine learning is a popular tool for building state of the art software systems. It is more and more used also in safety critical areas. This demands for verification techniques ensuring the safety and security of machine learning based solutions. However, in this presentation, we argue that the popularity of machine learning comes from the fact that no formal specification exists which renders traditional verification in appropriate. Instead, validation is typically demanded and we present a recent technique that validates certain correctness properties for an underlying recurrent neural network.


Time and place:
12:00pm Zoom5 - https://zoom.us/j/5911012202 (pass: 5551337)
IMDEA Software Institute, Campus de Montegancedo
28223-Pozuelo de Alarcón, Madrid, Spain


Wednesday, April 6, 2022

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

Gerardo Schneider, Full Professor, Universidad de Gotemburgo, Suecia

Towards a Framework for Specifying and Realizing Correct–by–Construction Contextual Robotic Missions

Abstract:

In this talk I will present some initial ideas (a first proposal) on how to define a framework to define missions for autonomous systems which are composed of different “controllers” that need to be active in different contexts. The idea is to try to be as formal as possible, to provide some kind of (semi-)formal reasoning, while being practical.


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


Tuesday, April 5, 2022

4:00pm Zoom3 - https://zoom.us/j/3911012202 (pass: 5551337)

Hannews Kallwies, PhD Student, U of Luebeck

Aggregate Update Problem for Multi-clocked Dataflow Languages

Abstract:

Dataflow languages have, as well as functional languages, immutable semantics, which is often implemented by copying values. A common compiler optimization known from functional languages involves analyzing which data structures can be modified in-place instead of copying them. In the presentation an algorithm to this so called Aggregate Update Problem for multi-clocked dataflow languages, i.e. those that allow streams to have events at disjoint timestamps, like e.g. Lucid, Lustre and Signal, is presented. Therefor TeSSLa, a generic stream transformation language with a small set of operators, is used to develop the ideas. Finally the empirical results of the implementation of the optimization into the TeSSLa compiler are presented.


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


Antonio Faonio

Tuesday, April 5, 2022

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

Antonio Faonio, Assistant Professor, EURECOM, Francia

Continuously Non-Malleable Secret Sharing in the Plain Model

Abstract:

In this talk I will present a paper published at TCC'21 together with Gianluca Brian and Daniele Venturi from Sapienza University of Rome. We study non-malleable secret sharing against joint leakage and joint tampering attacks. Our main result is the first threshold secret sharing scheme in the plain model achieving resilience to noisy-leakage and continuous tampering. The above holds under (necessary) minimal computational assumptions (i.e., the existence of one-to-one one-way functions), and in a model where the adversary commits to a fixed partition of all the shares into non-overlapping subsets of at most t−1 shares (where t is the reconstruction threshold), and subsequently jointly leaks from and tampers with the shares within each partition. We study the capacity (i.e., the maximum achievable asymptotic information rate) of continuously non-malleable secret sharing against joint continuous tampering attacks. In particular, we prove that whenever the attacker can tamper jointly with k>t/2 shares, the capacity is at most t−k. The rate of our construction matches this upper bound. An important corollary of our results is the first non-malleable secret sharing scheme against independent tampering attacks breaking the rate-one barrier (under the same computational assumptions as above).


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


Hanna Lachnitt & Nicholas Mosier

Tuesday, March 29, 2022

6:00pm Zoom3 - https://zoom.us/j/3911012202 (pass: 5551337)

Hanna Lachnitt & Nicholas Mosier, , Universidad Stanford, EE.UU.

Axiomatic Hardware-Software Contracts for Security

Abstract:

Microarchitectural attacks are side/covert channel attacks which enable leakage/communication as a direct result of hardware optimizations. Secure computation on modern hardware thus requires hardware-software contracts which include in their definition of software-visible state any microarchitectural state that can be exposed via microarchitectural attacks. Defining such contracts has become an active area of research. In this talk, we will present leakage containment models (LCMs)—novel axiomatic hardware-software contracts which support formally reasoning about the security guarantees of programs when they run on particular microarchitectures. Our first contribution is an axiomatic vocabulary for formally defining LCMs, derived from the established axiomatic vocabulary used to formalize processor memory consistency models. Using this vocabulary, we formalize microarchitectural leakage—focusing on leakage through hardware memory systems—so that it can be automatically detected in programs. To illustrate the efficacy of LCMs, we first demonstrate that our leakage definition faithfully captures a sampling of (transient and non-transient) microarchitectural attacks from the literature. Next, we develop a static analysis tool, called Clou, which automatically identifies microarchitectural vulnerabilities in programs given a specific LCM. We use Clou to search for Spectre gadgets in benchmark programs as well as real-world crypto-libraries (OpenSSL and Libsodium), finding new instances of leakage. To promote research on LCMs, we design the Subrosa toolkit for formally defining and automatically evaluating/comparing LCM specifications.


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


Collins Daniel Patrick

Tuesday, March 29, 2022

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

Collins Daniel Patrick, PhD Student, EPFL, Suiza

Secure messaging: past, present and future

Abstract:

Secure messaging applications are used by billions of users every day. Applications like WhatsApp make use of the seminal Signal protocol that provides conversation participants with end-to-end encryption guarantees. Due to the long-lived nature of messaging sessions, the threat of state exposure is more pronounced, and thus protocols like Signal regularly refresh keying material. In the cryptographic literature, many works address possible performance/security trade-offs beyond Signal and address additional problems like providing security against bad randomness generators and detecting active attacks. In this presentation, we examine this exciting line of work, discuss ongoing work and propose directions for further research. In particular we consider both the two-party setting and the more challenging group setting where parties may join and leave a group over time.


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


Alessio Mansutti

Thursday, March 24, 2022

10:00am Zoom3 - https://zoom.us/j/3911012202 (pass: @alessio)

Alessio Mansutti, Research Associate, Universidad de Oxford, Reino Unido

From arithmetic theories and separation logic to statically detecting arithmetic errors in programs

Abstract:

In this talk I will touch on two results I achieved during my PhD and Postdoc in the area of logics for algorithmic verification.

1. Integer linear arithmetic, also known as Presburger arithmetic, has been a central subject in computer science for many decades. A celebrated result by Ginsburg and Spanier show that the family of sets definable in Presburger arithmetic coincides with the family of semilinear sets. Despite more than fifty years of work on semilinear sets and several attempts, one question has remained unanswered: how do we efficiently compute the complement of a semilinear set? In a recent work with Chistikov and Haase, I answer this question by giving an optimal algorithm to compute such complements. As a corollary, this result gives a new way of deciding Presburger arithmetic optimally. Furthermore, our algorithm allows us to positively answer a conjecture by Pak and Nguyel on the VC dimension of Presbuger arithmetic [Combinatorica 39, 2019]. The VC dimension is a fundamental concept from Comptational Learning theory that can be applied to all first-order theories.

2. Separation logic is a well-known logic for the modular verification of pointer programs. An open problem in the area was how to design sound and complete proof systems for its assertion language, the major issue being that the multiplicative connectives of separation logic break all standard techniques used to prove completeness of axiom systems. In a paper published at CSL'20, I showed how to handle this issue, and derived the first sound and complete proof system for a separation logic featuring both multiplicative connectives (the so called separating conjunction and the separating implication). Completeness is shown with a model theoretical technique that is reusable in practice, and that can be adapted to tackle complexity questions.

After a round-up on the aforementioned results, I will move to my current research project, that aims at developing proof techniques and algorithms to mathematically prove the presence of arithmetic errors (e.g., buffer and integer overflows) in programs.


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


Dmitrii Ustiugov

Wednesday, March 16, 2022

10:00am Zoom7 - https://zoom.us/j/7911012202 (pass: @dmitrii)

Dmitrii Ustiugov, PhD Student, Universidad de Edimburgo, Reino Unido

Turbocharging Serverless Research with vHive

Abstract:

Serverless has emerged as the next dominant cloud architecture and paradigm due to its scalability and a flexible billing model. In serverless, developers structure their cloud services as a set of functions connected in a workflow, whereas providers take responsibility for dynamically scaling each function’s resources. This labor division opens opportunities for systems researchers to innovate in serverless computing. However, leading serverless providers, like AWS Lambda, rely on proprietary infrastructure ill-suited for systems research in academia.


Time and place:
10:00am Zoom7 - https://zoom.us/j/7911012202 (pass: @dmitrii)
IMDEA Software Institute, Campus de Montegancedo
28223-Pozuelo de Alarcón, Madrid, Spain


John Hughes

Tuesday, March 15, 2022

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

John Hughes, Professor, Universidad Tecnológica Chalmers, Göteborg, Suecia

Testing Smart Contracts on the Cardano Blockchain with QuickCheck

Abstract:

The Cardano blockchain underlies one of the world's top-ten cryptocurrencies, and supports smart contracts written in Haskell, which work very differently from those on the Ethereum Virtual Machine (the largest smart contract platform). While some vulnerabilities are fixed as a result, it is still possible in principle for large sums to be stolen, or simply lost, due to bugs in smart contracts. Testing smart contracts thoroughly is thus of paramount importance. QuickCheck is a 'property-based testing' tool, that generates random test cases and validates observed system behaviour against a kind of formal specification. But what should a formal specification of a smart contract look like? Quviq has been developing a QuickCheck-based test framework for these smart contracts. I'll talk about the framework itself, and some of the challenges we have addressed, and which remain to be addressed.


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


Yueqi Chen

Thursday, March 10, 2022

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

Yueqi Chen, PhD Student, Universidad Estatal de Pensilvania, EE.UU.

Securing Operating System Kernels with Fewer Shots

Abstract:

Despite significant efforts on cybersecurity, we are observing an increasing number of attacks in recent years. The reason for this harsh reality is all our efforts aim at individual incidents and there is no deep understanding of attack surfaces in software systems. As a result, software systems are integrated with too many individual patches and ad-hoc mitigations, which introduces unacceptable overhead but not substantial security benefits. In this talk, I will present a systematic approach to understanding attack surfaces. This approach provides security analysts and developers with the ability to quantify the impact of attack surfaces and facilitate the development of universal and effective defense solutions. Technically, this approach consists of two steps - induction and deduction. The induction step summarizes the security incident and abstracts the essential attack surface behind the incident. The deduction step generalizes the essential attack surface to different systems and applies it in the exploitation of different error types. By mitigating the generalized attack surface, the developers can design universal protections. In this talk, I will illustrate this research approach starting from a security incident in the Linux kernel. I will present a universal and effective defense that mitigates the generalized attack surface and is widely adopted in various commodity Operating System kernels. In the future, I plan to further advance this systematic approach and make it a fundamental part of the entire software development lifecycles. More specifically, I will: 1) enrich induction and deduction techniques for more attack forms under new contexts, 2) formalize the description of attack surfaces, and 3) quantify the security of systems to optimize and re-construct existing defenses architecture.


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


Kostas Ferles

Thursday, March 7, 2022

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

Kostas Ferles, Post-doctoral Researcher, Universidad de Texas en Austin, EE.UU.

Simple and Efficient Concurrent Programming via Synchronization Synthesis

Abstract:

Multithreaded concurrency is an extremely challenging programming setting, with bugs manifesting themselves in resource starvation and atomicity violations. While there have been efforts to simplify concurrent programming through higher-level programming abstractions, developers tend to choose low-level concurrent programming abstractions (with locks and condition variables as synchronization primitives) due to efficiency issues. This talk will present my recent work on bridging this efficiency vs. programmability trade-off in concurrent programming by employing lightweight formal methods in the compiler. Given a concurrent program implemented in a higher-level programming abstraction, our approach automatically synthesizes efficient and correct-by-construction code implemented in terms of standard synchronization primitives. Specifically, the first part of the talk will demonstrate how to synthesize all necessary signaling operations, and the second part will illustrate how to synthesize a fine-grained locking scheme that maximizes parallelism. As I will demonstrate through empirical results, this approach notably simplifies concurrent programming while achieving optimal performance.


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


Wouter Lueks

Friday, February 25, 2022

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

Wouter Lueks, Post-doctoral Researcher, Ecole Polytechnique Federale de Lausanne, Suiza

Designing End-to-End Privacy-Friendly and Deployable Systems

Abstract:

Digital technology creates risks to people's privacy in ways that did not exist before. I design end-to-end private systems to mitigate these real-world privacy risks. In this talk I will discuss my designs for two applications. These applications highlight key aspects of my work: I analyse security, privacy, and deployment requirements; and address these requirements by designing new cryptographic primitives and system architectures. In the first part of this talk, I will focus on my DP-3T and CrowdNotifier designs for digital proximity and presence tracing that help mitigate the COVID-19 pandemic. These designs combine novel cryptographic primitives and communication systems to protect users’ privacy. The DP3T and CrowdNotifier designs have been deployed to millions of phones. In the second part of this talk, I will present DatashareNetwork, a document search system for investigative journalists that enables them to locate relevant documents for their investigations. DatashareNetwork combines a novel multi-set private set intersection primitive with anonymous communication and authentication systems to create a decentralised and privacy-friendly document search system.


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


Gergely Neu

Friday, February 18, 2022

11:00am Meeting room 302 & Zoom3 https://zoom.us/j/3911012202 (pass: 5551337)

Gergely Neu, Research Assistant Professor, Universidad Pompeu Fabra, España

Information-Theoretic Generalization Bounds for Stochastic Gradient Descent

Abstract:

We study the generalization properties of the popular stochastic optimization method known as stochastic gradient descent (SGD) for optimizing general non-convex loss functions. Our main contribution is providing upper bounds on the generalization error that depend on local statistics of the stochastic gradients evaluated along the path of iterates calculated by SGD. The key factors our bounds depend on are the variance of the gradients (with respect to the data distribution) and the local smoothness of the objective function along the SGD path, and the sensitivity of the loss function to perturbations to the final output. Our key technical tool is combining the information-theoretic generalization bounds previously used for analyzing randomized variants of SGD with a perturbation analysis of the iterates.


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


Daniele Cozzo

Tuesday, January 25, 2022

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

Daniele Cozzo, PhD Student, KU Leuven, Bélgica

Gladius: LWR-based efficient hybrid public key encryption with distributed decryption

Abstract:

Standard hybrid encryption schemes based on the KEM-DEM framework are hard to implement efficiently in a distributed manner while maintaining the CCA security property of the scheme. This is because the DEM needs to be decrypted under the key encapsulated by the KEM, before the whole ciphertext is declared valid. In this paper we present a new variant of the KEM-DEM framework, closely related to Tag-KEMs, which sidesteps this issue. We then present a post-quantum KEM for this framework based on Learning-with-Rounding, which is designed specifically to have fast distributed decryption. Our combined construction of a hybrid encryption scheme with Learning-with-Rounding based KEM, called Gladius, is closely related to the NIST Round 3 candidate called Saber. We wrote prototype distributed implementation that achieves a decapsulation time of 4.99 seconds for three parties.


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


Pierre Civit

Tuesday, January 18, 2022

11:00am Zoom5 - https://zoom.us/j/5911012202 (pass: 5551337)

Pierre Civit, PhD Student, Universidad Sorbona, Francia

Accountability in distributed systems

Abstract:

Consider a distributed protocol whose n processes ensure some (distributed) safety and liveness properties, communicating with each other without synchrony, despite a certain the number t of Byzantine processes. It has been known for decades that such distributed protocols cannot ensure safety as soon as more than a threshold of t_0 processes fail, typically one third of the processes.

By contrast, only recently did the community discover that some of these distributed protocols can be made accountable by ensuring that correct processes detect at least t_0 + 1 faulty processes responsible of any safety violation. This is particularly surprising (and positive) given that accountability is a powerful tool to mitigate safety violations in distributed protocols. Indeed, exposing crimes and punishments naturally incentivizes exemplarity.

We propose a generic transformation of any distributed protocol into an accountable version of this protocol. First, we partition the commission faults into two classes: the equivocation faults and the evasion faults and illustrate why the former are are easier and less cumbersome to detect than the latter. Our transformation builds upon the secure broadcast primitive in a way ensuring that every safety violation is necessarily a consequence of equivocation faults.

Due to the secure broadcast primitive, our transformation increases the communication and message complexities of the original distributed protocol by an O(n^2) multiplicative factor in the worst case.


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


Hamza Abusalah

Monday, January 10, 2022

11:30am Zoom9 - https://zoom.us/j/9911012202 (pass: s3)

Hamza Abusalah, Post-doctoral Researcher, Universidad Técnica de Viena, Austria

SNACKs: Leveraging Proofs of Sequential Work for Blockchain Light Clients

Abstract:

We revisit the problem of designing light-client blockchain protocols from the perspective of classical proof-system theory. This results in a framework that allows quantifying the security guarantees provided to a light-client verifier even when interacting only with a single dishonest (full-node) prover. We define a new primitive called succinct non-interactive argument of chain knowledge (SNACK) capturing this intuition and show how augmenting any blockchain with a graph-labeling proof of sequential work (GL-PoSW) enables SNACK proofs for this blockchain. We also provide a unified and extended definition of GL-PoSW covering all existing constructions and describe a new variant. We then show how SNACKs can be used to construct light-client protocols, and highlight some deficiencies of existing solutions. (Joint work with: Georg Fuchsbauer, Peter Gazi, and Karen Klein)


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


Charlas Invitadas - 2021