A Semantic Approach to Verifying Programmable Networks
Abstract
As networks become more programmable, they are increasingly built around flexible software components. While this programmability enables new functionality and faster innovation, it also makes network behavior harder to reason about. In this talk, I will present a research agenda that brings ideas from formal methods to programmable networks. In particular, I will present techniques that leverage programmable-network semantics for concurrency safety, traffic monitoring, and failure recovery. More broadly, this work illustrates how semantic foundations can help bring stronger correctness guarantees to modern networked systems.
Bio
Guy Amir is a Postdoctoral Researcher at Cornell University, conducting research at the intersection of formal methods, networking, and systems. He earned his Ph.D. in 2024 from the Hebrew University of Jerusalem, where he studied AI safety, focusing on formally verifying reactive AI systems and interpreting neural networks. He holds an M.Sc. in Computer Science and a B.Sc. in Computational Biology and Computer Science, both from the Hebrew University. He has received Rothschild, Fulbright, AI-Net, and Charles Clore fellowships, as well as an ICML Spotlight and KLA Award.
Or David
The Secret Sauce of Distributed Agreement
Abstract: Agreement problems in general, and Consensus in particular, share fundamental characteristics that have been the subject of extensive research and comparative literature. This work utilizes knowledge theory (epistemic logic) to formally characterize these problems within fault-prone distributed environments. Specifically, we provide a logical characterization of a large class of All-or-Nothing (AoN) agreement problems, including Consensus, Reliable Broadcast, Coordinated Attack and Atomic Commitment. This characterization is built upon the notion of dynamic common knowledge (DCK), a concept recently introduced by Gonczarowski and Moses, which we adapt here for fault-prone distributed systems. By doing so, we offer a new, model-independent approach to the design, analysis, and optimization of agreement protocols. To demonstrate the power and practical utility of this knowledge-theoretic framework, we apply it to two distinct scenarios: optimizing a Consensus protocol in a synchronous crash-failure model, and streamlining Bracha’s reliable broadcast protocol in an asynchronous system with Byzantine failures. At the core of this work is the mathematical formalization establishing that DCK is both a necessary and sufficient condition for solving All-or-Nothing agreement. In essence, DCK provides a way to capture the required “state of agreement” among non-faulty processes without forcing them to reach their decisions at the exact same instant. We prove that any protocol satisfying the AoN condition inherently generates this dynamic knowledge. Conversely, we establish a sufficiency theorem: if a system guarantees that a set of facts satisfies Validity (the value is allowed), Exclusivity (no conflicting values are decided), and Epistemic Sufficiency (the fact ensures its own DCK), these facts are entirely sufficient to construct a working agreement protocol. Ultimately, this logical characterization transcends specific network models or failure assumptions, offering a unifying lens through which to view distributed agreement. By demonstrating that attaining DCK is the fundamental epistemic engine driving these protocols, our framework not only demystifies the structure of classical solutions but provides a rigorous, systematic blueprint for designing leaner and more efficient distributed algorithms in the future.
MSc seminar. Supervisor: Prof Yoram Moses
Abstract: Reservoir computing is an emerging recurrent neural network paradigm that can perform a wide range of tasks, including image recognition and time-series prediction, with simple training, smaller area, and lower energy consumption. It consists of a reservoir layer, which can be built from a time-varying dynamical system, and a readout layer, which is the only part that is trained. Memristors, particularly volatile memristors, are well-suited for constructing the reservoir because their natural decay and nonlinear response allow them to retain recent input information for a short time and act as leaky integrators. In this talk, I will show how volatile memristors can be used to build reservoirs for two tasks: image recognition and time-series prediction. I will explain how the input must be encoded differently for each task to obtain better reservoir states and improve performance. I will also discuss the main design trade-offs involved in these systems, and analyse how important memristor properties such as decay rate, quantization, and device variability affect accuracy, robustness, and hardware cost. By comparing these two tasks within the same reservoir computing framework, I will highlight practical insights into how memristive reservoir systems can be designed and adapted for different applications.MSc seminar. Supervisor: Prof Shahar Kvatinsky
Tel Aviv University
Title: Arm Weak Memory Consistency on Apple Silicon: What Is It Good For?
Abstract: Weak memory models such as the Arm model are perceived as enabling higher performance than strong models such as TSO. We critically test this perception on Apple silicon CPUs, whose runtime-configurable TSO mode enables a direct comparison with native Arm mode. We find that Apple silicon TSO mode preserves Arm weak-memory optimizations, typically yielding execution times within 3% of Arm mode across modern applications and classic benchmarks. Although some applications experience higher TSO slowdowns, we trace these to artifacts of Apple’s TSO implementation rather than inherent TSO ordering constraints. Our results challenge the perception that the Arm memory model offers a significant performance advantage over TSO in Apple silicon.
Alon Levi
Raissa Nataf
Technion
26/3/2026, 10:30
Location: Zoom https://technion.zoom.us/j/96302344036
Distributed asynchronous systems often require explicit synchronization to ensure the correct implementation of shared objects.
Alon Nemirovsky
Real-time speech source separation in a dynamic environment poses significant challenges for wearable augmented reality (AR) devices due to moving sources, head rotations, and adverse acoustic conditions. This seminar presents a robust bilinear framework that integrates minimum power distortionless response (MPDR) beamforming with weighted prediction error (WPE) dereverberation. By decoupling spatial and temporal filtering, we enable efficient recursive least squares (RLS) adaptation that tracks changes in the acoustic scene. To further improve robustness against steering vector errors caused by direction-of-arrival (DOA) mismatches, we introduce region-of-interest (ROI) beamforming. Additionally, we present a linearly constrained minimum power (LCMP) extension to enable flexible spatial control. Our comprehensive analysis of the framework, combined with robust ROI and LCMP extensions validated on real-world SPEAR recordings, establishes a practical and efficient solution for real-time audio enhancement in wearable AR systems.
Technion
Location: Zoom only https://technion.zoom.us/j/96241318455
Seize the Moment: An Information Gain Guided Split for Scaling Neural Network Verification
Abstract:
Verifying the local robustness of neural networks is crucial for understanding their safety level.
However, the complexity of a complete analysis is exponential in the number of unstable neurons, which introduce nonlinearity.
To scale, many complete verifiers split the verification task into smaller subtasks and select a split by relying on heuristics or learning.
We study the problem of finding optimal splits and phrase it as information gain maximization whose goal is to reduce the number of unstable neurons.
The challenge is that the information gain is defined over probabilities that are intractable to compute.
We present SIGNAL which efficiently computes a split by relying on a differentiable estimate of this information gain.
Our key idea is to extend moment propagation to the setting of local robustness verification.
We prove that our differentiable estimate converges to the true value as the neurons’ input dimensionality grows.
We integrate SIGNAL in the alpha-beta-CROWN verifier.
For fully-connected networks, whose neurons have high input dimensionality, SIGNAL scales prior approaches by at least 1.6x on average.
For the task of computing the largest robust $\epsilon$-ball, within 2 hours, SIGNAL
computes 1.25x larger radius for fully-connected and convolutional networks.
MSc seminar. Supervisor: Dr. Dana Drachsler Cohen
Dr. Aviv Yaish
Yale University
On 11/02/2026 at 10:30
Location: 506, Zisapel Building and Zoom
Title: Deconstructing and Rebuilding Trust in Decentralized Economies
Abstract:
Financial systems are becoming increasingly digital and decentralized, demanding a practical fusion of distributed systems security and economic theory. A key enabler of this change, blockchain technology, promises more private and egalitarian economic mechanisms, built by facilitating consensus between pseudonymous actors. However, the theoretical security of these systems may mask significant real-world risks. In this talk, I will present recent advances in bridging this gap between theory and practice. First, I will discuss the resolution of a decade-old puzzle: the lack of observed attacks on major consensus mechanisms. I will then distill the lessons learnt into a holistic approach to designing robust systems and demonstrate its adoption in practice using several lines of work on the economics and security of modern digital markets, tackling problems including denial-of-service resistance in distributed systems and pseudonymous markets where consumers may cheaply create new identities.
Bio:
Aviv is a postdoc at Yale University, where he makes and breaks distributed systems by bridging economic theory and practice. His approach is driven by a philosophy of constructive deconstruction: pushing systems to their limits is key to making them robust. Aviv’s work has been recognized across several fields: security (CCS Distinguished Paper award), economics (CBER Best Paper award), and industry (three prizes from the Ethereum Foundation and Flashbots). He earned his Ph.D. in Computer Science from the Hebrew University (HUJI), where he was the sole lecturer for large-scale courses and won a teaching award. During his studies, he served as a research consultant at Matter Labs. His honors include the AIANI and Jabotinsky fellowships, and inclusion in HUJI’s top 10 CS teaching staff of ‘20, CBER’s Top PhD Graduates of ‘23-‘24, CBER’s Rising Stars of ’25, and HUJI’s 40 Under 40 of ‘25 lists.
Tel-Aviv University
Abstract:
Recent advances in natural language processing (NLP) have given rise to transformative models, including large language models (LLMs) and text retrievers. Still, critical concerns remain regarding the security of these models: chiefly, LLMs can be jailbroken and misused (e.g., to launch cyberattacks), and text retrievers in search applications can be manipulated to prioritize adversary-chosen content. In this talk, I will present our recent efforts toward making LLMs and text retrievers more secure. In particular, I will show how potent attacks can provide explanations for models’ vulnerabilities, which, in turn, enable us to enhance security. Crucially, I will also demonstrate how our insights can inform the design of even stronger attacks, establishing a cycle that guides continuous model improvements.Based on joint work with Matan Ben-Tov and Mor Geva.
Title: ToggleCCI: Dynamic Cost Optimization for Multi-Cloud Transfers
Abstract: Cloud computing is now extremely common, and many organizations operate workloads across multiple providers. As a result, cross-cloud data transfer has become a critical requirement in modern distributed systems. New services such as Google Cross-Cloud Interconnect (CCI) offer dedicated, high-throughput links with low per-GB transfer costs. Yet these benefits come with high fixed leasing fees and a provisioning delay of several days, creating a difficult cost-performance trade-off under unknown traffic patterns.
In this talk, we study the problem of online cross-cloud routing, where decisions must be made without future knowledge. We show that no online algorithm can guarantee constant-factor optimality. To address this, we introduce ToggleCCI, a simple online algorithm that dynamically switches between VPN and CCI based on recent cost observations while accounting for leasing constraints and delays. Using both synthetic workloads and real-world traffic traces, we demonstrate that ToggleCCI consistently tracks the best static strategy and achieves substantial cost savings across a wide range of scenarios.
M.Sc. student under the supervision of Prof. Isaac Keslassy.
Title: Efficient LLM Systems: From Algorithm Design to Deployment
Abstract:
Large Language Models (LLMs) have transformed what machines can do and how systems are designed to serve them. These models are both computationally and memory demanding, revealing the limits of traditional optimization methods that once sufficed for conventional systems. A central challenge in building LLM systems is improving system metrics while ensuring response quality.
This talk presents approaches for reducing latency in LLM systems to support interactive applications, from scheduling algorithm design to deployment. It introduces scheduling frameworks that use lightweight predictions of request behavior to make informed decisions about prioritization and memory management across two core settings: standalone LLM inference and API-augmented LLMs that interact with external tools. Across both settings, prediction-guided scheduling delivers substantial latency reductions while remaining practical for deployment.
Bio:
Rana Shahout is a Postdoctoral Fellow at Harvard University, working with Michael Mitzenmacher and Minlan Yu. She received her Ph.D. in Computer Science from the Technion and previously worked as a Senior Software Engineer at Mellanox (now NVIDIA). Her research combines machine learning, systems, and algorithmic theory to design efficient and scalable AI systems. Rana is a recipient of the Eric and Wendy Schmidt Postdoctoral Award, the Zuckerman Postdoctoral Fellowship, the Weizmann Institute Women’s Postdoctoral Career Development Award, the VATAT Postdoctoral Fellowship, and first place in the ACC Feder Family Award for Best Student Work in Communications.
Columbia University12/1, 12:30
Location: TBDTitle: cache_ext: Customizing the Page Cache with eBPFAbstract:
The OS page cache is central to the performance of many applications, by reducing excessive accesses to storage. However, its one-size-fits-all eviction policy performs poorly in many workloads. While the systems community has experimented with new and adaptive eviction policies in non-OS settings (e.g., key-value stores, CDNs), it is very difficult to implement such policies in the kernel. To address these shortcomings, we design a flexible eBPF-based framework for the Linux page cache, called cache_ext, that allows developers to customize the page cache without modifying the kernel. cache_ext enables applications to customize the page cache policy for their specific needs, while also ensuring that different applications’ policies do not interfere with each other and preserving the page cache’s ability to share memory across different processes. We demonstrate the flexibility of cache_ext’s interface by using it to implement eight different policies, including sophisticated eviction algorithms. Our evaluation shows that it is indeed beneficial for applications to customize the page cache to match their workloads’ unique properties, and that they can achieve up to 70% higher throughput and 58% lower tail latency.Bio: Tal Zussman is a PhD student in Computer Science at Columbia University, advised by Prof. Asaf Cidon. He works on operating systems and eBPF, with a focus on accelerating, customizing, and modernizing memory management and storage systems. He received his MS and BS degrees at Columbia, and is an NSF Graduate Research Fellow.