Research and Projects

Automated Formal Analysis of Internet Routing Configurations
Verifying Formal Models and Synthesizing Faithful Implementations
Other Work

Research Statement

My research centers around the application of formal methods and programming languages techniques that enable us to create network systems that are functionally correct, scalable, and easy to manage.

I am the lead student for Formally Verifiable Routing (FVR) project, and reduction-based analysis of Internet routing systems project. I also contribute to Route Shepherd.

I am a member of NetDB@Penn, and I contribute to ExCAPE.

To create scalable, more securer, reliable and manageable networks, the past twenty years have witnessed, among many other efforts, advances in formal network modeling, system verification and testing, and point solutions for network management by formal reasoning. On the conceptual side, the formal models usually abstract away low-level details, specifying what are the correct functionality but not how to achieve them. On the practical side, system verification of existing networked systems is generally hard, and system testing or simulation provide limited formal guarantee. The middle approach — point solutions by formal reasoning, however, require deep understanding and insights, and rely on reasoning process that is often manual, tedious, and error prone. What's worse, even after the point solutions are verified, the correctness property is not automatically entailed in the actual implementation. This is known as a long standing challenge in network practice — the formal reasoning process is decoupled from the actual implementation.

My research seeks to bridge formal reasoning and actual network implementation by the application of formal methods and programming languages techniques in networking domain. The key enabling compo- nents and techniques are as follows.

Vrifying formal network models: To free the network operators from the manual reasoning process, I automate analysis on network models, by using existing formal tools.
Generating faithful implementations: From verified models. To enforce the verified correctness properties in the actual implementations, I compile the verified model into property-preserving distributed implementations, by leveraging recent advances in network programming framework.
Verifying actual network systems: To go beyond network models, I design and implement general automated tools for analyzing real-world network systems, by combining formal methods and network domain knowledge.
Scalability techniques for analysis: To scale up formal analysis, I propose novel scalability techniques, by exploring the networking problem space. I also establish correctness properties and demonstrate its effectiveness by evaluation on real-world networks.

Publications

Automated Formal Analysis of Internet Routing Configurations

Reduction-based Formal Analysis of BGP Instances PDF Technical report: Anduo Wang, Carolyn Talcott, Alexander J.T. Gurney, Boon Thau Loo and Andre Scedrov, IFIP 18th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS), 2012
Reduction-based analysis of BGP systems with BGPVerif PDF: Anduo Wang, Alexander J.T. Gurney, Xianglong Han, Jinyan Cao, Carolyn Talcot, Boon Thau Loo, Andre Scedrov, ACM Special Interest Group on Data Communication (ACM SIGCOMM) demonstration, Finland, 2012
Brief announcement: A calculus of policy-based routing systems PDF: Anduo Wang, Carolyn Talcott, Alexander Gurney, Boon Thau Loo, Andre Scedrov, ACM Symposium on Principles of distributed computing (PODC), 2012
Analyzing BGP Instances in Maude PDF: Anduo Wang, Carolyn Talcott, Limin Jia, Boon Thau Loo, Andre Scedrov, IFIP International Conference on Formal Techniques for Distributed Systems joint international conference 13th Formal Methods for Open Object-Based Distributed Systems 31nd Formal Techniques for Networked and Distributed Systems (FMOODS & FORTE), 2011
Partial Specifications of Routing Configurations Route Shepherd Website: Alexander J. T. Gurney, Limin Jia, Anduo Wang, and Boon Thau Loo, 1st International Workshop on Rigorous Protocol Engineering (WRiPE), co-located with IEEE International Conference on Network Protocols \textbf{(ICNP)} , Vancouver, Canada, 2011
Formalizing Metarouting in PVS: Anduo Wang, Boon Thau Loo, Automated Formal Methods workshop (AFM), co-located with 21st International Conference on Computer Aided Verification (CAV), France, 2009

Verifying Formal Models and Synthesizing Faithful Implementations

FSR: Formal Analysis and Implementation Toolkit for Safe Inter-domain Routing PDF FSR Website: Anduo Wang, Limin Jia, Wenchao Zhou, Yiqing Ren, Boon Thau Loo, Jennifer Rexford, Vivek Nigam, Andre Scedrov, Carolyn L. Talcott, IEEE/ACM Transactions on Networking (ToN), 2012
Recent advances in declarative networking RapidNet Website: Boon Thau Loo, Harjot Gill, Changbin Liu, Yun Mao, William R. Marczak, Micah Sherr, Anduo Wang, Wenchao Zhou, 14th International Conference on Practical Aspects of Declarative Languages, (PADL), 2012
FSR: Formal Analysis and Implementation Toolkit for Safe Inter-domain Routing: Yiqing Ren, Wenchao Zhou, Anduo Wang, Limin Jia, Alexander J.T. Gurney, Boon Thau Loo, and Jennifer Rexford, ACM Special Interest Group on Data Communication (ACM SIGCOMM demonstration), Toronto, Canada, 2011
An Operational Semantics for Network Datalog: Vivek Nigam, Limin Jia, Anduo Wang, Boon Thau Loo, and Andre Scedrov, Third International Workshop on Logics, Agents, and Mobility (LAM), in conjunction with 25th Annual IEEE Symposium on Logic In Computer Science (LICS), 2010
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, 2009
A Theorem Proving Approach Towards Declarative Networking: Anduo Wang, Boon Thau Loo, Changbin Liu, Oleg Sokolsky, Prithwish Basu, Theorem Proving in Higher Order Logics (TPHOLs), 22nd International Conference Emerging Trends Section, August, 2009
Declarative Network Verification PDF: Anduo Wang, Prithwish Basu, Boon Thau Loo, Oleg Sokolsky, International Symposium on Practical Aspects of Declarative Languages (PADL), 2009

Other Work

Formalizing a Component Model in PVS: Kung-Kiu Lau, Anduo Wang, preprint 40, Technical Report, School of Computer Science, The University of Manchester, 2006
A Component Based Approach to Verified Software: What, Why, How And What Next?: Kung-Kiu Lau, Zheng Wang, Anduo Wang, Ming Gu, 1st Asian Working Conference on Verified Software, 2006
Verifying Java Programs By Theorem Prover HOL: Anduo Wang, Fei He, Ming Gu, Xiaoyu Song, Proceedings of the 30th Annual International Computer Software and Applications Conference, 2006

Presentations and Demonstrations

DIMACS Workshop on Software Defined Networking Formal Synthesis in Software-Defined Networks: Rutgers University, 12/2012
PX-exchange meeting, invited talk: Reduction-based Formal Analysis of BGP Instances, Baltimore, 10/2012
SIGCOMM demo: BGPVerif: A Reduction-based Formal Analysis Toolkit for analyzing BGP Instances, Finland, 08/2012
SRI, Menlo Park: A calculus for policy-based routing systems, 07/2012.
PODC brief announcement: A calculus for policy-based routing systems Portugal, 05/2012
TACAS: Analyzing BGP Instances in Maude TACAS, Estonia, 04/2012
PX-exchange meeting, invited talk: Analyzing BGP Instances in Maude, Baltimore, 10/2011
SIGCOMM demo: FSR: Formal Analysis and Implementation Toolkit for Safe Inter-domain Routing, Canada, 08/2011
SRI, Menlo Park: Analyzing BGP Systems with Maude, 08/2010
PX-exchange meeting, invited talk: Formally Verifiable Networking, Baltimore, 10/2010
TPHOLs short talk: A Theorem Proving Approach Towards Declarative Networking, TPHOLs Emerging Trends Sec- tion, Germany, 08/2009
AFM: Formalizing Metarouting in PVS, Automated formal methods workshop, France, 06/2009
PADL: Declarative Network Verification, International Symposium on Practical Aspects of Declarative Languages, Charlotte, NC, 2009