Network address translation | EPFL Graph Search

Network address translation (NAT) is a method of mapping an IP address space into another by modifying network address information in the IP header of packets while they are in transit across a traffic routing device. The technique was originally used to bypass the need to assign a new address to every host when a network was moved, or when the upstream Internet service provider was replaced, but could not route the network's address space. It has become a popular and essential tool in conserving global address space in the face of IPv4 address exhaustion. One Internet-routable IP address of a NAT gateway can be used for an entire private network. As network address translation modifies the IP address information in packets, NAT implementations may vary in their specific behavior in various addressing cases and their effect on network traffic. The specifics of NAT behavior are not commonly documented by vendors of equipment containing NAT implementations.

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

A Formally Verified NAT

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

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 https://vignat.github.io/

Assoc Computing Machinery2017

A Location-Privacy Threat Stemming from the Use of Shared Public IP Addresses

Vincent Bindschaedler, Jean-Pierre Hubaux, Kévin Clément Huguenin, Nevena Vratonjic

This paper presents a concrete and widespread example of situation where a user’s location privacy is unintentionally compromised by others, specifically the location-privacy threat that exists at access points (public hotspots, FON, home routers, etc.) that have a single public IP and make use of network address translation (NAT). As users connected to the same hotspot share a unique public IP address, a single user’s making a location-based request is enough to enable a service provider to map the IP address of the hotspot to its geographic coordinates, thus compromising the location privacy of all the other connected users. When successful, the service provider can locate users within a few hundreds of meters, thus improving over existing IP-location databases. Even in the case where IPs change periodically (e.g., by using DHCP), the service provider is still able to update a previous (IP, Location) mapping by inferring IP changes from authenticated communications (e.g., cookies). The contribution of this paper is three-fold: (i) We identify a novel location-privacy threat caused by shared public IPs in combination with NAT. (ii) We formalize and analyze the threat theoretically. In particular we derive and provide expressions of the probability that the service provider will learn the mapping and of the expected proportion of victims. (iii) We experimentally assess the state in practice by using real traces (collected from deployed hotspots over a period of 23 days) of users who accessed Google services. We also discuss how existing countermeasures can thwart the threat.

Ieee Computer Soc2014

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