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

• ReceivedJul 31, 2018
• AcceptedFeb 18, 2019
• PublishedMay 8, 2019
Share
Rating

### 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
 Device Event Messages Operations 5*Switch SwPktHandle PACKET_IN Read SwMsgHandle PACKET_OUT, FLOW_MOD Read, add, modify, delete SwPktSend $\bot$ $\emptyset$ SwMsgSend PACKET_IN, FLOW_REMOVED $\emptyset$ SwFlowRemoved FLOW_REMOVED Delete 2*Controller CtrlMsgHandle $\bot$ $\emptyset$ CtrlMsgSend PACKET_OUT, FLOW_MOD $\emptyset$ 2*Host HostPktHandle $\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 events SDN-predict SDNRacer cmidrule11-14 App. Topology Controller Total WR RD Races Comm. Time Remain. Races Comm. Time Remain. 2*Star Pox EEL 193 7 42 309 255 74 10 294 218 66 10 Floodlight 314 7 70 511 227 236 48 494 223 227 44 Learning- 2*Mesh Pox EEL 274 16 66 570 403 143 24 532 387 121 24 switch Floodlight 233 6 66 204 68 131 5 190 64 125 1 2*BinTree Pox EEL 4033 487 663 64086 62571 1449 66 62066 61337 664 65 Floodlight 9230 1251 904 281380 274643 6076 661 275246 270207 4737 302 5*Star Pox Angler 106 4 16 68 35 25 8 61 33 21 7 Pox EEL 145 8 19 180 135 35 10 109 84 24 1 Pox EEL Fx 184 8 29 260 195 53 12 189 145 42 2 ONOS 476 18 71 1431 1248 133 50 1336 1163 127 46 Floodlight 97 3 13 42 14 18 10 35 13 14 8 5*Mesh Pox Angler 248 13 48 345 125 200 20 323 116 191 16 For- Pox EEL 306 20 50 590 348 217 25 405 235 159 7 warding Pox EEL Fx 303 16 51 464 348 97 19 276 206 62 8 ONOS 880 44 181 4444 4135 256 53 4059 3781 228 50 Floodlight 180 6 36 114 46 52 16 104 46 45 13 5*BinTree Pox Angler 2106 286 359 20935 13397 7230 308 20447 13179 6988 280 Pox EEL 4362 504 453 51918 40203 11378 337 34385 27956 6201 228 Pox EEL Fx 4283 467 413 44297 42977 1199 121 12509 12238 242 29 ONOS 8031 1492 920 248521 244687 3472 362 236429 233578 2598 253 Floodlight 1886 203 323 12681 11856 554 271 12293 11766 317 210 Circuit- Star Floodlight 218 25 41 1325 1052 230 43 1301 1040 218 43 pusher Mesh Floodlight 327 42 74 1974 1597 311 66 1933 1581 287 65 BinTree Floodlight 1200 144 227 6298 5610 639 49 6156 5605 507 44 3*FireWall Star Floodlight 190 3 36 111 37 65 9 104 35 62 7 Mesh Floodlight 221 6 48 150 58 76 16 139 56 69 14 BinTree Floodlight 841 52 170 1457 1093 278 86 1384 1090 228 66 Load- Star4 Floodlight 3889 822 476 728703 709379 17086 2238 703864 685158 16492 2214 balancer Mesh4 Floodlight 5475 1036 735 333483 327929 4796 758 319121 314091 4303 727 BinTree Floodlight 24612 6213 2163 4816843 4850370 64987 1486 4705379 4642118 62031 1230 Total races text– 7187 text– 6014

a

Citations

• #### 0

Altmetric

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