Arseniy Zaostrovnykh | EPFL Graph Search

About this result

This page is automatically generated and may contain information that is not correct, complete, up-to-date, or relevant to your search query. The same applies to every other page on this website. Please make sure to verify the information with EPFL's official sources.

Verification of Software Network Functions with No Verification Expertise

Arseniy Zaostrovnykh

Software network functions (NFs), such as a network address translator, load balancer, or proxy, promise to bring flexibility and rapid innovation to computer networks and to reduce operational costs. However, continuous updates and flexibility typically come with the risk of bugs. As networks are a critical component of modern computing (e.g., the Internet), both users and operators demand that they be as reliable as economically possible. One way to guarantee reliability is by formal verification. To prove the absence of bugs, formal verification applies rigorous mathematical logic. State-of-the-art formal verification methods either require substantial effort and verification expertise on the part of the practitioner or lack completeness. In particular, theorem proving, to guide a mechanical proof checker, requires a human to annotate the code they verify with logical steps, and this annotation is something for which NF developers typically lack the time or expertise to do. Whereas, symbolic execution (SE) can analyze the code automatically, hence requiring significantly less effort; but it has difficulties with the so-called path explosion. Fortunately, software NFs have a special structure:

They feature a single infinite event-processing loop, and most of their code is SE-friendly.
The non-SE-friendly parts implement well-defined data structures that are reused across NFs.

In this dissertation, we present Vigor, a new method and tool for verifying software NFs; it exploits this special structure of NFs. We make two contributions: First, we show that it is possible to develop software NFs that are guaranteed to satisfy a formal specification and at the same time exhibit competitive performance. We develop a practical toolchain for developing NFs in C by using a standard fast packet-processing framework. Vigor provides a library of formally verified data structures (libVig); this library replaces the parts posing a challenge to SE. The Vigor toolchain applies exhaustive SE to the NF code that uses libVig. Vigor introduces a new technique, which we call "lazy proofs", for automatically stitching the proofs together and, ultimately, for certifying the whole NF correct relative to its functional specification. Second, we show that practical high-level semantic verification of software NFs is possible. By practical, we mean a verification that (a) requires no verification input other than the specification (push-button), (b) guarantees correctness of the entire runtime software stack, i.e., OS, driver, framework, and NF (full-stack), and (c) does not require writing a comprehensive specification to verify the first line of code (pay-as-you-go). In summary, Vigor provides push-button, full-stack, pay-as-you-go formal verification of software NFs with no reduction in NF performance or developer productivity. To substantiate our claims we implement five NFs, prove their correctness, and show that their performance is as good as the performance of the fastest non-verified software NFs. All of our NFs achieve a median latency of 4.1±0.2 us and over 4 Mpps throughput with 10 Gbps network interfaces. In terms of developer productivity, an average partial property takes 6.4 lines of Python specification, and the verification of the full stack (NF, packet-processing framework, OS, driver) takes up to one day. The Vigor toolchain is open-source and is available, along with tutorials and example NF implementations, at vigor.epfl.ch.

EPFL2020

Performance Contracts for Software Network Functions

George Candea, Luis David Figueiredo Mascarenhas Moreira Pedrosa, Rishabh Ramesh Iyer, Solal Vincenzo Pirelli, Arseniy Zaostrovnykh

Software network functions (NFs), or middleboxes, promise flexibility and easy deployment of network services but face the serious challenge of unexpected performance behaviour. We propose the notion of a performance contract, a construct formulated in terms of performance critical variables, that provides a precise description of NF performance. Performance contracts enable fine-grained prediction and scrutiny of NF performance for arbitrary workloads, without having to run the NF itself. We describe BOLT, a technique and tool for computing such performance contracts for the entire software stack of NFs written in C, including the core NF logic, DPDK packet processing framework, and NIC driver. BOLT takes as input the NF implementation code and outputs the corresponding contract. Under the covers, it combines pre-analysis of a library of stateful NF data structures with automated symbolic execution of the NF’s code. We evaluate BOLT on four NFs—a Maglev-like load balancer, a NAT, an LPM router, and a MAC bridge—and show that its performance contracts predict the dynamic instruction count and memory access count with a maximum gap of 7% between the real execution and the conservatively predicted upper bound. With further engineering, this gap can be reduced.

USENIX ASSOC2019

A Formally Verified NAT Stack

George Candea, Solal Vincenzo Pirelli, Arseniy Zaostrovnykh

Prior work proved a stateful NAT network function to be semantically correct, crash-free, and memory safe. Their toolchain verifies the network function code while assuming the underlying kernel-bypass framework, drivers, operating system, and hardware to be correct. We extend the toolchain to verify the kernel-bypass framework and a NIC driver in the context of the NAT. We uncover bugs in both the framework and the driver. Our code is publicly available.

2018

Verification of Software Network Functions with No Verification Expertise

Arseniy Zaostrovnykh

They feature a single infinite event-processing loop, and most of their code is SE-friendly.
The non-SE-friendly parts implement well-defined data structures that are reused across NFs.

EPFL2020