Wang, AnduoJia, LiminLiu, ChangbinLoo, Boon ThauSokolsky, OlegBasu, Prithwish2023-05-222023-05-222009-10-012013-01-11https://repository.upenn.edu/handle/20.500.14332/6816This 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.CPS Formal MethodsPresentation