\n\u201cIf you view a whole network as a program, can you use program analysis to tweak these networks?\u201d \u2013 George Varghese<\/strong><\/p>\n<\/blockquote>\nConfluences<\/h3>\n
Meanwhile, George Varghese had recently joined the Networking Research group at Microsoft when he reached out to peers from software engineering. Varghese, along with collaborators from Stanford University, had developed a method for verifying flow properties in networks by using header space data structures that could efficiently simulate networks on a massive number of flows. It was an exciting development that would form the basis of the Palo Alto-based Forward Networks intent-based networking startup and represented a clear example of what could be achieved by exploiting confluences between techniques from design automation and software-defined networking. Varghese created awareness of this insight with peers in the networking and verification communities; this led to several collaborations, including a close partnership with Bj\u00f8rner. Also drawn to the potential of the research was Nuno Lopes, an intern at the time and now a researcher at Microsoft Research Cambridge in the U.K. Lopes\u2019 internship project had created a general-purpose engine that could perform efficient header space operations inspired by Varghese\u2019s earlier work. The engine involved Cambridge-based researcher Andrey Rybalchenko and professor Gordon Plotkin of The University of Edinburgh, well-known for seminal work on programming language semantics. Plotkin instigated exploiting symmetries for scaling network verification.<\/p>\n
George Varghese, Chancellor\u2019s Professor of Computer Science at UCLA, formerly Principal Researcher at Microsoft Research<\/p><\/div>\n
Symmetries are a basis for process calculi used to model concurrency, and they are inherent in cloud networks built with a redundant set of routers. The networking research community continues to embrace network verification with a welcoming culture, whether for data-plane validation, control plane verification, verifying programs that perform packet processing\u2014noteworthy in the P4 programming language\u2014or verifying networking stacks. Several startups in the network verification space have emerged, including Veriflow and Intentionet, addressing needs of enterprises for administrating their global networks, and other major cloud providers are now also embracing network verification.<\/p>\n
\u201cThe joy is, first of all, it\u2019s useful; it helps Azure avoid bugs and keep going. But it\u2019s also intellectually stimulating because it\u2019s not simply using verification tools that already exist, but it\u2019s inventing new ones specialized for networking. And Nikolaj and Nuno and Andrey and Gordon and I have all enjoyed that a lot. We contributed not just to engineering but to science,\u201d said Varghese.<\/p>\n
\u201cGeorge has inspired and mentored me in so many respects. He made the point that throughout history, when somewhat unrelated areas of fields are brought together, a new starting point is created,\u201d said Bj\u00f8rner.<\/p>\n
Varghese used the concept of abstract art as an analogy, pointing out how the development of photography influenced the painters of the day in that they began to find the accurate capturing of nature less appealing, giving rise to the new genre. Such stories also exist in technology, said Bj\u00f8rner, and the arrival of a new technology will see two parties benefiting from such confluences. \u201cThe networking world benefits from verification methodologies to understand what it means to build these reliable networks with guarantees. The verification community in turn is learning tricks of the trade and domain-specific trades that will teach us what it means to build efficient tools or create efficient algorithms for these networks.\u201d<\/p>\n
Onward<\/h3>\n
Meanwhile, SecGuru had been extended to verifying network configurations beyond ACLs, checking reachability properties in Azure datacenters. SecGuru scales these checks to 100Ks routers, involving trillions of network paths. The checks are done on demand and in a matter of minutes for all Azure routers. It owes the efficiency to a domain insight Jayaraman developed when reviewing the datacenter architecture of Azure. The architecture uses a highly regular structure in which each router has a fixed role for a configurable set of address ranges. It suffices verifying that the roles are enforced on each router and global reachability properties follow as consequences of overall network properties. The issues that the verifier unearths include configuration bugs, software bugs, faulty hardware, and errors introduced during troubleshooting incidents. The sources for intent drift are varied and beyond the control of any single tool, but network verification can catch such drift regardless of its root cause.<\/p>\n
\n\u201cAssuring all changes and that the reality of the network always preserves our intent is critical for reliability. Reliability is critical for earning customer trust.\u201d \u2013 Karthick Jayaraman<\/strong><\/p>\n<\/blockquote>\nAzure cloud services exist in an ecosystem of constant change. Daunting amounts of new capacity are constantly deployed along with constantly emerging new technologies and infrastructure. It is an exciting time for networking research and synergies with formal methods. New uses for formal methods applied to network and configuration verification emerge. As a fresh hire, Jayaraman forged collaborations with researchers from different backgrounds and helped fuel cloud-wide innovation. It\u2019s a testament to a culture at Microsoft that fosters collaboration and encourages creativity. Stay tuned.<\/p>\n","protected":false},"excerpt":{"rendered":"
What does it take to build one of the most reliable hyperscale clouds on the planet? It clearly requires astronomical investments and a vast organization that operates at global scale in near seamless coordination. Yet the breakthroughs that fuel this story emerged organically, from a combination of innovation and mentoring relationships that grew into close […]<\/p>\n","protected":false},"author":37074,"featured_media":551190,"comment_status":"closed","ping_status":"closed","sticky":false,"template":"","format":"standard","meta":{"msr-url-field":"","msr-podcast-episode":"","msrModifiedDate":"","msrModifiedDateEnabled":false,"ep_exclude_from_search":false,"footnotes":""},"categories":[194463],"tags":[],"research-area":[13547],"msr-region":[],"msr-event-type":[],"msr-locale":[268875],"msr-post-option":[],"msr-impact-theme":[],"msr-promo-type":[],"msr-podcast-series":[],"class_list":["post-551046","post","type-post","status-publish","format-standard","has-post-thumbnail","hentry","category-systems","msr-research-area-systems-and-networking","msr-locale-en_us"],"msr_event_details":{"start":"","end":"","location":""},"podcast_url":"","podcast_episode":"","msr_research_lab":[],"msr_impact_theme":[],"related-publications":[],"related-downloads":[],"related-videos":[],"related-academic-programs":[],"related-groups":[],"related-projects":[171010],"related-events":[],"related-researchers":[],"msr_type":"Post","featured_image_thumbnail":"","byline":"","formattedDate":"November 20, 2018","formattedExcerpt":"What does it take to build one of the most reliable hyperscale clouds on the planet? It clearly requires astronomical investments and a vast organization that operates at global scale in near seamless coordination. Yet the breakthroughs that fuel this story emerged organically, from a…","locale":{"slug":"en_us","name":"English","native":"","english":"English"},"_links":{"self":[{"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/posts\/551046"}],"collection":[{"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/posts"}],"about":[{"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/types\/post"}],"author":[{"embeddable":true,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/users\/37074"}],"replies":[{"embeddable":true,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/comments?post=551046"}],"version-history":[{"count":16,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/posts\/551046\/revisions"}],"predecessor-version":[{"id":551967,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/posts\/551046\/revisions\/551967"}],"wp:featuredmedia":[{"embeddable":true,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/media\/551190"}],"wp:attachment":[{"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/media?parent=551046"}],"wp:term":[{"taxonomy":"category","embeddable":true,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/categories?post=551046"},{"taxonomy":"post_tag","embeddable":true,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/tags?post=551046"},{"taxonomy":"msr-research-area","embeddable":true,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/research-area?post=551046"},{"taxonomy":"msr-region","embeddable":true,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-region?post=551046"},{"taxonomy":"msr-event-type","embeddable":true,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-event-type?post=551046"},{"taxonomy":"msr-locale","embeddable":true,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-locale?post=551046"},{"taxonomy":"msr-post-option","embeddable":true,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-post-option?post=551046"},{"taxonomy":"msr-impact-theme","embeddable":true,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-impact-theme?post=551046"},{"taxonomy":"msr-promo-type","embeddable":true,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-promo-type?post=551046"},{"taxonomy":"msr-podcast-series","embeddable":true,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-podcast-series?post=551046"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}