A Formally Verified NAT
A Formally Verified NAT
复制标题
经过正式验证的 NAT
DOI：
--
复制
发表时间：
2017
期刊：
影响因子：
--
通讯作者：
George Candea
中科院分区：
文献类型：
--
作者：
Arseniy Zaostrovnykh;Solal Pirelli;Luis Pedrosa;K. Argyraki;George Candea
我们提出了一个用C语言编写的网络地址转换器（NAT），并根据RFC 3022证明其语义正确，并且无崩溃和内存安全。最近有很多关于网络验证的工作，但它主要是假设网络功能的模型，并证明特定于网络配置的属性，例如可达性和无环路。我们的证明直接适用于网络函数的C代码，并且它证明了没有实现错误。先前的工作认为这是不可行的（即，验证用C编写的真实的，有状态的网络功能无法扩展），但我们证明了其他方面：NAT是最流行的网络功能之一，并且维护需要适当更新和过期的每流状态，这是验证挑战的典型来源。我们通过使用分离逻辑的符号执行和证明检查的新组合来解决可扩展性挑战；这种组合很好地符合网络函数的典型结构。然后我们证明，在这种情况下，正式证明的正确性并不会以性能为代价。NAT代码、证明工具链和证明可在[58]获得。
We present a Network Address Translator (NAT) written in C and proven to be semantically correct according to RFC 3022, as well as crash-free and memory-safe. There exists a lot of recent work on network verification, but it mostly assumes models of network functions and proves properties specific to network configuration, such as reachability and absence of loops. Our proof applies directly to the C code of a network function, and it demonstrates the absence of implementation bugs. Prior work argued that this is not feasible (i.e., that verifying a real, stateful network function written in C does not scale) but we demonstrate otherwise: NAT is one of the most popular network functions and maintains per-flow state that needs to be properly updated and expired, which is a typical source of verification challenges. We tackle the scalability challenge with a new combination of symbolic execution and proof checking using separation logic; this combination matches well the typical structure of a network function. We then demonstrate that formally proven correctness in this case does not come at the cost of performance. The NAT code, proof toolchain, and proofs are available at [58].