Mooly Sagiv
Verifying Safety of Distributed Systems
April 15, 2016 at 3:30pm
CSE 305
Abstract
Distributed systems play an essential role in modern life. However, they are notoriously hard to develop. Bugs may occur on rarely executed scenarios and therefore testing distributed systems is hard. I will describe two ongoing efforts to verify the safety of distributed systems. Our approach is motivated by the need to verify small and intricate distributed protocols like Paxos and large symmetric stateful networks of Middleboxes.
In the first part of the, I will describe IVY: an interactive static analysis tool for proving safety of infinite-state (distributed) systems with an unbounded number of nodes. IVY combines automation using SAT solvers and user interaction. We provide initial data which shows that IVY can drastically simplify the task of verifying systems and identifying potential design bugs.
The key insight in IVY is a careful design of a modeling language RML which permits effective verification. This is combined with user-directed counterexample guided refinement.
In the second part of the talk I will address the problem of verifying the safety of stateful networks which include Middleboxes such as Firewall and Cache Proxy. I will show that abstract effect of middleboxes can also be modeled by RML and describe theoretical and practical results about the complexity of stateful network verification.
Bio
Mooly Sagiv is a professor in the School of Computer Sciences at Tel-Aviv University. He is a leading researcher in the area of large scale (inter-procedural) program analysis, and one of the key contributors to shape analysis. His fields of interests include programming languages, compilers, abstract interpretation, profiling, pointer analysis, shape analysis, inter-procedural dataflow analysis, program slicing, and language-based programming environments. Sagiv is a recipient of a 2013 senior ERC research grant for Verifying and Synthesizing Software Composition. Prof. Sagiv served as Member of the Advisory Board of Panaya Inc. He received best-paper awards at PLDI’11 and PLDI’12 for his work on composing concurrent data structures and a ACM SIGSOFT Retrospective Impact Paper Award (2011) for program slicing. He is an ACM fellow.