Verification and Attack Synthesis for Network Protocols

TL;DR

This paper demonstrates how formal methods can be used to verify network protocols and synthesize attacks, ensuring their correctness and security under various conditions.

Contribution

It introduces a framework for formal verification and attack synthesis for network protocols, addressing both correctness and security concerns.

Findings

Formal methods effectively characterize protocol behavior.

Verification identifies potential protocol bugs.

Attack synthesis reveals vulnerabilities.

Abstract

Network protocols are programs with inputs and outputs that follow predefined communication patterns to synchronize and exchange information. There are many protocols and each serves a different purpose, e.g., routing, transport, secure communication, etc. The functional and performance requirements for a protocol can be expressed using a formal specification, such as, a set of logical predicates over its traces. A protocol could be prevented from achieving its requirements due to a bug in its design or implementation, a component failure (e.g., a crash), or an attack. This dissertation shows that formal methods can feasibly characterize the functionality and performance of network protocols under normal conditions as well as when subjected to attacks.