P4BID: Information Flow Control in P4
summary
Tool implements an information-flow type system for P4 as a static type checker built on the P4 reference compiler, flags table-based leaks that arise when tables match on high (untrusted) keys and write to low (trusted) fields, and proves a non-interference theorem ensuring well-typed programs prevent high-to-low flows. Prototype catches real bugs (fixes typically require relabeling fields), focuses on tables only, and leaves recirculation and inter-packet/stateful leaks as open problems.
AI-written summary · about
chapters (9)
- 0:00Start
- 0:10SHIFTING TRENDS
- 0:51CUSTOMIZING A SWITCH
- 5:06INFORMATION FLOW CONTROL REFRESHER
- 6:22TYPE SYSTEM GUARANTEES
- 10:29SECURITY TYPES
- 11:36TYPING JUDGEMENT
- 12:10NON-INTERFERENCE THEOREM
- 12:29LEAKY TABLE
related talks
22mDependently-Typed Data Plane Programming
19mP4R-Type: A Verified API for P4 Control Plane Programs
15mOn Temporal Verification of Stateful P4 Programs
15mWhen P4 Meets Run-to-completion Architecture
18mP4Cub: A Little Language for Big Routers
27mPetr4: Formal Foundations for P4 Data Planes
22mP4-Based Automated Reasoning (P4-BAR) using Symbolic Execution
15mStructural Information Flow: A Fresh Look at Types for Non-Interference
