2025 talks

David Trabish
Technion

31/12, 11:30
Location: TBD

Title: Enhancing Symbolic Execution with Machine-Checked Safety Proofs
Abstract:
Symbolic execution (SE) is a program analysis technique that executes the program with symbolic inputs. In modern SE engines, when the analysis of a given program is exhaustive, the analyzed program is typically considered safe, i.e., free of bugs, but no formal guarantees are provided to support this. Rather than aiming for a formally verified SE engine that will provide such guarantees, which is challenging, we propose a systematic approach where each individual analysis additionally outputs a formal safety proof that validates the symbolic computations that were carried out.
Our approach consists of two main components: A formal framework connecting concrete and symbolic semantics, and an instrumentation of the SE engine that generates formal safety proofs based on this framework. We showcase our approach by implementing a KLEE-based prototype that operates on a subset of LLVM IR with integers and generates proofs in Coq.
Our preliminary experiments show that our approach generates proofs that have reasonable validation times, while the instrumentation incurs only a minor overhead on the SE engine.
In addition, during the implementation of our prototype, we found previously unknown semantic implementation issues in KLEE.

Shir Cohen
Researcher at Gen Labs

3/12, 10:30
Location: Zisapel Building 506

Title:  Bridging Theory and Practice in Distributed Systems

Abstract:
Distributed systems must be worthy of the trust we place in them, yet theory and practice often speak different languages. My research bridges this gap by using theoretical rigor to solve practical problems and real-world deployments to surface new theoretical questions.

In this talk, I will present work spanning theoretical and practical aspects of distributed systems. I developed the first sub-quadratic asynchronous Byzantine Agreement algorithm, showing that consensus can be achieved with near-linear communication even without timing assumptions – resolving a long-standing open question. I will also discuss recent work on building and analyzing distributed systems at scale. Together, these projects illustrate how theoretical insights and practical demands can inform each other in the design of reliable distributed infrastructures.

Short bio:

Shir Cohen is a researcher at Gen Labs working on scalable distributed systems. She completed her PhD in Computer Science at Technion under the supervision of Prof. Idit Keidar, where she focused on Byzantine fault tolerance and efficient consensus protocols, and was subsequently a postdoctoral researcher at Cornell University with Prof. Lorenzo Alvisi in the Systems Lab. Her research bridges theory and practice in distributed systems.


Itay Flam

Technion

Title: Communication Abstractions for Optimal Byzantine Resilience

26/11, 11:30
Taub 601

*The lecture will be given in Hebrew*

Abstract:
We study communication abstractions for asynchronous Byzantine fault tolerance with optimal failure resilience, where n > 3f . Two classic patterns—canonical asynchronous rounds and communication-closed layers—have long been considered as general frameworks for designing distributed algorithms, making asynchronous executions appear synchronous and enabling modular reasoning. We show that these patterns are inherently limited in the critical resilience regime 3f < n ≤5f . Several key tasks—such as approximate and crusader agreement, reliable broadcast and gather—cannot be solved by bounded-round canonical-round algorithms, and are unsolvable if communication closure is imposed. These results explain the historical difficulty of achieving optimal-resilience algorithms within round-based frameworks. On the positive side, we show that the gather abstraction admits constant-time solutions with optimal resilience (n > 3f ), and supports modular reductions. Specifically, we present the first optimally-resilient algorithm for binding connected consensus by reducing it to gather. For completeness, we present an optimally-resilient algorithm for gather which terminates in constant time. Our results demonstrate that while round-based abstractions are analytically convenient, they obscure the true complexity of Byzantine fault-tolerant algorithms. Richer communication patterns such as gather provide a better foundation for modular, optimal-resilience design.

M.Sc. student under the supervision of Prof. Hagit Attiya

Barak Gerstein
Technion

Making congestion control robust to per-packet load balancing in datacenters

On 28/10 at 16:00
Mayer 1061 and Zoom

Per-packet load-balancing approaches are increasingly deployed in datacenter networks. However, their combination with existing congestion control algorithms (CCAs) may lead to poor performance and even throughput collapse.

In this talk, I first model the throughput collapse of a wide array of CCAs when some of the paths are congested. I explain that since CCAs are typically designed for single-path routing, their estimation function focuses on the latest feedback and mishandles feedback that reflects multiple paths. I propose to use a median feedback that is more robust to the varying signals that come with multiple paths. I introduce MSwift, which applies this principle to make Google’s Swift CCA robust to multi-path routing while keeping its incast tolerance and single-path performance. Finally, I demonstrate that MSwift improves the 99th-percentile FCT by up to 25%, both with random packet spraying and adaptive routing.

M.Sc. student under the supervision of Prof. Isaac Keslassy and Prof. Mark Silberstein.


Saar Tzour-Shaday
Technion

On 17/9/2025 at 11:30

Mayer 1061 and Zoom

Mini-Batch Robustness Verification of Deep Neural Networks
Neural network image classifiers are ubiquitous in many safety-critical applications. However, they are susceptible to adversarial attacks. To understand their robustness to attacks, many local robustness verifiers have been proposed to analyze epsilon-balls of inputs. Yet, existing verifiers introduce a long analysis time or lose too much precision, making them less effective for a large set of inputs. In this work, we propose a new approach to local robustness: group local robustness verification. The key idea is to leverage the similarity of the network computations of certain epsilon-balls to reduce the overall analysis time. We propose BaVerLy, a sound and complete verifier that boosts the local robustness verification of a set of epsilon-balls by dynamically constructing and verifying mini-batches. BaVerLy adaptively identifies successful mini-batch sizes, accordingly constructs mini-batches of epsilon-balls that have similar network computations, and verifies them jointly. If a mini-batch is verified, all its epsilon-balls are proven robust. Otherwise, one epsilon-ball is suspected as not being robust, guiding the refinement. BaVerLy leverages the analysis results to expedite the analysis of that epsilon-ball as well as the analysis of the mini-batch with the other epsilon-balls. We evaluate BaVerLy on fully connected and convolutional networks for MNIST and CIFAR-10. Results show that BaVerLy scales the common one by one verification by 2.3x on average and up to 4.1x, in which case it reduces the total analysis time from 24 hours to 6 hours.

MSc Seminar. Supervisor: Dr. Dana Drachsler Cohen

Roi Bar-Zur
Technion

On 3/9/2025 at 11:30
Mayer 1061 and Zoom

Blockchain Analysis with Reinforcement Learning
Blockchains secure trillions of dollars in value while operating in adversarial environments where rational actors pursue economic gain. When economic incentives fail to align with system security, critical vulnerabilities emerge. This talk examines how to identify and defend against these vulnerabilities across different decentralized systems.

First, I will present analysis of optimal selfish mining strategies, where miners manipulate the protocol for profit, particularly in scenarios where previously unexplored attack vectors are created by complex revenue structures and potential collaboration with other miners. I demonstrate how rational participants that deliberately assist attackers for their own gain risk the whole system’s security. Building on this analysis, I introduce a novel protocol that, compared to Bitcoin’s current implementation, provides stronger resistance to these collaborative selfish mining attacks.
Second, I will address vulnerabilities in restaking networks, an emerging paradigm where operators use their locked capital across multiple decentralized applications simultaneously. While restaking improves capital efficiency, the stake reuse introduces new risks. I present a more robust restaking architecture that better balances the economic benefits and potential risks.
Together, these contributions advance our understanding of how to align incentives with security in decentralized systems and provide practical solutions for their design.
PhD Seminar. Supervisor: Prof. Ittay Eyal and Prof. Aviv Tamar.

Shalev Kuba
Technion
 On 30/7/2025 at  11:30
Taub 301 and zoom

Online Deduplicated Data Migration

Abstract: In storage systems, the data migration process periodically remaps files between volumes with the goal of preserving the system’s load balance and deduplication efficiency. Previous studies focused on offline selection of files to migrate, a task complicated by the inter-file dependencies introduced by deduplication. However, they did not address the possibility of files entering and leaving the system due to user actions, nor the order between individual file transfers. Our motivational study reveals that naïve ordering may create traffic spikes and leave the system in poorly balanced intermediate states. To address these challenges, we present Slide—a novel online migration approach based on sliding windows. Slide takes advantage of long-term planning to maximize deduplication efficiency while maintaining short-term load balance and adapting to system changes. It achieves superior load balancing than alternative approaches while incurring minimal increase in the overall system size.

M.Sc. student under the supervision of Prof. Gala Yadgar.


Nicolás Wainstein
Technion
On 21/5/2025 at 11:30
Mayer 1061 and zoom

Towards Energy-Efficient AI Hardware: Mixed-Signal In-Memory Computing and Ultra-Dense Die-to-Die Links

Abstract: The rapid advancement of artificial intelligence (AI) is pushing the limits of conventional digital computing architectures. Key performance bottlenecks–computational efficiency, memory bandwidth, and interconnect performance–are becoming increasingly critical, especially for edge AI applications that demand low latency and ultra-low power consumption. In this talk, I will present my recent research aimed at overcoming these challenges through a multidisciplinary approach focusing on three main pillars: 1) analog/mixed-signal circuits, 2) in-memory computing (IMC), and 3) high-speed die-to-die (D2D) links. I will show how time-domain IMC using nonvolatile emerging memory technologies, such as ferroelectric FETs, can improve the energy-efficiency of AI hardware, as demonstrated by a prototype in 28 nm CMOS. I will also present a mixed-mode fast-locking delay-locked loop for latency-critical parallel links (such as D2D), implemented in a 3 nm FinFET CMOS process. These works span CMOS and emerging device technologies, combining insights from device physics, circuit design, and system architecture to enable the next generation of high-performance, energy-efficient AI hardware.

Bio: Nicolas Wainstein is a Research Fellow at the ECE faculty at the Technion. From 2021 to 2024, he was a Senior Analog/Mixed-Signal Design Engineer and Technical Lead at Intel, Israel, working on high-speed parallel wireline links, such as DDR and die-to-die (D2D) communication. He earned his PhD in Electrical Engineering from the Technion, supervised by Prof. Shahar Kvatinsky and Prof. Eilam Yalon. Nicolás was the recipient of several awards, including the Hershel Rich Innovation Award, the IEEE Electron Devices Society Ph.D. Student Fellowship (Europe and Middle East region), the Yablonovitch Research Prize, the 1st place in the RBNI Prize for Excellence in Nanoscience and Nanotechnology, and the Jury Award for Outstanding Students.


Yotam Gafni
Weizmann

On 7/5/2025 at 11:30
Mayer 1061 and Zoom

Designing Blockchain Fees

Abstract: Miner fees are a key component in the incentive scheme of properly running Blockchains’ decentralized transaction processing. In determining how fees work, we should consider many different goals: Efficient allocation, simplicity for users, and robustness to possible manipulation vectors. We consider this problem through the lens of auction theory, and characterize the tradeoffs different mechanisms may offer, in particular w.r.t. the threat of miner-user collusion.
The talk is based on joint works with Aviv Yaish, Matheus Ferreira, and Max Resnick.


Michael Mirkin
Technion

On 23/4/2025 at 11:30 
Mayer 1061  and  Zoom
 
Blockchain: Unmotivating, Overpowered, Underperforming — and Still Full of Potential
 

Blockchain networks like Bitcoin and Ethereum underpin billions in value and promise decentralized trust, yet they face critical challenges: their security depends on fragile economic incentives, their energy consumption raises sustainability concerns, and their limited computational capacity constrains scalability.

In this talk, I’ll share our research on all three fronts. First, I’ll explore incentive vulnerabilities in proof‑of‑work that can disrupt participation and threaten system integrity. Then I’ll question the “more security means more power” mantra, showing how shifting costs toward hardware acquisition can achieve the same level of security with far less energy. Finally, I’ll present our new approach to extending on‑chain computation, unlocking fresh possibilities for smarter, more scalable contracts.

Dr. Nadav Amit
Technion
On 2/4/2025 at 11:30
Meyer building 1061 and Zoom

When a File Means a File: Proper Huge Pages for Code

Abstract: Despite huge pages dramatically reducing CPU frontend stalls from address translation, their use for executable code remains limited due to operating system constraints and impracticality of rebuilding system binaries with special alignment. Current solutions that copy code into huge pages break essential system functionality – preventing memory sharing between processes, disrupting debugging tools, and interfering with memory management operations.In this talk, I will present a practical userspace solution that achieves huge page performance benefits while preserving critical system services. Our approach transforms binaries to align code segments with huge page boundaries post-linkage while maintaining all internal references, and orchestrates page cache operations to ensure proper mapping. PostgreSQL evaluations demonstrate up to 7% performance improvement through a 94% reduction in iTLB misses, while maintaining memory sharing, debugging support, and proper memory management.


Dr. Daniel Amir
Technion
On 26/2/2025 at 11:30
Meyer building 1061 and Zoom

Oblivious Reconfigurable Datacenter Networks
As Moore’s Law slows down, packet switch capabilities are falling behind datacenter demands. This has made optical circuit switches increasingly attractive in datacenter networks. These switches have already seen significant commercial use in the form of hybrid networks, which combine both packet switches and circuit switches. Recent advances in optical circuit switching technology can now operate fast enough to potentially fully replace packet switches, when combined with novel network designs.
This talk presents my research into Oblivious Reconfigurable Networks (ORNs), a design paradigm capable of using the full capabilities of emerging fast circuit switches. I will describe Shale, an ORN that achieves a tunable tradeoff between throughput and latency which is Pareto optimal for ORNs. Along the way, I will also touch on the current state of the art in commercially-deployed hybrid networks. Finally, I will discuss our present research into Semi-Oblivious Reconfigurable Networks (SORNs), which extend ORNs with intuitions found in commercial hybrid networks to further improve the performance possible on fast circuit-switched networks.

Prof. Rafael Pass

Tel-Aviv University

On 19/2/2025 at 11:30
Meyer building 1061 and Zoom

On Cryptography and Kolmogorov Complexity
Whether secure Cryptography exists is one of the most important open problems in Computer Science: Cryptographic schemes today rely on unproven computational hardness assumption.
We will survey a recent thread of work (Liu-Pass,FOCS’20, Liu-Pass-STOC’21,.., Ball-Liu-Pass-Mazor, FOCS’23, Liu-Pass’EUROCRYPTO’24) showing *equivalences* between the existence of some of the most basic cryptographic primitives, and the hardness of various computational problems related to the notion of *time-bounded Kolmogorov Complexity* (dating back to the 1960s).
These results yield the first natural computational problems *characterizing* the feasibility of central primitives and protocols in Cryptography, as well as the first *unstructured* computational problems enabling public-key cryptography.
No prior knowledge of Cryptography or Kolmogorov complexity will be assumed.

Marwa Mouallem

Technion

On 12/2/2025 at 11:30
Meyer building 1061 and Zoom
Asynchronous Authentication

Abstract: A myriad of authentication mechanisms embody a continuous evolution from verbal passwords in ancient times to contemporary multi-factor authentication: Cryptocurrency wallets advanced from a single signing key to using a handful of well-kept credentials, and for online services, the infamous “security questions” were all but abandoned. Nevertheless, digital asset heists and numerous identity theft cases illustrate the urgent need to revisit the fundamentals of user authentication.

We abstract away credential details and formalize the general, common case of asynchronous authentication, with unbounded message propagation time. Given credentials’ fault probabilities (e.g., loss or leak), we seek mechanisms with maximal success probability. Such analysis was not possible before due to the large number of possible mechanisms. We show that every mechanism is dominated by some Boolean mechanism-defined by a monotonic Boolean function on presented credentials.  We present an algorithm for finding approximately optimal mechanisms by leveraging the problem structure to reduce complexity by orders of magnitude.
The algorithm immediately revealed two surprising results: Accurately incorporating easily-lost credentials improves cryptocurrency wallet security by orders of magnitude. And novel usage of (easily-leaked) security questions improves authentication security for online services.

Oleg Kolosov

Technion
On 5/2/2025 at 11:30
Taub Building 8
Workloads, Storage, and Service Allocation in Edge Computing

Abstract. Edge computing extends cloud capabilities to the proximity of end-users, offering ultra-low latency, which is essential for real-time applications. Unlike traditional cloud systems that suffer from latency and reliability constraints due to distant datacenters, edge computing employs a distributed model, leveraging local edge datacenters to process and store data.

This talk explores key challenges in edge computing across three domains: workloads, storage, and service allocation. The first part focuses on the absence of comprehensive edge workload datasets. Current datasets do not accurately reflect the unique attributes of edge systems. To address this, we propose a workload composition methodology and introduce WoW-IO, an open-source trace generator. The second part examines aspects of edge storage. Edge datacenters are significantly smaller than their cloud counterparts and require dedicated solutions. We analyze the applicability of a promising mathematical model for edge storage systems and raise inherent gaps between theory and practice. The final part addresses the virtual network embedding problem (VNEP). In VNEP, given a set of requests for deploying virtualized applications, the edge provider has to deploy a maximum number of them to the underlying physical network, subject to capacity constraints. We propose novel solutions, including a proactive service allocation strategy for mobile users, a flexible algorithm for service allocation that is adaptable to the underlying physical topology, and  an algorithm for scalable online service allocation.

Dr. Ben Nassi
Technion
On 29/1/2025 at 11:30
Zisapel Building 506
 
Securing Modern Systems is More Challenging Than Ever (and Requires New and Dedicated Guardrails).
Abstract. Over the past decade, an increasing number of systems and devices have gained Internet connectivity and been enhanced with sensing capabilities and AI. While these advancements have created a world of smarter, more automated, and highly connected devices, they have also introduced significant security and privacy challenges that cannot be effectively addressed with traditional countermeasures.

In the first part of this talk, we will explore the security and privacy concerns of cyber-physical systems. Specifically, we will examine new threats that have emerged with the deployment of technologies like drones and Teslas in real-world environments. Our discussion will highlight methods for detecting intrusive drone filming and securing Teslas against time-domain adversarial attacks.The second part of the talk focuses on the challenges posed by the coexistence of functional devices with limited computational power (that do not adhere to Moore’s law) alongside sensors with ever-increasing sampling rates. We will explore how threats such as cryptanalysis and speech eavesdropping—previously accessible only to well-resourced adversaries—can now be executed by ordinary attackers using readily available hardware like photodiodes and video cameras. These attacks leverage optical traces or video footage from a device’s power LED to extract sensitive information.

Finally, in the last part of the talk, we will address the emerging need to secure GenAI-powered applications against a new category of threats we call Promptware. This threat highlights the evolving landscape of vulnerabilities introduced by generative AI systems.

Skip to content