{"id":167009,"date":"2014-07-26T00:00:00","date_gmt":"2014-07-26T00:00:00","guid":{"rendered":"https:\/\/www.microsoft.com\/en-us\/research\/msr-research-item\/automated-analysis-and-debugging-of-network-connectivity-policies\/"},"modified":"2019-05-13T03:44:22","modified_gmt":"2019-05-13T10:44:22","slug":"automated-analysis-and-debugging-of-network-connectivity-policies","status":"publish","type":"msr-research-item","link":"https:\/\/www.microsoft.com\/en-us\/research\/publication\/automated-analysis-and-debugging-of-network-connectivity-policies\/","title":{"rendered":"Automated Analysis and Debugging of Network Connectivity Policies"},"content":{"rendered":"<div class=\"asset-content\">\n<p>Network connectivity policies are crucial for assuring the security and availability of large-scale datacenter. Managing these policies is fraught with complexity and operator errors. The difficulties are exacerbated when deploying large scale offerings of public cloud services where multiple tenants are hosted within customized isolation boundaries. In these large-scale settings it is impractical to depend on human effort or trial and error to maintain the correctness and consistency of policies.<\/p>\n<p>We describe an approach for automatically validating network connectivity policies and its implementation in a tool called SecGuru. SecGuru can check selected properties of policies, e.g., is some traffic permitted or denied, and it can compare two policies yielding a <em>semantic diff<\/em> to summarize drifts. We use bit-vector logic to encode policies and semantic diffs; and the theorem prover Z3 as the underlying solver. A key contribution is a new algorithm for compactly enumerating symbolic diffs. We finally describe the experience of using SecGuru in Azure, a public cloud provider. Azure uses SecGuru for continuously monitoring policy configurations and alerting on errors, and also as a regression test suite to check policies before deployment. As a result of using SecGuru, today Azure proactively detects and avoids policy misconfigurations that lead to security and availability issues.<\/p>\n<\/div>\n<p><!-- .asset-content --><\/p>\n","protected":false},"excerpt":{"rendered":"<p>Network connectivity policies are crucial for assuring the security and availability of large-scale datacenter. Managing these policies is fraught with complexity and operator errors. The difficulties are exacerbated when deploying large scale offerings of public cloud services where multiple tenants are hosted within customized isolation boundaries. In these large-scale settings it is impractical to depend [&hellip;]<\/p>\n","protected":false},"featured_media":0,"template":"","meta":{"msr-url-field":"","msr-podcast-episode":"","msrModifiedDate":"","msrModifiedDateEnabled":false,"ep_exclude_from_search":false,"_classifai_error":"","footnotes":""},"msr-content-type":[3],"msr-research-highlight":[],"research-area":[13561,13560,13547],"msr-publication-type":[193718],"msr-product-type":[],"msr-focus-area":[],"msr-platform":[],"msr-download-source":[],"msr-locale":[268875],"msr-post-option":[],"msr-field-of-study":[],"msr-conference":[],"msr-journal":[],"msr-impact-theme":[],"msr-pillar":[],"class_list":["post-167009","msr-research-item","type-msr-research-item","status-publish","hentry","msr-research-area-algorithms","msr-research-area-programming-languages-software-engineering","msr-research-area-systems-and-networking","msr-locale-en_us"],"msr_publishername":"","msr_edition":"","msr_affiliation":"","msr_published_date":"2014-7-26","msr_host":"","msr_duration":"","msr_version":"","msr_speaker":"","msr_other_contributors":"","msr_booktitle":"","msr_pages_string":"","msr_chapter":"","msr_isbn":"","msr_journal":"","msr_volume":"","msr_number":"MSR-TR-2014-102","msr_editors":"","msr_series":"","msr_issue":"","msr_organization":"Microsoft","msr_how_published":"","msr_notes":"","msr_highlight_text":"","msr_release_tracker_id":"","msr_original_fields_of_study":"","msr_download_urls":"","msr_external_url":"","msr_secondary_video_url":"","msr_longbiography":"","msr_microsoftintellectualproperty":1,"msr_main_download":"204773","msr_publicationurl":"","msr_doi":"","msr_publication_uploader":[{"type":"file","viewUrl":"https:\/\/www.microsoft.com\/en-us\/research\/wp-content\/uploads\/2016\/02\/secguru.pdf","id":"204773","title":"secguru.pdf","label_id":"243109","label":0}],"msr_related_uploader":"","msr_attachments":[{"id":204773,"url":"https:\/\/www.microsoft.com\/en-us\/research\/wp-content\/uploads\/2016\/02\/secguru.pdf"}],"msr-author-ordering":[{"type":"text","value":"Karthick Jayaraman","user_id":0,"rest_url":false},{"type":"user_nicename","value":"Nikolaj Bjorner","user_id":33067,"rest_url":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/microsoft-research\/v1\/researchers?person=Nikolaj Bjorner"},{"type":"text","value":"Geoff Outhred","user_id":0,"rest_url":false},{"type":"text","value":"Charlie Kaufman","user_id":0,"rest_url":false}],"msr_impact_theme":[],"msr_research_lab":[],"msr_event":[],"msr_group":[],"msr_project":[171010],"publication":[],"video":[],"download":[],"msr_publication_type":"techreport","related_content":{"projects":[{"ID":171010,"post_title":"Network Verification","post_name":"network-verification","post_type":"msr-project","post_date":"2012-08-01 09:54:13","post_modified":"2024-10-24 09:09:12","post_status":"publish","permalink":"https:\/\/www.microsoft.com\/en-us\/research\/project\/network-verification\/","post_excerpt":"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 on their large networks. Specifically, the project explores three sub-areas: Data-plane verification Because networks forward packets according to their data&hellip;","_links":{"self":[{"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-project\/171010"}]}}]},"_links":{"self":[{"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-research-item\/167009"}],"collection":[{"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-research-item"}],"about":[{"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/types\/msr-research-item"}],"version-history":[{"count":2,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-research-item\/167009\/revisions"}],"predecessor-version":[{"id":534855,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-research-item\/167009\/revisions\/534855"}],"wp:attachment":[{"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/media?parent=167009"}],"wp:term":[{"taxonomy":"msr-content-type","embeddable":true,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-content-type?post=167009"},{"taxonomy":"msr-research-highlight","embeddable":true,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-research-highlight?post=167009"},{"taxonomy":"msr-research-area","embeddable":true,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/research-area?post=167009"},{"taxonomy":"msr-publication-type","embeddable":true,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-publication-type?post=167009"},{"taxonomy":"msr-product-type","embeddable":true,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-product-type?post=167009"},{"taxonomy":"msr-focus-area","embeddable":true,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-focus-area?post=167009"},{"taxonomy":"msr-platform","embeddable":true,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-platform?post=167009"},{"taxonomy":"msr-download-source","embeddable":true,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-download-source?post=167009"},{"taxonomy":"msr-locale","embeddable":true,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-locale?post=167009"},{"taxonomy":"msr-post-option","embeddable":true,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-post-option?post=167009"},{"taxonomy":"msr-field-of-study","embeddable":true,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-field-of-study?post=167009"},{"taxonomy":"msr-conference","embeddable":true,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-conference?post=167009"},{"taxonomy":"msr-journal","embeddable":true,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-journal?post=167009"},{"taxonomy":"msr-impact-theme","embeddable":true,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-impact-theme?post=167009"},{"taxonomy":"msr-pillar","embeddable":true,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-pillar?post=167009"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}