Network function virtualization

Summary

Network functions virtualization (NFV) is a network architecture concept that leverages IT virtualization technologies to virtualize entire classes of network node functions into building blocks that may connect, or chain together, to create and deliver communication services. NFV relies upon traditional server-virtualization techniques such as those used in enterprise IT. A virtualized network function, or VNF, is implemented within one or more virtual machines or containers running different software and processes, on top of commercial off the shelf (COTS) high-volume servers, switches and storage devices, or even cloud computing infrastructure, instead of having custom hardware appliances for each network function thereby avoiding vendor lock-in. For example, a virtual session border controller could be deployed to protect a network without the typical cost and complexity of obtaining and installing physical network protection units. Other examples of NFV include virtualized load

Official source

https://en.wikipedia.org/wiki/Network_function_virtualization

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.

Related publications (11)

Related publications

Related people (3)

Related people

Related units (3)

Related units

Related concepts (1)

Cloud computing is the on-demand availability of computer system resources, especially data storage (cloud storage) and computing power, without direct active management by the user. Large clouds of

Related concepts

Related courses (1)

Related courses

Related lectures (2)

Related lectures

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 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

A Formally Verified NAT Stack

George Candea, Solal Vincenzo Pirelli, Arseniy Zaostrovnykh

Prior work proved a stateful NAT network function to be, crash-free, memory safe and semantically correct [29]. 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 [28].

ASSOC COMPUTING MACHINERY2018