logo

SCIENCE CHINA Information Sciences, Volume 62, Issue 6: 062101(2019) https://doi.org/10.1007/s11432-018-9826-x

Predictive analysis for race detection in software-defined networks

More info
  • ReceivedJul 31, 2018
  • AcceptedFeb 18, 2019
  • PublishedMay 8, 2019

Abstract

Race condition remains one kind of the most common concurrency bugs in software-defined networks (SDNs). The race conditions can be exploited to lead tosecurity and reliability risks. However, the race conditions are notoriously difficult to detect. The existing race detectors for SDNs have limited detection capability. They can only detect the races in the original traces (observed traces) and cause false negatives. In this study, we present a predictive analysis framework called SDN-predict for race detection in SDNs.By encoding the order between the specified network events in SDNs as constraint, we formulate race detection as a constraint solving problem. In addition to detectingthe races in the original trace, our framework can also detect the races in the feasible traces got from reordering the events in the original trace while satisfying the consistency requirements of trace. Moreover, we formally prove that our predictive analysis framework is sound and can achieve the maximal possible detectioncapability for any sound dynamic race detector with respect to the same trace. We evaluate our framework on a set of traces collected from three SDN controllers (POX, Floodlight, ONOS), running 5 representative applicationsincluding reactive and proactive applications in large networks, on three different network topologies. These experiments show that our framework has higherrace detection capability than exisiting SDN race detector-SDNRacer, and detects more 1173 races. These 1173 races were previously undetected and confirmed by checking the race graphs.


Acknowledgment

This work was partially supported by National Basic Research Program of China (973 Program) (Grant No. 2014CB340702), National Natural Science Foundation of China (Grant Nos. 91418202, 61472178, 91318301), and National Science Foundation for Young Scientists of China (Grant No. 61702256).


References

[1] Open Networking Foundation. OpenFlow Switch Specification. version 1.3.3. 2013. https://www.opennetworking.org/wp-content/uploads/2014/10/\\openflow-spec-v1.3.3.pdf. Google Scholar

[2] Deng D D, Jin G L, de Kruijf M. Fixing, preventing, and recovering from concurrency bugs. Sci China Inf Sci, 2015, 58: 1-18 CrossRef Google Scholar

[3] Wu Z, Lu K, Wang X. Surveying concurrency bug detectors based on types of detected bugs. Sci China Inf Sci, 2017, 60: 031101 CrossRef Google Scholar

[4] Xu L, Huang J, Hong S M, et al. Attacking the brain: races in the SDN control plane. In: Proceedings of the 26th USENIX Security Symposium, Vancouver, 2017. 451--468. Google Scholar

[5] Cai Y, Cao L W. Effective and precise dynamic detection of hidden races for Java programs. In: Proceedings of the 10th Joint Meeting of the European Software Engineering Conference and the ACM SIGSOFT Symposium on the Foundations of Software Engineering, Bergamo, 2015. 450--461. Google Scholar

[6] Huang J, Meredith P O, Rosu G. Maximal sound predictive race detection with control flow abstraction. In: Proceedings of the 35th ACM SIGPLAN Conference on Programming Language Design and Implementation, Edinburgh, 2014. 337--348. Google Scholar

[7] Huang J, Zhou J, Zhang C. Scaling predictive analysis of concurrent programs by removing trace redundancy. ACM Trans Softw Eng Methodol, 2013, 22: 1-21 CrossRef Google Scholar

[8] Liu P, Tripp O, Zhang X Y. IPA: improving predictive analysis with pointer analysis. In: Proceedings of the 25th International Symposium on Software Testing and Analysis, Saarbrücken, 2016. 59--69. Google Scholar

[9] Wang C, Kundu S, Limaye R. Symbolic predictive analysis for concurrent programs. Form Asp Comp, 2011, 23: 781-805 CrossRef Google Scholar

[10] El-Hassany A, Miserez J, Bielik P, et al. SDNRacer: concurrency analysis for software-defined networks. In: Proceedings of the 37th ACM SIGPLAN Conference on Programming Language Design and Implementation, Santa Barbara, 2016. 402--415. Google Scholar

[11] Zhang Z, Chen Z, Gao R. An empirical study on constraint optimization techniques for test generation. Sci China Inf Sci, 2017, 60: 012105 CrossRef Google Scholar

[12] Big Switch Networks, Inc. Floodlight learning switch. 2013. https://github.com/floodlight/floodlight/tree/v0.91/src/main\\/java/net/floodlightcontroller/learningswitch. Google Scholar

[13] McCauley J. POX EEL L2 learning switch. 2015. https://github.com/noxrepo/pox/blob/eel/pox/forwarding/\\l2_learning.py. Google Scholar

[14] Big Switch Networks, Inc. Floodlight forwarding application. 2013. https://github.com/floodlight/floodlight/blob/v0.91/src/\\main/java/net/floodlightcontroller/forwarding/Forwarding.java. Google Scholar

[15] McCauley J. POX angler forwarding application. 2012. https://github.com/noxrepo/pox/blob/angler/pox/forwarding/\\l2_multi.py. Google Scholar

[16] McCauley J. POX EEL forwarding application. 2015. https://github.com/noxrepo/pox/blob/eel/pox/forwarding/\\l2_multi.py. Google Scholar

[17] Open Networking Laboratory. ONOS: forwarding application. 2015. https://github.com/opennetworkinglab/onos/tree/onos-1.2/apps/fwd. Google Scholar

[18] Big Switch Networks, Inc. Floodlight circuit pusher application. 2013. https://github.com/floodlight/floodlight/tree/v0.91/\\apps/circuitpusher. Google Scholar

[19] Big Switch Networks, Inc. Floodlight firewall. 2013. https://github.com/floodlight/floodlight/tree/v0.91/src/main/java/net/\\floodlightcontroller/firewall. Google Scholar

[20] Big Switch Networks, Inc. Floodlight load-balancer application. 2013. https://github.com/floodlight/floodlight/tree/v0.91/\\src/main/java/net/floodlightcontroller/loadbalancer. Google Scholar

[21] Sun X S, Agarwal A, Ng T S E. Controlling Race Conditions in OpenFlow to Accelerate Application Verification and Packet Forwarding. IEEE Trans Netw Serv Manage, 2015, 12: 263-277 CrossRef Google Scholar

[22] Majumdar R, Tetali S D, Wang Z. Kuai: a model checker for software-defined networks. In: Proceedings of the 14th International Conference on Formal Methods in Computer-Aided Design, Portland, 2014. 163--170. Google Scholar

[23] Khurshid A, Zhou W, Caesar M. Veriflow: verifying network-wide invariants in real time. SIGCOMM Comput Commun Rev, 2012, 42: 467-472 CrossRef Google Scholar

[24] May R, EI-Hassany A, Vanbever L, et al. BigBug: practical concurrency analysis for SDN. In: Proceedings of the Symposium on SDN Research, Santa Clara, 2017. 88--94. Google Scholar

[25] Naik M, Aiken A, Whaley J. Effective static race detection for Java. In: Proceedings of ACM SIGPLAN Conference on Programming Language Design and Implementation, Ottawa, 2006. 308--319. Google Scholar

[26] Luo Z D, Hillis L, Das R, et al. Effective static analysis to find concurrency bugs in Java. In: Proceedings of the 12th IEEE International Working Conference on Source Code Analysis and Manipulation, Timisoara, 2010. 135--144. Google Scholar

[27] Pozniansky E, Schuster A. Efficient on-the-fly data race detection in multithreaded C+ programs. In: Proceedings of ACM SIGPLAN Symposium on Principles and Practice of Parallel Programming, San Diego, 2003. 179--190. Google Scholar

[28] Serebryany K, Iskhodzhanov T. ThreadSanitizer: data race detection in practice. In: Proceedings of the Workshop on Binary Instrumentation and Applications, New York, 2009. 62--71. Google Scholar

[29] Xie X W, Xue J L. Acculock: accurate and efficient detection of data races. In: Proceedings of the 9th International Symposiumon Code Generation and Optimization, Nanjing, 2011. 201--212. Google Scholar

[30] Yu Y, Rodeheffer T, Chen W. RaceTrack: efficient detection of data race conditions via adaptive tracking. In: Proceedings of ACM Symposium on Operating Systems Principles, Brighton, 2005. 221--234. Google Scholar

[31] Yannis S, Jacob M E, Caitlin S, et al. Sound predictive race detection in polynomial time. In: Proceedings of the 39th annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, Philadelphia, 2012. 387--399. Google Scholar

[32] Dileep K, Umang M, Mahesh V. Dynamic race prediction in linear time. In: Proceedings of the 38th ACM SIGPLAN Conference on Programming Language Design and Implementation, Barcelona, 2017. 157--170. Google Scholar

[33] Savage S, Burrows M, Nelson G. Eraser: a dynamic data race detector for multithreaded programs. ACM Trans Comput Syst, 1997, 15: 391-411 CrossRef Google Scholar

[34] Flanagan C, Freund S N. FastTrack: efficient and precise dynamic race detection. In: Proceedings of the 30th Annual ACM SIGPLAN Conference on Programming Language Design and Implementation, Dublin, 2009. 121--133. Google Scholar

[35] Sen K. Race directed random testing of concurrent programs. In: Proceedings of the 29th Annual ACM SIGPLAN Conference on Programming Language Design and Implementation, Tucson, 2008. 11--21. Google Scholar

[36] Callahan R, Choi J D. Hybrid dynamic data race detection. In: Proceedings of the 9th ACM SIGPLAN Symposium on Principles and Practice of Parallel Programming, California, 2003. 167--178. Google Scholar

  • Figure 1

    (Color online) An example of a LearningSwitch application in Floodlight and a sequence of events (represented by numbers) which causes three race conditions.

  • Figure 2

    (Color online) A segment of event sequence in Figure 1 and two race conditions detected by SDN-predict.

  • Figure 3

    (Color online) Another segment of event sequence in Figure 1 and a race condition detected by SDN-predict.

  • Figure 4

    (Color online) The overview of SDN-predict.

  • Figure 5

    The constraint encoding for the trace in our example.

  • Figure 6

    (Color online) Race detection capability of the two detectors. LS: LearingSwitch, FO: Forwarding, CP: CircuitPusher, FW: FireWall, LB: LoadBalancer, S: Star, M: Mesh, B: BinTree, PE: Pox EEL, F: Floodlight, PA: Pox Angler, PEF: Pox EEL Fx, O: ONOS.

  • Figure 7

    (Color online) Analysis time for traces from Table 3.

  • Table 1   The events in each SDN device and their related messages and operations
    DeviceEventMessagesOperations
    5*SwitchSwPktHandlePACKET_INRead
    SwMsgHandlePACKET_OUT, FLOW_MODRead, add, modify, delete
    SwPktSend$\bot$$\emptyset$
    SwMsgSendPACKET_IN, FLOW_REMOVED$\emptyset$
    SwFlowRemovedFLOW_REMOVEDDelete
    2*ControllerCtrlMsgHandle$\bot$$\emptyset$
    CtrlMsgSendPACKET_OUT, FLOW_MOD$\emptyset$
    2*HostHostPktHandle$\bot$$\emptyset$
    HostPktSend$\bot$$\emptyset$
  • Table 2   The encoding rules for MHB constraints ($X_{e_1.{\rm~eid}}~<~X_{e_2.{\rm~eid}}$)
    CategoryRuleEvent 1Event 2
    4*
    pid_out $\rightarrow$ pid_in
    $(e_2.{\rm~pid}~\in~e_1.{\rm~out}\_{\rm~pids})$
    1
    $e_1$ $\in$ SwPktHandle $\cup$ SwMsgHandle
    $e_2$ $\in$ SwPktSend
    2
    $e_1$ $\in$ SwPktHandle $\cup$ SwMsgHandle
    $e_2$ $\in$ SwMsgHandle
    3$e_1$ $\in$ HostPktHandle$e_2$ $\in$ HostPktSend
    4
    $e_1$ $\in$ SwPktSend $\cup$ HostPktSend
    $e_2$ $\in$ SwPktHandle $\cup$ HostPktHandle
    4*
    mid_out $\rightarrow$ mid_in
    $(e_2.{\rm~mid}~\in~e_1.{\rm~out}\_{\rm~mids})$
    5
    $e_1$ $\in$ SwPktHandle $\cup$ SwMsgHandle
    $\cup$ SwFlowRemoved
    $e_2$ $\in$ SwMsgSend
    6$e_1$ $\in$ CtrlMsgHandle$e_2$ $\in$ CtrlMsgSend
    7$e_1$ $\in$ SwMsgSend$e_2$ $\in$ CtrlMsgHandle
    8$e_1$ $\in$ CtrlMsgSend$e_2$ $\in$ SwMsgHandle
    BARRIERPRE
    ($e_2.{\rm~msg\_type}$ = BARRIER
    $e_1.{\rm~sw}~=~e_2.{\rm~sw}$ $e_1~\prec_{\tau}~e_2$)
    9$e_1$ $\in$ SwMsgHandle$e_2$ $\in$ SwMsgHandle
    BARRIERPOST
    ($e_1.{\rm~msg\_type}$ =BARRIER
    $e_1.{\rm~sw}~=~e_2.{\rm~sw}$ $e_1~\prec_{\tau}~e_2$)
    10$e_1$ $\in$ SwMsgHandle$e_2$ $\in$ SwMsgHandle
    ALT_BARRIERPRE
    ($e_2.{\rm~msg\_type}$ = BARRIER
    $e_1.{\rm~sw}~=~e_2.{\rm~sw}$ $e_1~\prec_{\tau}~e_2$)
    11$e_1$ $\in$ CtrlMsgHandle$e_2$ $\in$ SwMsgHandle
    ALT_BARRIERPOST
    ($e_1.{\rm~msg\_type}$ = BARRIER
    $e_1.{\rm~sw}~=~e_2.{\rm~sw}$ $e_1~\prec_{\tau}~e_2$)
    12$e_1$ $\in$ CtrlMsgHandle$e_2$ $\in$ SwMsgHandle
    TIME1 ($e_2.t~-e_1.t~>~\delta$)
    13
    $e_1~\in$ SwPktHandle
    $\cup$ SwMsgHandle
    $e_2~\in$ SwMsgHandle
    TIME2 ($e_2.t~-e_1.t~>~\delta$)
    14$e_1~\in$ SwMsgHandle
    $e_2~\in$ SwPktHandle $\cup$ SwMsgHandle
    FlOW_REMOVED
    ($e_2.t~-e_1.t~>~\delta$)
    15$e_1~\in$ SwMsgHandle
    $e_2~\in$ AsyncFlowExpiry
  • Table 3   Reported races for different traces with applying time filter using $\delta~=2$ s$^{\rm~a)}$
    lrlr
    Num. of eventsSDN-predictSDNRacer
    cmidrule11-14 App.TopologyControllerTotalWRRDRacesComm.TimeRemain.RacesComm.TimeRemain.
    2*StarPox EEL19374230925574102942186610
    Floodlight3147705112272364849422322744
    Learning-
    2*MeshPox EEL27416665704031432453238712124
    switchFloodlight233666204681315190641251
    2*BinTreePox EEL40334876636408662571144966620666133766465
    Floodlight9230125190428138027464360766612752462702074737302
    5*StarPox Angler10641668352586133217
    Pox EEL145819180135351010984241
    Pox EEL Fx1848292601955312189145422
    ONOS476187114311248133501336116312746
    Floodlight97313421418103513148
    5*MeshPox Angler24813483451252002032311619116
    For-Pox EEL3062050590348217254052351597
    wardingPox EEL Fx30316514643489719276206628
    ONOS8804418144444135256534059378122850
    Floodlight180636114465216104464513
    5*BinTreePox Angler21062863592093513397723030820447131796988280
    Pox EEL436250445351918402031137833734385279566201228
    Pox EEL Fx428346741344297429771199121125091223824229
    ONOS8031149292024852124468734723622364292335782598253
    Floodlight188620332312681118565542711229311766317210
    Circuit-StarFloodlight218254113251052230431301104021843
    pusherMeshFloodlight327427419741597311661933158128765
    BinTreeFloodlight120014422762985610639496156560550744
    3*FireWallStarFloodlight1903361113765910435627
    MeshFloodlight221648150587616139566914
    BinTreeFloodlight8415217014571093278861384109022866
    Load-Star4Floodlight3889822476728703709379170862238703864685158164922214
    balancerMesh4Floodlight5475103673533348332792947967583191213140914303727
    BinTreeFloodlight24612621321634816843485037064987148647053794642118620311230
    Total racestext–7187text–6014

    a

Copyright 2020 Science China Press Co., Ltd. 《中国科学》杂志社有限责任公司 版权所有

京ICP备18024590号-1