Program/Keynotes

Keynotes

Using Formal Methods to Understand the Security Risks of Distributed Protocols Cristina Nita-Rotaru

An Hourglass Architecture for Distributed Systems Mahesh Balakrishnan


Keynote 1

Using Formal Methods to Understand the Security Risks of Distributed Protocols

Communication protocols connect our world, facilitating data transmission for smart homes and cities, financial applications, education, manufacturing, and entertainment services. Given their critical role, these protocols must be resilient to misconfigurations, faults, and attacks. But how do we ensure this resilience?

Specifications are often limited, frequently described in natural language, with the code serving as the ultimate reference for behavior. Although most protocols undergo intensive testing before deployment, including adversarial testing, this alone is not sufficient to guarantee resilience. We need rigorous specifications to define what resilience means and identify the necessary assumptions for system correctness. Formal methods can help by clarifying system specifications and making implicit assumptions explicit. They can also uncover flaws in system requirements that testing might miss.

In this talk, I will discuss work done with my students and collaborators using formal methods to rigorously specify and analyze several protocols from two domains. The first category includes Internet protocols such as TCP, DCCP, and SCTP which ensure communication between two peers. The second category involves DeFi protocols like GossipSub, a communication protocol used by Ethereum and other platforms, and the Lightning Network, the largest payment channel network for Bitcoin, both ensuring communication between multiple peers. In all cases, I will explain how we developed rigorous specifications that explicitly state assumptions and clearly define protocol goals. Using the ACL2 theorem prover and the SPIN model checker, we analyzed whether these goals were achieved and discovered several undesirable behaviors. I will conclude with lessons learned from this work.

Short Biography

Cristina Nita-Rotaru is a Professor of Computer Science in the Khoury College of Computer Sciences at Northeastern University where she leads the Network and Distributed Systems Security Laboratory (NDS2) and is a founding member of the Cybersecurity and Privacy Institute. Prior to joining Northeastern she was a faculty in the Department of Computer Science at Purdue University (2003 - 2015). She served as an Associate Dean of Faculty at Northeastern University (2017 - 2020) and as an Assistant Director for CERIAS at Purdue University (2011 - 2013). Her research lies at the intersection of cybersecurity, distributed systems, and computer networks. The overarching goal of her work is designing and building resilient distributed systems and network protocols that are resilient to faults, misconfigurations, and attacks. Her work received several best paper awards in NETYS 2023, ACM SACMAT 2022, IEEE SafeThings 2019, NDSS 2018, ISSRE 2017, DSN 2015, two IETF/IRTF Applied Networking Research Prize in 2018 and 2016, and Test-of-Time award in ACM SACMAT 2022. She is a recipient of the NSF Career Award in 2006.

Cristina Nita-Rotaru has served on the program committee of numerous conferences in networking, distributed systems and security such as ISOC NDSS, IEEE S&P, IEEE Euro S&P, IEEE/IFIP DSN, IEEE ICNP, IEEE ICDCS, IEEE INFOCOM, ACM CCS, ACM Wisec, ACM SOCC, ACM SIGCOMM, ACM CoNEXT, ACM Web, ACM Eurosys, ASPLOS, USENIX Security, USENIX OSDI, USENIX ATC. She was an Associate Editor for Elsevier Computer Communications (2008 - 2011), IEEE Transactions on Computers (2011 - 2014), ACM Transactions on Information Systems Security (2009 - 2013), Computer Networks (2012 - 2014), IEEE Transactions on Mobile Computing (2011 - 2016), and IEEE Transactions on Dependable and Secure Systems (2013 - 2017). She was a member of the steering committee of ISOC NDSS, ACM Wisec, and IEEE/IFIP DSN. She was a general chair for IEEE DSN 2022 and ISOC NDSS 2024, and a chair of the Steering Group of NDSS 2024. She was a chair of the CRA Outstanding Undergraduate Research Award Committee 2019, 2020. She is currently a member of the IFIP Working Group on Dependable Computing and Fault-tolerance and the Steering Committee of ACM SACMAT, the Vice-Chair of the IEEE Technical Community on Dependable Computing and Fault Tolerance (TCFT), and the co-chair of IEEE S&P 2025.

http://cnitarot.github.io

Cristina Nita-Rotaru, Khoury College of Computer Sciences, Northeastern University, USA


Keynote 2

An Hourglass Architecture for Distributed Systems

In this talk, I propose an hourglass architecture for distributed systems with the shared log abstraction as its narrow waist. The top of the hourglass consists of diverse applications layered above the shared log API: metadata services, transactional databases, key-value stores, publish-subscribe layers, and even blockchain apps. At the bottom of the hourglass, we have a similar diversity of ordering and durability mechanisms hidden by the shared log API, including protocols such as Paxos variants, Raft, and ZAB; streaming systems like LogDevice; or even storage systems like S3. A log-based hourglass architecture accelerates innovation by allowing applications and distributed protocols to be developed and deployed independently: for example, we can run a ZooKeeper clone. a SQL database, or a Kafka implementation on a single codebase and operational platform; which in turn can dynamically switch its ordering and durability engine between Paxos, Raft, or S3. I'll describe the origins of this paradigm at Microsoft Research (Corfu/Tango in NSDI 2012 and SOSP 2013), along with its roots in group communication; its evolution at VMware Research and Yale; its practical validation at massive scale as Meta's control plane storage (Delos in OSDI 2020 and SOSP 2021); and its current role in enabling next-generation Kafka implementations at Confluent that can provide different trade-off points between cost and performance.

Short Biography

Mahesh Balakrishnan is a distributed systems researcher and engineer at Confluent, working on next-generation streaming systems. Prior to this, he led a team at Meta that built and deployed Delos, a production database which currently provides control plane storage for all Meta services. Mahesh was a professor at Yale University from 2015 to 2019; and a researcher at VMware Research and Microsoft Research Silicon Valley before that, where he co-led the Corfu project (later commercialized by VMware as CorfuDB). He obtained his PhD from Cornell University in 2008. His work has received best paper awards at OSDI and ASPLOS. He has served as the program co-chair of NSDI, SoCC, and LADIS. https://maheshba.bitbucket.io

Mahesh Balakrishnan, Confluent, USA