Reasoning about the Robustness of Protocols

ABSTRACT

A typical protocol makes various assumptions about the environment in which it is deployed. For instance, to guarantee a security requirement, a protocol may rely on the attacker not having prior knowledge of secrets that the system relies on, or the end user correctly carrying out a key protocol step (e.g., browser authentication). Similarly, a distributed protocol typically relies on assumptions about the reliability of the underlying network (e.g., a message is delivered without corruption; certain network nodes are always connected). Once the protocol is deployed, however, the environment may deviate from its expected behavior over time, possibly undermining one or more of these assumptions. The attacker may gain access to a secret through a side channel; the user may inadvertently commit an erroneous action; the network may experience an unexpected fault and lose important messages. A protocol that is robust would ideally be able to preserve its most critical safety or security guarantee even under such deviations.

In this talk, I will introduce a rigorous, tool-guided framework for designing and analyzing robust protocols. Our approach will be based on a formal notion of robustness that represents the protocol's ability to tolerate possible deviations in the environment and continue to guarantee a desired property. I will then present an analysis tool that, given formal specifications of a protocol and its environmental assumptions, automatically computes robustness as a measure of the quality of the protocol design. I will also show how this type of analysis can be used to rigorously compare two alternative designs of a protocol with respect to their robustness. Finally, I will describe a technique called robustification, which takes an existing protocol and automatically synthesizes a new, improved version that is more robust against a user-specified set of deviations. I will demonstrate the applications of our approach to different case studies in protocol design, including electronic voting and network protocols.

Author

Eunsuk Kang is an Assistant Professor in the Software and Societal Systems Department, School of Computer Science at Carnegie Mellon University. His research interests include software engineering and formal methods, with applications to system safety and security. He is especially interested in leveraging formal modeling techniques, design methodologies, and automated verification to construct safe and secure software systems. He has applied his work to a diverse range of systems, including intelligent vehicles, unmanned aerial vehicles (UAVs), medical devices, water treatment plants, and mobile applications. He is a winner of the NSF CAREER Award and three ACM SIGSOFT Distinguished Paper Awards.