Formally Verifiable Networking

Today's Internet is increasingly complex and fragile. The networking community is more open to verification techniques than ever. In the passing years, runtime verification and model checking gradually comes in to the development of complicated and next-generation network protocols. We argue that time is ripe for the use of formal verification technique in aiding networking development.

To remedy the numerous difficulty in developing and analyzing network protocols, we propose Formally Verifiable Networking (pronounced FUN ), a unified framework the design, specification, implementation and verification of network protocols.

Declarative Network Verification

blabla

System Code Generation

blabla

Meta-models and linear logic

blabla

Project Members

• Anduo Wang, University of Pennsylvania
• Limin Jia, University of Pennsylvania
• Changbin Liu, University of Pennsylvania
• Boon Thau Loo, University of Pennsylvania
• Prithwish Basu, BBN Technologies
• Oleg Sokolsky, University of Pennsylvania

Publications

1. tech-report...
2. tphol09...
3. Formalizing Metarouting in PVS Anduo Wang, Boon Thau Loo., Automated Formal methods (AFM 2009), co-located with CAV09, July, 2009. [Paper] [Talk]
4. 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] [Outdated Declarative Network Verification]

Acknowledgments