Jump to Content
Steffen Smolka

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
Google Publications
Other Publications
results

Year

Research Area

Sort By
  • Title
  • Title, descending
  • Year
  • Year, descending
    KATch: A Fast Symbolic Verifier for NetKAT
    Mark Moeller
    Jules Jacobs
    Olivier Savary Belanger
    David Darais
    Cole Schlesinger
    Steffen Smolka
    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
    Ali Kheradmand
    Steffen Smolka
    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
    No Results Found
    Search on Google Scholar