Program/Keynotes

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