newsfilter.io

JK Lee

Showing 1–1 of 1 transcripts.

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