Jovan Komatovic, PhD student, Distributed Computing Laboratory(EPFL)
Byzantine agreement, a fundamental problem in distributed computing, enables $N$ processes to reach consensus on a common value despite up to $T < N$ arbitrary failures. It serves as the backbone of critical distributed services such as distributed key generation (DKG), secure multi-party computation (MPC), blockchain technologies, and state machine replication (SMR), highlighting its crucial role in modern computing. Despite their importance, existing agreement protocols face significant limitations. Many struggle to scale efficiently due to poor performance or heavy reliance on cryptographic tools such as threshold signatures, which require expensive setup and computationally intensive algebraic operations. Furthermore, dependence on these “heavyweight” cryptographic primitives weakens their security in a post-quantum world. As agreement protocols continue to grow in scale and importance, there is an urgent need for solutions that are both efficient and resilient to emerging security threats and future technological advancements. In this talk, I will present the first complexity-optimal agreement protocols that either rely only on “lightweight” cryptographic primitives, such as hash functions, or eliminate the need for cryptography entirely. These solutions cover all major network models— asynchrony, partial synchrony, and synchrony—matching or exceeding the best-known results while relying on minimal cryptographic assumptions.
Time and place:
11:00am 302-Mountain View and Zoom3 (https://zoom.us/j/3911012202, password:@s3)
IMDEA Software Institute, Campus Montegancedo
28223-Pozuelo de Alarcón, Madrid, Spain
Lucianna Kiffer, Research Assistant Professor, IMDEA Networks
Many blockchain networks aim to preserve the anonymity of validators in the peer-to-peer (P2P) network, ensuring that no adversary can link a validator’s identifier to the IP address it is running from, due to associated privacy and security concerns. This talk presents work that demonstrates that the Ethereum P2P network does not offer this anonymity. I will present our methodology that enables any node in the network to identify validators hosted on connected peers and empirically verify the feasibility of the proposed method. Using data collected from four nodes over three days, we locate more than 15% of Ethereum validators in the P2P network. The insights gained from our deanonymization technique provide valuable information on the distribution of validators across peers, their geographic locations, and hosting organizations. The work presented in this talk has been awarded a bug bounty by the Ethereum Foundation.
Time and place:
11:00am 302-Mountain View and Zoom3 (https://zoom.us/j/3911012202, password:@s3)
IMDEA Software Institute, Campus Montegancedo
28223-Pozuelo de Alarcón, Madrid, Spain
Grigory Fedyukovich, Assistant Professor, Florida State University
State-of-the-art solvers for constrained Horn clauses (CHC) are successfully used to generate reachability facts for software using its symbolic encoding. In this talk, I will present a new application of CHCs to test-case generation, a problem of finding a set of tuples of input values to a program under which the program visits as many branches as possible. The key insight to achieve maximality is to identify and skip blocks of code that are provably unreachable. The new approach to test case generation called HORNTINUUM uses CHC to incrementally construct different program unrollings and extract test cases from models of satisfiable formulas. At the same time, a CHC solver keeps track of CHCs that represent unreachable blocks of code which makes the unrolling process more efficient. In practice, this lets HORNTINUUM terminate early while guaranteeing maximal coverage. HORNTINUUM exhibits promising performance: it generates high coverage in the majority of cases and spends less time on average than state-of-the-art based on bounded model checking, concolic execution, and/or fuzzing.
Time and place:
11:00am 302-Mountain View and Zoom3 (https://zoom.us/j/3911012202, password:@s3)
IMDEA Software Institute, Campus Montegancedo
28223-Pozuelo de Alarcón, Madrid, Spain
Miguel Ambrona, Cryptography Engineer, Input Output Global (IOHK)
The FIDE Laws of Chess establish that if a player runs out of time during a game, they lose unless there exists no sequence of legal moves that ends in a checkmate by their opponent, in which case the game is drawn. The problem of determining whether or not a given chess position is unwinnable for a certain player has been considered intractable by the community and, consequently, chess servers do not apply the above rule rigorously, thus unfairly classifying many games. We propose, to the best of our knowledge, the first algorithm for chess unwinnability that is sound, complete and efficient for practical use. We also develop a prototype implementation and evaluate it over the entire Lichess Database (containing more than 6 billion games), successfully identifying all unfairly classified games in the database.
Time and place:
11:00am 302-Mountain View and Zoom3 (https://zoom.us/j/3911012202, password:@s3)
IMDEA Software Institute, Campus Montegancedo
28223-Pozuelo de Alarcón, Madrid, Spain
María Elena Gomez Martinez, Research Professor, Universidad Complutense de Madrid
Petri nets (PN) are a popular formalism to represent concurrent systems. However, they lack support for modelling and analysing system families, like variants of controllers, process models, or configurations of flexible assembly lines. a Petri net product line (PNPL) defines a collection of similar systems compactly. A PNPL represents a set of Petri nets with different admissible derivations. Having just one artefact allows for analysing all derivable nets of a family more efficiently at the same time, instead of one by one. Thus, PNPLs permit the analysis of structural and behavioural properties and the runtime verification of reconfigurable systems. In addition, a software tool has been developed to evaluate the benefits of our proposal.
Time and place:
11:00am 302-Mountain View and Zoom3 (https://zoom.us/j/3911012202, password:@s3)
IMDEA Software Institute, Campus Montegancedo
28223-Pozuelo de Alarcón, Madrid, Spain