Cristina Nita-Rotaru
Northeastern University

Bio: 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),
Director of the Undergraduate Cybersecurity Program (2024 – 2025), 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, three IETF/IRTF Applied Networking Research Prize in 2018, 2016 and 2024, 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 2023, 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 PC co-chair of IEEE S&P 2025 and S&P 2026.

Abstract: Communication protocols are the backbone of our connected world, enabling data exchange across smart homes and cities, financial systems, educational platforms, manufacturing, and entertainment. Given their central role, these protocols must be resilient—not just to everyday faults and misconfigurations, but also to deliberate attacks. So, how can we ensure this level of resilience?

In practice, protocol specifications are often incomplete or expressed informally, with natural language descriptions and implementation code becoming the de facto source of truth. While extensive testing—including adversarial testing—is standard before deployment, it alone cannot guarantee robust behavior. What’s needed is a rigorous, formal definition of protocol objectives and a clear articulation of the assumptions under which protocols are expected to operate correctly. Formal methods provide the tools to clarify specifications, make hidden assumptions explicit, and reveal flaws that testing might overlook.Yet despite their promise, formal methods remain underutilized in the design, implementation, and validation of network protocols.

In this talk, I’ll share work done in collaboration with my students and collaborators to explore the different roles specifications play in both the networking and formal methods communities. I’ll illustrate the value of formal specification through case studies in two domains. The first involves traditional Internet protocols like TCP, DCCP, and SCTP, which manage communication between two peers. The second focuses on decentralized finance (DeFi) protocols like GossipSub—used by Ethereum—and the Lightning Network, Bitcoin’s largest payment channel network, both of which coordinate communication among multiple peers. In each case, we developed precise, rigorous specifications that explicitly captured underlying assumptions and clearly stated protocol objectives. Using tools such as the ACL2 theorem prover and the SPIN model checker, we analyzed these protocols, assessed whether their goals were met, and uncovered several unexpected and undesirable behaviors. I’ll conclude with the lessons we’ve gained from this work.