A Formally Verified NAT

Authors:

Arseniy Zaostrovnykh*

Solal Pirelli*

Luis Pedrosa*

Katerina Argyraki*

George Candea*

*EPFL, Switzerland

http://delivery.acm.org/10.1145/3100000/3098833/p141-Zaostrovnykh.pdf?ip=128.97.8.14&id=3098833&acc=OPEN&key=CA367851C7E3CE77%2E79535EF926D6BC05%2E4D4702B0C3E38B35%2E6D218144511F3437&CFID=975190330&CFTOKEN=93017280&__acm__=1503375257_d9b9bc2b9428feb87b2eb0fdf116d348

As Arseniy stated, this is a work that applies directly to the software network functions rather than assuming models of them.

The contribution of the paper is a Network Address Translator (NAT) function (NF) written in C whose correctness is formally verified as being in line with the semantics specified in RFC3022.

This approach uses different verification techniques for different parts of the code (a new combination of symbolic execution and formal proof checking using separation logic), and combines the results through so-called "lazy proofs" (a lazy proof consists of sub-proofs structured in a way that top-level proofs proceed assuming lower level properties, and the latter are proven lazily a posteriori). All these make it a novel work which aims to improve the state of the art on two fronts: (1) verify high-level semantic properties, such as the correct implementation of an RFC, and (2) verify the stateful property (that Network Functions that are stateful). 

To verify this NAT, the authors developed a verification toolchain, called Vigor.

Experimental results demonstrate the practicality of the in question approach: the verified NAT box performs as well as an unverified Data Plane Development Kit (DPDK) NAT and outperforms the standard Linux NAT. 

———————

Questions & Answers:

Q: How difficult is to generalise for mor RFCs?

A: While it took us 3 man days for the RFC3022 specifically, can't say for sure about how such generalisation could be implemented. May be some future work could consider a kind of automatic parsing of these specifications.

Q: How long would take to verify the whole data plane 

A: Most of the network verification projects use SAM simplified representation of middleboxes which take these models and specifications and verify the network function code. However these models are just abstractions of the real network and not the "real code" and this is where we can fit.

Q:  Do the programs have loop in them or short bounded loops?

A: Yes, it is important that they might have single loops, however we can deal with other data structures and apply our algorithm again.