{"id":171010,"date":"2012-08-01T09:54:13","date_gmt":"2012-08-01T09:54:13","guid":{"rendered":"https:\/\/www.microsoft.com\/en-us\/research\/project\/network-verification\/"},"modified":"2025-04-08T21:50:40","modified_gmt":"2025-04-09T04:50:40","slug":"network-verification","status":"publish","type":"msr-project","link":"https:\/\/www.microsoft.com\/en-us\/research\/project\/network-verification\/","title":{"rendered":"Network Verification"},"content":{"rendered":"<p>Networks need to run reliably, efficiently, and without users noticing any problems, even as they grow. Keeping networks tuned this way requires the development of tools that improve the functioning of large-scale datacenter networks.<\/p>\n<p>This project investigates a range of network verification tools that help network operators and architects design, operate, maintain, troubleshoot, and report on their large networks.<\/p>\n<p>Specifically, the project explores three sub-areas:<\/p>\n<p><strong>Data-plane verification<br \/>\n<\/strong>Because networks forward packets according to their data plane, verification tools need to have data-plane intelligence built in, for pre- and post-deployment verification and bug detection.<\/p>\n<p><strong>Control-plane verification<br \/>\n<\/strong>Networks generate routing tables through protocols such as BGP (border gateway protocol). To analyze networks before they go into production, they need to be verified at this, the control-plane level.<\/p>\n<p><strong>Emulation<br \/>\n<\/strong>With emulation, network designers can find bugs in firmware and models; network operators can be trained before they are working on production systems. The goal of this product is to enable highly scalable, high-fidelity network emulation for those applications.<\/p>\n<h3>Deployed tools<\/h3>\n<p>We continue to develop and deploy a range of network verification tools.<\/p>\n<ul>\n<li><a href=\"https:\/\/www.microsoft.com\/en-us\/research\/wp-content\/uploads\/2016\/02\/secguru.pdf\">SecGuru<\/a> &#8211; checks network access restrictions of Network Security Groups<\/li>\n<li><a href=\"https:\/\/www.microsoft.com\/en-us\/research\/blog\/eliminating-network-downtime\">CrystalNet<\/a> &#8211; emulates router BGP negotiation using virtual machines.<\/li>\n<li><a href=\"https:\/\/www.microsoft.com\/en-us\/research\/publication\/fast-bgp-simulation-of-large-datacenters\/\">Network Logic Solver, NLS<\/a>, &#8211; simulates, at scale, BGP negotiations.<\/li>\n<li><a href=\"https:\/\/www.microsoft.com\/en-us\/research\/publication\/validating-datacenters-at-scale\/\">RCDC<\/a> &#8211; Reachability Checker in Data Centers, verifies, at scale, dataplanes in all of Microsoft&#8217;s datacenters with > 5B z3 queries per day.<\/li>\n<li><a class=\"msr-external-link glyph-append glyph-append-open-in-new-tab glyph-append-xsmall\" rel=\"noopener noreferrer\" target=\"_blank\" href=\"https:\/\/learn.microsoft.com\/en-us\/azure\/virtual-network-manager\/concept-virtual-network-verifier\">VNetVerifier<span class=\"sr-only\"> (opens in new tab)<\/span><\/a> &#8211; reachability analysis tools for virtual network https:\/\/www.microsoft.com\/en-us\/research\/publication\/validating-datacenters-at-scale\/configurations.<\/li>\n<li>Zen &#8211; <a class=\"msr-external-link glyph-append glyph-append-open-in-new-tab glyph-append-xsmall\" rel=\"noopener noreferrer\" target=\"_blank\" href=\"https:\/\/github.com\/microsoft\/Zen\">microsoft\/Zen: Zen is a constraint solving library for .NET.<span class=\"sr-only\"> (opens in new tab)<\/span><\/a><\/li>\n<li>NCVS &#8211; a system integrating most of the above tools to validate network repave operations.<\/li>\n<\/ul>\n<h3>Emerging trends<\/h3>\n<p>There are several exciting areas we are evolving network verification. These include:<\/p>\n<ul>\n<li>Using AI to infer and codify intent from legacy configurations.<\/li>\n<li>Compositional control plane verification.<\/li>\n<\/ul>\n<p>&nbsp;<\/p>\n","protected":false},"excerpt":{"rendered":"<p>Networks need to run reliably, efficiently, and without users noticing any problems, even as they grow. Keeping networks tuned this way requires the development of tools that improve the functioning of large-scale datacenter networks. This project investigates a range of network verification tools that help network operators and architects design, operate, maintain, troubleshoot, and report [&hellip;]<\/p>\n","protected":false},"featured_media":382355,"template":"","meta":{"msr-url-field":"","msr-podcast-episode":"","msrModifiedDate":"","msrModifiedDateEnabled":false,"ep_exclude_from_search":false,"_classifai_error":"","footnotes":""},"research-area":[13560,13547],"msr-locale":[268875],"msr-impact-theme":[],"msr-pillar":[],"class_list":["post-171010","msr-project","type-msr-project","status-publish","has-post-thumbnail","hentry","msr-research-area-programming-languages-software-engineering","msr-research-area-systems-and-networking","msr-locale-en_us","msr-archive-status-complete"],"msr_project_start":"","related-publications":[168871,237717,215445,167009,166542,588349],"related-downloads":[],"related-videos":[],"related-groups":[144812],"related-events":[],"related-opportunities":[],"related-posts":[235473,551046],"related-articles":[],"tab-content":[],"slides":[],"related-researchers":[{"type":"user_nicename","display_name":"Ryan Beckett","user_id":37775,"people_section":"Group 1","alias":"rybecket"},{"type":"user_nicename","display_name":"Nikolaj Bj\u00f8rner","user_id":33067,"people_section":"Group 1","alias":"nbjorner"},{"type":"user_nicename","display_name":"Andrey Rybalchenko","user_id":33480,"people_section":"Group 1","alias":"rybal"},{"type":"user_nicename","display_name":"Siva Kesava Reddy Kakarla","user_id":42540,"people_section":"Group 1","alias":"sivakakarla"},{"type":"user_nicename","display_name":"Karthick Jayaraman","user_id":43650,"people_section":"Group 1","alias":"karjay"}],"msr_research_lab":[199561,199565],"msr_impact_theme":[],"_links":{"self":[{"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-project\/171010","targetHints":{"allow":["GET"]}}],"collection":[{"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-project"}],"about":[{"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/types\/msr-project"}],"version-history":[{"count":9,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-project\/171010\/revisions"}],"predecessor-version":[{"id":1136173,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-project\/171010\/revisions\/1136173"}],"wp:featuredmedia":[{"embeddable":true,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/media\/382355"}],"wp:attachment":[{"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/media?parent=171010"}],"wp:term":[{"taxonomy":"msr-research-area","embeddable":true,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/research-area?post=171010"},{"taxonomy":"msr-locale","embeddable":true,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-locale?post=171010"},{"taxonomy":"msr-impact-theme","embeddable":true,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-impact-theme?post=171010"},{"taxonomy":"msr-pillar","embeddable":true,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-pillar?post=171010"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}