Paper Info
Title
Aquila: a practically usable verification system for production-scale programmable data planes
Abstract
ABSTRACTThis paper presents Aquila, the first practically usable verification system for Alibaba's production-scale programmable data planes. Aquila addresses four challenges in building a practically usable verification: (1) specification complexity; (2) verification scalability; (3) bug localization; and (4) verifier self validation. Specifically, first, Aquila proposes a high-level language that facilitates easy expression of specifications, reducing lines of specification codes by tenfold compared to the state-of-the-art. Second, Aquila constructs a sequential encoding algorithm to circumvent the exponential growth of states associated with the upscaling of data plane programs to production level. Third, Aquila adopts an automatic and accurate bug localization approach that can narrow down suspects based on reported violations and pinpoint the culprit by simulating a fix for each suspect. Fourth and finally, Aquila can perform self validation based on refinement proof, which involves the construction of an alternative representation and subsequent equivalence checking. To this date, Aquila has been used in the verification of our production-scale programmable edge networks for over half a year, and it has successfully prevented many potential failures resulting from data plane bugs.
Year
DOI
Venue
2021
10.1145/3452296.3472937
COMM
Keywords
DocType
Citations 
Formal Methods, Programmable Switches, P4 Verification
Conference
0
PageRank 
References 
Authors
0.34
27
16
Name
Order
Citations
PageRank
Bingchuan Tian1124.22
Jiaqi Gao2183.75
Mengqi Liu3155.32
Ennan Zhai410019.42
Yanqing Chen500.34
Yu Zhou6206.47
Li Dai700.34
Feng Yan800.34
Mengjing Ma900.34
Ming Tang1000.34
Jie Lu1100.34
Xionglie Wei1200.34
Hongqiang Liu1349725.77
Ming Zhang143509181.37
Chen Tian15378.36
Li Dai168815.78