Committee

  • David Walker (advisor)
  • Zak Kincaid
  • Aarti Gupta

Title

Flexible, line-rate flow monitoring of packet sequences

Abstract

A sequence monitor is responsible for identifying important patterns in a sequence of packets. In my talk, this is viewed as the sequence of packets flowing through a single programmable switch. I will present FLM, which is a language designed to specify sequence monitors that can be implemented at line rate on a programmable switch. FLM is an extension to the Lucid programming language, and has several interesting compilation steps first to core Lucid, and then to P4. A specification takes the form of a regular-expression-like syntax over network events, with the added ability to bind variables that can then be referred to later in the specification (an example in our applications might be a pattern containing all the same source IP address). The idea focuses on transforming such a specification into a preamble that contains all of the relevant variable-binding parts, and a new (classic) regular expression over events and predicates about the variables. The variable bindings are easy to implement in switch stages, and the regular expression is implemented via syntax-guided synthesis with an off-the-shelf SMT solver. I have attached a short paper published recently with two students from the Systems group about the sub-problem of synthesis of DFA implementations on switches.

Reading List

Papers

Runtime Verification
  1. "Aragog: Scalable Runtime Verification of Shardable Networked Systems". Nofel Yaseen,Behnaz Arzani, Ryan Beckett, Selim Ciraci, Vincent Liu. (link)
  2. "Monitoring Events that Carry Data ". Klaus Havelund, Giles Reger, Daniel Thoma, and Eugen Zălinescu. (link)
  3. "DBVal: Validating P4 Data Plane Runtime Behavior". K Shiv Kumar, Ranjitha K, P S Prashanth, Mina Tahmasbi Arashloo, Venkanna U., and Praveen Tammana (2021). (link)
Programmable switches / P4
  1. "Marple: Language-Directed Hardware Design for Network Performance Monitoring". Srinivas Narayana, Anirudh Sivaraman, Vikram Nathan, Prateesh Goyal, Venkat Arun, Mohammad Alizadeh, Vimalkumar Jeyakumar, Changhoon Kim. (link)
  2. "Switch Code Generation Using Program Synthesis". Xiangyu Gao, Taegyun Kim, Michael D. Wong, Divya Raghunathan, Aatish Kishan Varma, Pravein Govindan Kannan, Anirudh Sivaraman, Srinivas Narayana, and Aarti Gupta (2020). (link)
  3. "Lucid: a language for control in the data plane.". John Sonchack, Devon Loehr, Jennifer Rexford, and David Walker. (2021) (link)
Automata and Synthesis
  1. "Derivatives of Regular Expressions". Janusz A. Brzozowski (1964). (link)
  2. "Regular-expression derivatives re-examined". Scott Owens, John Reppy, Aaron Turon (2009). (link)
  3. "Symbolic Register Automata". Loris D'Antoni, Tiago Ferreira, Matteo Sammartino, and Alexandra Silva . (link)
  4. "Syntax guided synthesis". Rajeev Alur, Rastislav Bodik, Garvit Juniwal, Milo M. K. Martin, Mukund Raghothaman, Sanjit A. Seshia, Rishabh Singh, Armando Solar-Lezama, Emina Torlak, Abhishek Udupa. (link)

Textbooks

  1. Daniel Kroening and Ofer Strichman Decision Procedures: an Algorithmic Point of View, 2nd Edition Springer Science & Business Media, 2016.
    • Chapters 1-4
    • Chapter 10
  2. Benjamin C. Pierce. Types and Programming Languages. The MIT Press, 2002.
    • Chapters 1-24

Questions

  1. (Aarti Gupta) Is FLM compiled to DFAs? Can you expand on the expressiveness of FLM and its limitations?
  1. (Aarti Gupta) Are the rewrite rules complete; that is, can every expressible pattern be rewritten and compiled? If not, what is an example pattern that cannot be implemented?
  1. (Zak Kincaid) Draw and define the transition of a Symbolic Register Automaton. How would you encode your compiled FLM patterns as SRAs?
  1. (David Walker) Write the terms and values of the lambda calculus with functions, fixed-length tuples, and booleans. What is the subtype relation for functions and tuples? If you had a bogus tuple subtype relation, what is a program that would typecheck but still go wrong?
  1. (Aarti Gupta) About the Chipmunk Paper, what is the key thing that makes it succeed in compiling any P4 program to the Tofino hardware?