Paper titled “Computing Precise Control Interface Specifications” co-authored by TEIAS/Khatam faculty Dr. Hossein Hojjat (with collaborators from the Cornell University, Dr. Eric Campbell and Dr. Nate Foster) has been accepted for publication in The ACM SIGPLAN Object Oriented Programming Systems Languages and Applications (OOPSLA’24).
https://2024.splashcon.org/track/splash-2024-oopsla

OOPSLA is a top international conference which brings together experts in programming languages and software engineering to share the latest findings in these areas. This year’s conference will take place in Pasadena, California, United States October 20-25, 2024.

The abstract of the paper is the following:

“Verifying network programs is challenging because of how they divide labor: the control plane computes high level routes through the network and compiles them to device configurations, while the data plane uses these configurations to realize the desired forwarding behavior. In practice, the correctness of the data plane often assumes that the configurations generated by the control plane will satisfy complex specifications. Consequently, validation tools such as program verifiers, runtime monitors, fuzzers, and test-case generators must be aware of these control interface specifications (CISes) to avoid raising false alarms.
In this paper, we propose the first algorithm for computing precise CISes from data plane programs. Our specifications are designed to be efficiently monitorable-concretely, checking that a given configuration satisfies a CIS can be done in polynomial time. Our algorithm, based on modular program instrumentation, quantifier elimination, and a path-based analysis, is more expressive than prior work, and is applicable to practical network programs. We present an implementation and show that CISes computed by our tool are useful for finding real bugs in practical data plane programs.”