Automated Analysis for Correct and Efficient Execution ofSoftware Middleboxes
Loading...
Date
Authors
Zhang, Kaiyuan
Journal Title
Journal ISSN
Volume Title
Publisher
Abstract
Middleboxes are important building blocks of modern networks. They provide a wide range of functionalities such as packet transformation (e.g., NATs), security (e.g., firewalls), and performance (e.g., load balancers). As middleboxes reside on the data path of networked applications, their correctness and performance have significant implications.To improve the correctness guarantee of middlebox implementations, we studied the feasibility of applying automated verification techniques on existing middlebox implementations. Our study shows that, with slight code modifications, over 70% of existing Click elements could be verified using symbolic execution. Based on this result, we de-signed and implemented Gravel, a framework that allows developers to express RFC properties of middleboxes using its high-level specification API and verifies the correctness of middlebox implementations against those properties.To utilize the packet processing power of programmable switches, we designed and implemented Gallium, a compiler that performs program analysis on a software middle-box implementation and automatically discovers parts of the program that could be offloaded to the programmable switch. Gallium then generates code in P4, a domain-specific language for programmable switches. Gallium ensures the functional equivaence between the offloaded implementation and the original implementation and could save 21-79% of processing cycles.To help developers build efficient and scalable middlebox implementations, we present Pebble, a programming framework and runtime system that provides transaction API.Pebble hides the low-level implementation details of concurrency control from the developers. It uses transaction chopping to utilize the pipeline parallelism in middlebox applications and uses optimistic concurrency control to boost the performance for concurrent read operations. Our evaluation shows that developers could build scalable middleboxes with Pebble without significant effort compared with building single-threaded ones.
Description
Thesis (Ph.D.)--University of Washington, 2021
Keywords
, Computer science