Steffen Smolka
I work on automated switch validation & verification, and all things P4, at Google.
Prior to joining Google full time, as an intern, I developed a static analysis tool for Google Cloud that now powers several features of Network Intelligence Center.
I received a Ph.D. in Computer Science from Cornell University in 2019, where I worked with Nate Foster and Dexter Kozen on programming languages, compilers, and automated verification tools for making networks more programmable and more reliable. I also received a Bc.S. in Computer Science from Technical University of Munich in 2013, where I worked with Jasmin Blanchette and Topias Nipkow on integrating automated and interactive theorem provers.
Research Areas
Authored Publications
Sort By
KATch: A Fast Symbolic Verifier for NetKAT
Mark Moeller
Jules Jacobs
Olivier Savary Belanger
David Darais
Cole Schlesinger
Nate Foster
Alexandra Silva
Programming Languages and Implementation (PLDI) (2024) (to appear)
Preview abstract
We develop new data structures and algorithms for checking verification queries in NetKAT, a domain-specific language for specifying the behavior of network data planes. Our results extend the techniques obtained in prior work on symbolic automata and provide a framework for building efficient and scalable verification tools. We present \KATch, an implementation of these ideas in Scala, including extended logical operators that are useful for expressing network-wide specifications and optimizations that construct a bisimulation quickly or generate a counter-example showing that none exists. We evaluate the performance of our implementation on real-world and synthetic benchmarks, verifying properties such as reachability and slice isolation, typically returning a result in well under a second, which is orders of magnitude faster than previous approaches.
View details
SwitchV: Automated SDN Switch Validation with P4 Models
Kinan Dak Albab
Jonathan Dilorenzo
Stefan Heule
Konstantin Weitz
Muhammad Tirmazi
Jiaqi Gao
Minlan Yu
SIGCOMM 2022 (2022)
Preview abstract
Increasing demand on computer networks continuously pushes
manufacturers to incorporate novel features and capabilities into
their switches at an ever-accelerating pace. However, the traditional
approach to switch development relies on informal specifications
and handcrafted tests to ensure reliability, which are tedious and
slow to maintain and update, effectively putting feature velocity at
odds with reliability.
This work describes our experiences following a new approach
during the development of switch software stacks that extend
fixed-function ASICs with SDN capabilities. Specifically, we focus on
SwitchV, our system for automated end-to-end switch validation
using fuzzing and symbolic analysis, that evolves effortlessly with
the switch specification. Our approach is centered around using the
P4 language to model the data plane behavior of the switch as well
as its control plane API. Such P4 models are then used as a formal
specification by SwitchV, as well as a switch-agnostic contract by
SDN controllers, and a living documentation by engineers.
SwitchV found a total of 154 bugs spanning all switch layers.
The majority of bugs were highly relevant and fixed within 14 days.
View details
