Class Central is learner-supported. When you buy through links on our site, we may earn an affiliate commission.

YouTube

Automated Verification of Network Function Binaries

USENIX via YouTube

Overview

Explore an automated technique for verifying network function binaries in this NSDI '22 conference talk. Delve into the challenges of bridging abstraction levels between implementations and specifications without relying on specific data structures. Learn about the innovative use of "ghost maps" to model data structures and specify network functions. Discover how Klint, a new verification tool, can analyze network function binaries without source code or debug symbols, enabling operators to verify proprietary code. Examine the process of inferring control flow and types through NF-environment interactions, and understand how this approach allows for verification of entire NF binary stacks down to the NIC driver level. Gain insights into the performance and practical applications of this verification technique across multiple network function binaries.

Syllabus

Intro
Context
Network Functions
Hard part
Requirements
Translation
Source code
Exhaustive symbolic execution
Binaries
Klint
Outline
Verification performance
Summary

Taught by

USENIX

Reviews

Start your review of Automated Verification of Network Function Binaries

Never Stop Learning.

Get personalized course recommendations, track subjects and courses with reminders, and more.

Someone learning on their laptop while sitting on the floor.