-By Valentina De Vincenti
With the recent emergence of software-defined networking, which brings programmability and lowers the barrier for new functionalities into networks, the academic and industry communities have become very interested in the problem of network verification.
Networks are a vital infrastructure and ensuring their correctness is crucial for any application that moves its data over the network. For the very first time, Cocoon, which stands for Correct by Construction Networks, deals with network verification faster than existing competitors.
Cocoon was developed by Marco Canini, Professor of Computer Science (CS) from the Computer, Electrical & Mathematical Sciences and Engineering (CEMSE) Division, in a joined effort with Leonid Ryzhyk, project leader at VMware, along with researchers at Samsung, Microsoft, and other industry players. Cocoon was also successfully presented at the 14th USENIX Symposium on Networked Systems Design and Implementation (NSDI'17), a major conference in the field of networked systems.
"It is a very competitive conference, and we are pleased that the paper was among the 46 out of 253 submissions selected through a tough peer reviewing process," commented Canini.
Compared to previous existing verification tools, Cocoon gives to designers the ability to specify a higher level view of the network. In this way, it is possible to capture the correct network behavior verifying that the network implementation is equivalent to the high-level specification. Canini and co-workers' approach ensures a bug-free network by design since its very first stage.
"Cocoon can statically verify the network design without knowing the exact configuration. More specifically, Cocoon checks that the network design is correct in all possible configurations. This is an impressive result as it guarantees that the network never enters configurations that violate safety properties," stressed Canini.
Moreover, the team was also able to craft a tool to capture dynamic behavior that is only known at runtime. Thus, the designer can express assumptions in the specifications, which are later checked at runtime. Then, using the principle of stepwise refinement, Cocoon achieves faster verification of functional correctness than other approaches also proving that successive refinements of the high-level specification preserve the same network correctness.
In doing so, Cocoon advances the state-of-the-art significantly. Many prior works focused on verifying specific properties of a given snapshot of the data plane configuration of the network. Cocoon performs functional verification, which is more general than property based verification but can also be combined with other verification tools and enable them to run faster.
On the hit of international recognition, the team has already foreseen further developments. Canini and co-workers will continue to collaborate to enlarge the scope of network design supported by Cocoon for direct industry applications.
Related Persons
