Formally Verifiable Networking

We propose Formally Verifiable Networking, a novel approach towards unifying the design, specification, implementation, and verification of networking protocols with 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 (PVS and Coq) is used to statically verify the specified properties of declarative network protocols. Moreover, a property preserving translation exists for generating declarative networking implementations from verified formal specifications. Using metarouting as our driving example, we demonstrate the possibility of using FVN to design and specify network models in a systematic and compositional way with correctness guarantee, hence enabling additional exploration in the space of well-behaved protocols within FVN.

Students

• Anduo Wang
• Changbin Liu

Postdoc

• Vivek Nigam

Faculty

• Boon Thau Loo
• Andre Scedrov
• Oleg Sokolsky

External collaborators

• Limin Jia, Carnegie Mellon University
• Prithwish Basu, BBN Technologies

Publications

1. Formally Verifiable Networking Anduo Wang, Limin Jia, Changbin Liu, Boon Thau Loo, Oleg Sokolsky, and Prithwish Basu. 8th Workshop on Hot Topics in Networks (ACM SIGCOMM HotNets-VIII), New York, Oct 2009 (16.0% acceptance) [Paper] [Talk] [ICNP'09 poster] [Extended PX talk]
2. A Theorem Proving Approach Towards Declarative Networking Anduo Wang, Boon Thau Loo, Changbin Liu, Oleg Sokolsky, Prithwish Basu., (TPHOLs 2009) Emerging Trends Section, August, 2009 [Paper] [Talk] [Group picture]
3. Formalizing Metarouting in PVS Anduo Wang, Boon Thau Loo., Automated Formal methods (AFM 2009), co-located with CAV09, July, 2009. [Paper] [Talk] [TPHOLs'09 poster] [PVS codes]
4. Verifiable Policy-based Routing with DRIVER Anduo Wang, Changbin Liu, Boon Thau Loo, Oleg Sokolsky, Prithwash Basu., University of Pennsylvania Department of Computer and Information Science Technical Report No. MS-CIS-09-12. [Technical Report]
5. Declarative Network Verification Anduo Wang, Prithwish Basu, Boon Thau Loo, Oleg Sokolsky., Eleventh International Symposium on Practical Aspects of Declarative Languages (PADL), co-located with ACM's Principles of Programming Languages, Jan, 2009. [Paper] [Talk] [Extended Technical Report]

Acknowledgments

This work is partially supported by NSF CAREER CNS-0845552, NSF CCF-0820208, NSF CNS-0721845, and AFOSR MURI 22179000-41070B. Any opinions, findings, and conclusions or recommendations expressed in this material are those of the author(s) and do not necessarily reflect the views of the National Science Foundation.