Computer networks depend on distributed routing protocols to determine how data should be forwarded through the network. However, software implementations of routing protocol often contain errors: e.g., in a recent survey, 40% of network engineers reported that software bugs were most often the cause of network failures. Researchers have developed a variety of techniques for verifying the correctness of routing protocols before they are implemented and verifying the computed paths after the protocol has run, but few researchers have addressed the challenge of verifying the software implementations of the routing protocols
. This is due, in part, to the complexity of the protocols and the many points in the code at which a decision is made---i.e., many if-statements that result in divergent execution paths.
The goal of this project is to explore whether the specific ways in which a network uses a routing protocol can be used to restrict which parts of the software implementation must be checked, and hence make it practical to apply formal software verification techniques to uncover bugs before a protocol implementation is deployed. Toward this end, students will:
- Study bug reports from commercially-adopted, open-source routing protocol implementations to determine what type of bugs commonly occur
- Analyze what code segments (from a protocol implementation) are executed under various network configurations, in order to determine how much code needs to be verified
- Apply existing software verification techniques to the identified code segments to measure how quickly bugs can be detected
As part of these tasks, students will learn how distributed routing protocols work, read research papers on network and software verification, write code to analyze bug-report and code-coverage data, and learn how to apply existing software verification tools.