Reasoning about hyperproperties of concurrent implementations, such as the guarantees these implementations provide to randomized client programs, has been a long-standing challenge. Standard linearizability enables the use of atomic specifications for reasoning about standard properties, but not about hyperproperties. A stronger correctness criterion, called strong linearizability, enables such reasoning, but is rarely achievable, leaving various useful implementations with no means for reasoning about their hyperproperties. In this paper, we focus on registers and devise non-atomic specifications that capture a wide-range of well-studied register implementations and enable reasoning about their hyperproperties. First, we consider the class of write strong-linearizable implementations, a recently proposed useful weakening of strong linearizability, which allows more implementations, such as the well-studied single-writer ABD distributed implementation. We introduce a simple shared-memory register specification that can be used for reasoning about hyperproperties of programs that use write strongly-linearizable implementations. Second, we introduce a new linearizability class, which we call decisive linearizability, that is weaker than write strong-linearizability and includes multi-writer ABD, and develop a second shared-memory register specification for reasoning about hyperproperties of programs that use register implementations of this class. These results shed light on the hyperproperties guaranteed when simulating shared memory in a crash-resilient message-passing system.

Based on joint work with Yoav Ben Shimon and Sharon Shoham presented as DISC'24.

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.

In the zoo of programming languages there are two cute yet rather misbehaved animals, typically found in the Dynamic Languages section: the Duck Typing and the Monkey Patching. The Duck Typing is hardly seen. You hear a “quack!”, but you can’t easily tell if it’s coming from an actual duck, a parrot, or a recording. Monkey Patching, like the name suggests, patches any existing creature to change their behavior. It can even make a dog quack! While these two animals bring lots of joy, they are also quite dangerous when used in the wild, as they can bring unexpected behavior to the rest of the creatures. Crystal is a rarity in the Static Languages section that has Duck Typing and Monkey Patching. Given the strong —yet barely visible— fences of types, it manages to properly contain these beasts. In this talk I will present Crystal and provide a glimpse at how it manages to feel so dynamic.

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.

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.