緒在減少向網絡引入新功能的的同時，軟件定義網絡（SDN，SoftwareDefinedNetworking）也增加了程序錯誤（或）的風險。即使是現在的網絡軟件，由設備供過不同網絡運營商和第開發者開發的軟件提供了范圍更加廣闊的功能。SDN以及像OpenFlow[3]技術的成功，依賴于追求高可靠性的應用測試的方法。這篇中，我們會展示NICE工具，它結合了模型檢測和符號執行，是一個能夠高效發現OpenFlow程序中的工具。在我們討論自動進行OpenFlow應用測試的意見書[4]基礎上，我們在1.3OpenFlow應用中1報文穿越OpenFlowOpenFlow網絡是由分布式交換機集合組成，這些交換機是由一個運行在邏輯路連上或斷開的時候會發送“portchange”消息。OpenFlow控制器可以安裝或卸載交換機中的規則，流量數據并且對于事件作或者會發送流量數據請求。許多OpenFlow應用1都是在NOX控制器平臺[5]上編寫的，這個平臺為PythonC++應用提供了一個OpenFlow的接口。這些程序能夠進行任意的OpenFlow交換機，越來越多。[4]。此外，許多應用是通過路徑來給多個交換機安裝規則的。因為規則不是原子性地中間交換機會將報文轉發到控制器。結果，一個絕大部分時間都正確運行的OpenFlow測試OpenFlowOpenFlow應用需要捕捉交換機大狀態進行反應。OpenFlowMAC地址、IP地址、TCP/UDP端TCP標志和序列數等的字段進行任意的操作。因此OpenFlow應用需要處理大容此，測試OpenFlow應用需要檢測事件序列大空間有效的策略。但是實際上使用新語言卻很難。，大多數OpenFlow應用都是用通用語言編寫PythonJava。或者，開發者可以創建自己應用程序的抽象模型，并使用形式化中會很容易就過時。除此之外，已經有的模型檢查工具如SPIN[12]和JavaPathFinder們在第7章中會展示的一樣。相反，我們認為，測試工具應該能夠直接在未修改的OpenFlow應用上操作，并利用特定域的知識來提高可擴展性。NICE研究屬 網絡正確性屬符號模型為了解決可擴展性的問題，我們提出了NICE（NobugsInControllerExecution，控制器執行排除）工具，它是一個在許多可能事件交錯情況下，通過自動生成精心制作的報文流來測試未修改的控制程序的工具。為了使用NICE，程序員為控制程序和某NICE檢測一般的正確性屬性，屬 網絡正確性屬符號模型2給定一個OpenFlow程序、一個網絡拓撲和正確性屬性，NICE[17,18]。通過符號執行報文到達的響應方法，NICE識別了報文的等價類，即決定到達代碼唯一路徑的報文頭部字段的范圍。通過添加一個注入報文的狀態過度，NICE向網絡將這些想法聚到一起，NICE結合了模型檢測（來發掘系統執行路徑）、會在5章討NICE原型檢測了在流NOX平臺上Python編寫的未更改的應用，這些會在第6章討論到。第7章中我們的性能評估說明：(i)即使是小的例子，NICE也比應用了水平工具的方法快5倍，(ii)我們的特定OpenFlow搜索策略減少了最多20倍的狀態空間的規模，以及(iii)簡化的交換機模型為它自己帶來了減少7倍8NICEOpenFlow應用并且發現了11個。我們發現的大多數都是設計上的缺陷，它們本質上就比簡單實現上的少很多。第9章我們會討論測試覆蓋性和符號執行系統開銷之間的權衡。第10章討論了相關的工作，第11章用對未來研究方向的討論總結了這篇。 應用的模型檢考慮更大系統的狀態。系統地發掘系統狀態空間并檢測每個狀態的正確-性的需要自然OpenFlow應用上的草案，并且描述了一些讓它更加實用的改變。狀態空間建模。分布式系統具有多種組件通道進行異步的通信，即先入先出的緩沖區（例如，[19]的第二章）。每一個組件都有一個變量集，組件狀態系統狀態轉移（例如因為發送了一個消息）次系統執行響應了這些轉移的序列，因此確定了系統的一個可能的行為。模型檢測過程。給定狀態空間的模型，進行搜索在概念上是很直接的。圖5（非文OpenFlow應用的事件響應方法（3MAC學習應用的報文到達和交換機加入/離開）的集合組以，我們能按照程序的全局變量（如圖3中ctrl_state）來對它進行建模，并且將每一個37行，比如，packet_inMACmactable賦值，而且會不會安裝一個轉發規則或者模型檢測不能處理好依賴數據的應用（例子參考[19]的第1章）。因為枚舉所有可能的如第3節會討論到。OpenFlow交換OpenFlow交換機實現（如[20]）開始，定義交換機狀態為所有變量的值，并且按照的狀態（如幾百KB），還不包含存有報文的緩沖區和OpenFlow信息等待服務；這個加次性的工作，不需要給用戶增加任何負擔。根據OpenFlow規范[21]，交換機看作通信通道、處理數據報和OpenFlow信息的轉移以及一個流表的集合。靠的、有序的OpenFlow消息的交付，除了可能的交換機故障之外。我們不在TCP/IP頂部的SSL上運行OpenFlow協議，使得我們可以避免中間協議的編碼和以及網絡棧兩個簡單的轉移：交換機模型支process_pktprocess_of轉移——分別是處理數OpenFlowOpenFlow通道不是空我們就分別合并等價的流表：mrolow些規則并不交疊——成列表會導致模型檢測器將兩個不同按照不同順序排列的規則序列當成兩個不同的狀轉移的明確描述。相反的，NICEEthernet、ARP、IPTCP的許多協議提供了被前者啟用。這個模型的一個更加實際的細化是移動端主機。它有move主機轉移到新的位置<switch,port>。程序員也可以自己更改我們提供的模型，或者創建事件響應方法的符號執應方法的行為決定于它的輸入（例如，圖3中報文的MAC地址）。與其發掘所有可能的輸入，NICE識別出了哪些輸入會運行路徑通向事件響應方法的不同代碼。要系統地NICE是如何將模型檢測與符號執行結合起來從而達到有效發掘狀態空間的目的。變量的使用以及記錄了它們可能值的約束。例如，圖3中的第4行，引擎識別到37MAC80。會造成對同一個系統狀態2的重復檢查。此外，盡管檢查了所有的代碼路徑，符號執行所以，符號執行并不是一個測試OpenFlow應用的一個足夠的解決方案。取而代之的，NICE使用模型檢測來發掘系統執行路徑（并且檢測對于同一狀態的重復[23]），用OpenFlow的符號執了解決packet_in響應方法的多種的輸入，我們構建了符號報文。第二，為了最小化狀態符號報文。pkt_inICE必須識別哪些或者哪些范圍的報文頭部字段決定了到達響應方法的路徑。除了將一個報文視作符號字節的一個通用的數組，我們引入了符號報文作為我們符號的數據類型。一個符號報文是組符號型變量，一了一個頭部字。為了少約束求器（個A6字節的變量節或者低位級的。我們同時也運用了域的知識來更好地限定頭部字段可能的值具體的控制器狀態。事件響應方法的執行也依賴于控制器的狀態。例如，圖3中的代碼只會在單播的目的MAC地址在了mactable中時才到達第9行。以一個空mactable9行的輸入報文；然而以非空表NICE部分放在一起，我們現在來表述我們是如何將模型檢測（來發掘系制器上所有可行代碼路徑的報文組合。為了實現這一點，我們創建了一個叫做discover_packetspack_in4控制器狀態空間圖4中0（ii（）具體的報文（指向一個相關的報文），并ndpkt_in響應方法，我們也可以的diovr_tts響id）。個控制器狀態相關的報文，（ii）啟用了discover_packets轉移。檢測過程（12-18行）：當到達一個新狀態時，算法為每一個客戶端（15行）檢測discover_packets（26-31行）discover_stats（32-25行）轉移使得系統可以到通過對控制器事件響應方法的符號執行，NICE可以在沒有開發者的輸入下自動推第9章討論。 特定的搜索策的事件交錯上操作的，除了可以減少狀態空間的PKT-SEQ，這得益于被符號執行發現的PKT-SEQ:相關報文序列。send轉移的效如果圖4中的client1只允許一個單報文突發，啟發式方狀態2中的send(pkt2)和狀態3中的send(pkt1)。有效的是，這些限制了在狀態空間中“報文并發”的程度。為了引入這個限制，我們給每一個終端主機賦予了一個計數器c；當c=0時，終端主機不能對于每一個接收的報文將c加一。然而，這個行為也可以針對更復雜的終端主機模型進行修改，例如模仿TCP流量和擁塞控制。如，MAC學習應用只根據目的MAC地址來安裝轉發規則這就了控制器接收來自MAC法要給交換機1、2、3安裝規則，啟發式方發現反轉順序的轉移，允許交換機3首先安裝規則，然后是2最后是1。這個啟發式方發現像圖1例子中的。FLOW-IR流量獨立性減少。許多OpenFlow應用將不同的報文組獨立對待；即對于一個組的處理不會受到其它組的存在與否影響。這種情況下，NICE能夠通過發掘事PythonisSameFlow，它將兩個報文（以及交換機和輸入端口）作為mircoflow是獨立的，然而其他程序可能將不同MAC目的地址的報文獨立對待。總結。PKT-SEQsend轉移的數量而不是可能的應用正確性的明測試正確性包括對安全性（“不好的情況從不發生”和活性“最終好的情況會發生”）進行斷言，更加正式的定義可見[19]的第三章。檢測安全性相對簡單，盡管有時查流量規則合不會形一個轉發路或者洞。檢測活更加因為需要慮ICE中，我們讓輸入有限（例如，有限數量的報文，每一個都帶有一個有限的可能頭部值的集合NICE可以檢測一旦兩臺主機在每一個方向上至少交換一個報文，那么別的報文就不會發向控制器（我們稱作“嚴格直接路徑（SritDirecPths）”的屬性）。檢查這個活性屬性不僅NICE調用的回調函數來觀察系統執行中的重要的轉移，（iii）維持本地的狀態。在packet_in事件它就會標記一個。當一個正確性屬性發出信號有一個，工具就會NICEOpenFlow一樣。NoForwardingLoops沒有轉發回路：這個屬性斷言報文不會遇到轉發回路，通過檢查每一個報文最多通過給定的<switch,inputport>對多一次來實現的耗了（簡單起見，我們禁用了通信通道上可選的報文丟棄和）。為了解釋泛洪，這個屬性在報文副本和消耗間的平衡強制設為了0。DirectPaths直接路徑：這個屬性檢測一旦一個報文成功到達它的目的地址，相同流的的報文就不應該到達控制器。它可以很有效的檢測到控制器在處理OpenFlowMAC學習交換機，MACStrictDirectPaths嚴格直接路徑：這個屬性可以檢測在兩個主機成功在每個方向NoForgottenPackets沒有遺忘的報文：這個屬性檢測了在系統執行結束的時候，所時間的程序運行可能不會讓隊列填滿了等待控制器響應的報文，但是NoForgottenPackets屬性可以很容易檢測到這些。實現亮我們已經用Python編寫組建了NICE的原型實現，從而可以無縫地支持流行的控制平臺（提供了PythonAPI）上的OpenFlow應用了Pthon，我們了對一個動態的弱類型的語言進行符號執行的。改Python（onoictn3[4PythonNICE包含三個部：（i）一個模型檢測器（ii）一個具體符號執行引（iii）模型檢測器細節。為了給系統狀態設立檢查點和進行恢復，NICE采取了記錄到新數的數組（Python的術語是元組）PythonPython解釋分成了嵌套的if語句來進行快捷的評估，（ii）函數調用移到條件表達式之前來AST樹最后重新轉換回了源代碼來執行。性能評這里，我們展示了NICE是如何高效應對OpenFLow中大狀態空間的的數目NICE-NO-SWITCH-轉CPU轉CPU2345----實驗設置。我們在圖1的簡單的拓撲基礎上進行了實驗，其中終端主機進行以下行的數目NICE-NO-SWITCH-轉CPU轉CPU2345----1NICE-MC的窮盡搜索和沒有對交換機狀態典型表示的模型檢測的對比。沒有交換機狀態典型表示會造成不能識別等價狀態。兩個情況下都沒有開啟符號執行。NO-SWITCH-REDUCTION在四天的時間里都沒有完成5個的測試。簡化交換機模型的好處。我們用NICE 了????，是對由于使用簡化交換機模型而減少的狀態空間的度量，定義為????????(NO?CH?EDCIO)???????(NCE?C)。我們觀察到了以下結果????????????SWITCH- 中的增長速度的一般狀態空間減少ρ的有效性根據問題的大小（的數量）不同，并且也足夠（3個中減少了7個因子）。6與NICE-MC基于啟發式方法的搜索策略。圖6描述了在減少狀態空間中，相對于與報告的完全搜索（NICE-MC）的度量，NO-DELAYFLOW-IR方法的貢獻。我們省略UNUSUAL與其他模型檢測器比較。NICE-MC與兩個最先進的模型檢測器SPIN[12]和JPF[13]進行比較。我們用PROMELA和Java創建了系統模型，盡可能接近地了NICE中測試的系統。由于空間的限制，我們只是簡單地總結了結果，可以參看[26]得到詳細內容SPIN能比NICE進行更有效的完全搜索。SPIN的部分順序減少（PORpartial-orderreduction）4，對發掘的狀態增長速率僅僅減少了18%。這是因為即便是POR被應用到的最好的粒度，也不能區分獨4POR是一個防止發掘不需要的轉移序列的有名的技術（例如[27]）“理所當然的”，JPF已經比NICE在3個的時候慢了290個因子這是因為即使是我們又重寫了Java模型來明確可能的轉移在用4個的情況下也比NICE慢了5.5倍。ICE與其他的模型檢測器相比，能夠很好的平衡（i）在合適的粒度水平上捕捉系統并行，（ii簡化狀態空間以及（ii允許測試未更改的控制器程序這三個方面。真實應用試這一章中，我們報告了 應用到三個真實應用上的情況，分別是MAC學習交換機我們試驗的第一個應用是在NOX版（98LoC）中的pyswitch軟件。這個應用I：在遷移后主機不可達。這個相當微妙的是當主機B從一個地址遷移到NoBlackHoles屬性。如果規則有一個強B的新地址；然后，BMAC學習，允許未來的報文沿著直接NoBlackHoles屬性是我們正II：延遲的直接路徑。pyswitch也會違背StrictDirectPaths屬性，造成了次優的修復方式是在14行之后加入了另外一個install_rule調用，將地址和端口反轉，來從發出的數據流安裝規則。用這個“修復”，最終的程序滿足了StrictDirectPaths屬性。III：過量的泛洪。當我們在一個含有一個回路的拓撲上測試pyswitch 了一個負載平衡應用，它使用通配符規則根據客戶端IP地址來劃分數據流從而達到目客戶端打開了連到與兩個服務器副本相關的虛擬IP地址的TCP連接。除了默認的正確單個TCP連接的所有報發到同一個服務器副本上。在這我們給出NICE在原始代碼-IV：在重配置之后的下一個TCP報文總會被丟棄。在觀察到了一個對每一個流都正確安裝了轉發規則，應用還是不會指示交換機去轉發報文觸發packet_inTCP發送端最終會重傳丟失的報文，程序最終還是成功處理了每一個網絡請求，使得很難發現這個。這個降低了性能，并且在一次很長的-V：在重配置之后一些TCP報文被丟棄。在修復了-IV之后，NICE檢測到另外一個由于競爭情況的NoForgottenPackets。在從一個負載平衡政策轉換到另的轉發規則令以及隨后（ii）安裝一個或將報文定向到控制器的規則（每一個受影響的客戶端IP地址組都會有一個規則）令。因為這些命令并不是原子地執行的，在第一步和第二步之間發來的報不能匹配任何規則。OpenFlow規范規定了不的“原因代碼”到達控制器（如NO_MATCH）。正如所編寫的，packet_in響應方-VI：在地址解析的時候ARP報文被遺忘。NoForgottenPacketsARP報文。對于服務器產生的ARP消息也有類似的問題。-VII：在轉移過程中重復的SYN報文。一個FlowAffinity發現了一個微妙一個SYN報文意味著數據流是新的，應該遵循新的負載平衡政策。在這些重復的SYN報文中，一些連接（SYN之前到達的）可能會連接到一個服務器，而接下來的的注腳#2），但只是在仔細考慮之后了這是個問題。OpenFlow在負載較輕的時候可以通過選擇性地關閉一些鏈路并重定向流量到可選2），然后為每一個流作出的選擇。NOX的實現（374LoC）有一個常開的路由（能夠在低需求的時候承擔所有流量）以及一個按需的路由表（為高需求下的流裝在按需的路徑。我們定義以下的應用的正確性屬性：使用正確的路由表（UCortRoutingTable：這個屬性檢查控制器程序在從一個交換機接收到報文時，處理給所有交換機安裝規則以及根據網絡負載比它在物理上能夠承擔的的流量，降低在網絡頂層運行的終端應用的性能。NICE在這個應用中找到了幾個-VIII：新流的第一個報文被丟棄。一個NoForgottenPackets的揭示了一個與-V相同的。packed_in響應方法安裝了則卻沒有命令交換機轉發觸發那-IX：新流的開始幾個報文可能會丟棄。在修復了-VIIINICE在路徑中的第二個交換機發現了另外一個NoForgotenPkts為pkt_in響應方法機會將報文向到控制。然而因為在安裝程中的通延遲，報可以pkt_in時發生這個難被發。簡單地反過安裝這規則，從后一個交換機到第一個是不足夠的——安裝規則過程中不同的延遲仍然會導致一個報文到達還沒有（完成時處它，者一“障（可用的時候來確保在讓報文離開交換機之前為所有中間跳上安裝好規則。-X：只有在高負載的時候使用按需的路由。NICE 確使用的CorrectRoutingTableUsed。程序會在端口數據響應方法（當網絡感知的能-XI：在負載減少的時候報文可能被丟棄。在修復了-IX之后，NICE檢測到了另外一個NoForgottenPackets 。當負載減少的時候，程序會在常開的路徑中重運行NICE的系統2中，我們總結了在四種搜索策略下，NICE要用多少秒以及（多少轉移被發現了）去發現能夠揭示的第一個屬性。注意這個數目總體上比較小因為NICE可以很快地生成簡單的測試案例來觸發。一個例外是-VII，通過做PKT-SEQ-only搜索花了一個小時才找到，但是用UNUSAL5分鐘就能找到。我們的搜索中占27%）。-VII被FLOW-IR遺漏，因為重復的SYN被當作一個新的獨立的流（9%）PKT-SEQ-NO-IVX序員不會知道是什么引起了這些。例如，運行時檢測因為-IV和-V標志了NICE給出的——非常重要。覆蓋性和系統開銷的權具體的全局控制器變量：在符號執行每一個事件響應方法時，NICE會遺漏一些響開始，錯過來識別報文頭部字段的約束的機會。我們可以通過在不同響應方法調用3。OpenFlow特別的搜索策略。這些啟發相關工常，創造這樣的環境是一個手動的過程（例如[22]）。NICE重用了模型檢測的了理念—環境建模的負擔交給用戶。而且，NICE是第一個聲稱可以用這些技術去測試OpenFlow網絡的動態行為的。最后，NICE在為這個特定領域處理狀態空間作出了貢獻。Khurshid等人[23]讓模型檢測器能夠進行符號執行。我們和他們的工作都有在非常大減少了可行路徑造成的狀態空間因為不是所有代碼都是符號執行的，而且（ii）采OpenFlow和網絡測試。Frenetic[29]OpenFlow的特定域語言，目的是根除一大類編程錯誤運用Frenetic需要網絡程序員學習對Python的擴展去支持更次的記錄和重放功能。然而，它不能自動進行OpenFlow控制器程序的測試。Mai等人[31]用對網絡設備轉發信息基礎的靜態分析來發現了數據平面的問題。檢測OpenFlow轉中錯誤配置的二元決策圖的。我們認為這些工作與我們的正交，Bishop等人[33]驗證了測試終端主機協議規范的問題。在軟件定義網絡的新領域中，NICE檢測了網絡的本身。Kothari等人[34]用符號執行和開發者的輸入識別了協議對網絡協議的。對比之下，NICE結合了模型檢測和符號執行來為對模型檢測器的注總我們組件了NICE，一個以一種新奇的方式結合了模型檢測和具體符號執行來能夠自動進行OpenFlow應用特使的工具，并且能夠快速地發掘為流行的NOX平臺所編寫們將NICE運用到了三個重要的應用實現上，找到了11個。NICE的一個版現在已經在http 致我們感謝我們的ArvindKrishnamurhy以及提供很好反饋的的審閱者。我DarkoMarinov的有用的討論和在最開始的草稿上給出的評論。這項研究得到了這些成EuropeanUnion’sSeventhFrameworkProgramme(FP7/2007-2013)/ERCgrantagreement259110EuropeanResearchCouncil的資助。參考文AfNOGTakesByteOutofInternet.RecklessDrivingontheInternet.N.McKeown,T.Anderson,H.Balakrishnan,G.Parulkar,L.Peterson,J.Rexford,S.Shenker,andJ.Turner.OpenFlow:EnablingInnovationinCampusNetworks. Comput.Commun.Rev.,38:69–74,March2008.M.Canini,D.Kosti′c,J.Rexford,andD.Venzano.AutomatingtheTestingofOpenFlowApplications.InWRiPE,2011.N.Gude,T.Koponen,J.Pettit,B.Pfaff,M.Casado,N.McKeown,andS.Shenker.NOX:TowardsanOperatingSystemforNetworks. put.Commun.Rev.,38:105–110,July2008.M.Casado,M.J.Freedman,J.Pettit,J.Luo,N.Gude,N.McKeown,andS.Shenker.RethinkingEnterpriseNetworkControl.IEEE/ACMTransactionsonNetworking,17(4),August2009.A.Nayak,A.Reimers,N.Feamster,andR.Clark.Resonance:DynamicAccessControlforEnterpriseNetworks.InWREN,2009.N.Handigoletal.Plug-n-Serve:Load-BalancingWebTrafficusingOpenFlow,August MDemo.R.Wang,D.Butnariu,andJ.Rexford.OpenFlow-BasedServerLoadBalancingGoneWild.InHot-ICE,2011.B.er,S.Seetharaman,P.Mahadevan,Y.Yiakoumis,P.Sharma,S.Banerjee,andN.McKeown.ElasticTree:SavingEnergyinDataCenterNetworks.InNSDI,2010.D.Ericksonetal.ADemonstrationofVirtualMachineMobilityinanOpenFlowNetwork,August2008. MDemo.G.Holzmann.TheSpinModelChecker-PrimerandReferenceManual.Addison-Wesley,ReadingMassachusetts,2004.W.Visser,K.Havelund,G.Brat,S.Park,andF.Lerda.ModelCheckingPrograms.AutomatedSoftwareEngineering,10(2):203–232,2003.M.MusuvathiandD.R.Engler.ModelCheckingLargeNetworkProtocolImplementations.InNSDI,2004.C.E.Killian,J.W.Anderson,R.Jhala,andA.Vahdat.Life,Death,andtheCriticalTransition:FindingLivenessBugsinSystemsCode.InNSDI,2007.J.Yang,T.Chen,M.Wu,Z.Xu,X.Liu,H.Lin,M.Yang,F.Long,L.Zhang,andL.Zhou.MODIST:TransparentModelCheckingofUnmodifiedDistributedSystems.InNSDI,C.Cadar,D.Dunbar,andD.R.Engler.KLEE:UnassistedandAutomaticGenerationofHigh-CoverageTestsforComplexSystemsPrograms.InOSDI,2008.S.Bucur,V.Ureche,C.Zamfir,andG.Candea.ParallelSymbolicExecutionforAutomatedReal-WorldSoftwareTesting.InEuroSys,2011.C.BaierandJ.-P.Katoen.PrinciplesofModelChecking.TheMITPress,OpenvSwitch:AnOpenVirtualSwitch.OpenFlowSwitchSpecification.R.Sasnauskas,O.Landsiedel,M.H.Alizai,C.Weise,S.Kowalewski,andK.Wehrle.KleeNet:DiscoveringInsidiousInteractionBugsinWirelessSensorNetworksBeforeDeployment.InIPSN,2010.S.Khurshid,C.S.P?as?areanu,andW.Visser.GeneralizedSymbolicExecutionforModelCheckingandTesting.InTACAS,2003.P.Godefroid,N.Klar