Formally Verifiable Networking

This paper proposes Formally Verifiable Networking (FVN), a novel approach towards unifying the design, specification, implementation, and verification of networking protocols within a logic-based framework. In FVN, formal logical statements are used to specify the behavior and the properties of the protocol. FVN uses declarative networking as an intermediary layer between high-level logical specifications of the network model and low-level implementations. A theorem prover is used to statically verify the properties of declarative network protocols. Moreover, a property preserving translation exists for generating declarative networking implementations from verified formal specifications. We further demonstrate the possibility of designing and specifying well-behaved network protocols with correctness guarantees in FVN using meta-models in a systematic and compositional way.