Nate Foster
Showing 1–2 of 2 transcripts.
- Jane Street1h 35m
The Network as a Program with Nate Foster
Nate Foster, a professor at EPFL and visiting researcher at Jane Street, bridges programming languages and networking by advocating for treating networks as verifiable programs through formal methods and Domain Specific Languages like Netcat and P4. His work has evolved from foundational theories on bidirectional data conversion to practical industrial applications, including the Butane system which compiles high-level latency policies into safe, distributed BGP configurations to replace error-prone manual router management. Foster's approach combines algebraic analysis of routing semantics with a software engineering culture that prioritizes rigorous testing and visualization, enabling complex network modifications while challenging traditional end-to-end principles in favor of in-network computing for specialized workloads.
- Jane Street1h 13m
Nate Foster: Verifying Network Data Planes
Nate Foster, Bill Hallahan, JK Lee, Cole Schlesinger, Steffen Smolks, Robert Soule, Han Wang, Ron
Cornell Professor Nate Foster and Barefoot Networks have developed an automated verification tool for P4 programs running on programmable data planes to prevent catastrophic network failures caused by configuration errors. This system transforms P4 code into guarded commands to efficiently compute weakest preconditions using the Sacks and Flanagan algorithm, checking safety conditions against the Z3 SMT solver to generate counter-examples for invalid header accesses without requiring manual annotations. By modeling the separation between data and control planes through ghost state, the tool validates programs up to 20,000 lines of code in minutes, establishing a critical foundation for verifying complex software-defined network topologies.