P4 Developer Days – Securing P4 Programs by Information Flow Control

Abstract

P4’s flexibility makes it easy to leak sensitive data without realizing it. A bad table entry, a copy-paste bug in a branch condition, or a stray debug field can quietly expose secrets to an untrusted network, and nothing in the toolchain today catches it.

I’ll show how our tool, TAP4S, catches this kind of leak automatically. You mark which fields are sensitive and which ports are untrusted, and it checks every path for violations, with no annotations or code changes required.

Speaker

Anoud Alshnakat is a PhD researcher in Formal Methods at KTH Royal Institute of Technology in Stockholm, where her work focuses on verifying and securing P4 data-plane programs (HOL4P4 and TAP4S). She’s especially interested in bringing formal methods closer to how developers actually write and reason about network code.