Talk: Detecting Protocol Implementation Bugs at Runtime
Bio: Aurojit Panda, Assistant Professor, Computer Science, New York University
Event Details
Abstract: Despite significant progress in verifying protocols, services that implement distributed protocols , e.g., Chubby or Etcd, can exhibit safety bugs in production deployments. These bugs are often introduced by programmers when converting protocol descriptions into code. In this talk I will describe a new technique we have been developing to identify these bugs at runtime: Runtime Protocol Refinement Checking} (RPRC). RPRC systems observe a deployed service’s runtime behavior and notify operators when this behavior evidences a protocol implementation bug, allowing operators to mitigate the bugs impact and developers to fix the bug. We have developed an algorithm for RPRC and implemented it in a system called Ellsberg that targets services that assume the asynchronous or partially synchronous model, and fail-stop failures. We designed Ellsberg so it makes no assumptions about how services are implemented, and requires no additional coordination or communication. We have used Ellsberg with three open source services: Etcd, Zookeeper and Redis Raft.
Bio: Aurojit Panda is an assistant professor in the Computer Science department at New York University. He works in systems and networking, though he borrows problems and techniques from several fields, including formal methods, programming languages, graphics and machine learning. He received his PhD in 2017 from UC Berkeley, where he was advised by Scott Shenker. He has received several awards, including a VMware Early Career Faculty Award, a Google Research Scholar Award, an NSF Career award, best paper awards at EuroSys, SIGCOMM and OSDI, and a EuroSys test of time award.