In this project, we are formulating a formal science of securing packet forwarding in computer networks. In particular, we are developing a formal algebra of the network's data plane (packet-forwarding) operations. Our approach represents the network's forwarding behavior and state in the form of Boolean satisfiability (SAT) clauses. Our framework enables rigorous analysis and study of the way that networks forward packets, including the ability to check correctness invariants against a specific network deployment (e.g., reachability, service quality, classification level), providing metrics that capture the degree of packet-forwarding security, and enabling the derivation of theorems about how to build networks with strong security properties on packet-forwarding behavior. We are bridging the gap between theory and practice by developing a system to directly read SAT clauses from network deployments and are building upon existing SAT solver technologies to perform automated reasoning. To speed progress, we are building upon our earlier work on using satisfiability checking for testing network reachability.
Brighten Godfrey and Matthew Caesar
Towards a Science of Securing Network Forwarding