Specification Generation for Neural Networks in Networking Systems

Specifications - precise mathematical representations of correct domain-specific behaviors - are crucial to guarantee the trustworthiness of networking systems. With increasing development of neural networks (NNs) as networking system components, specifications gain more importance as they can be used to regulate the behaviors of these black-box models. Traditionally, specifications are designed by domain experts. However, this is labor-intensive and hence not scalable. We hypothesize that the traditional (aka reference) algorithms that NNs replace for higher performance can act as effective proxies for correct behaviors of the models, when available. This is because they have been used for long enough to encode several aspects of the trustworthy/correct behaviors in the underlying domain. Driven by our hypothesis, we develop a novel automated framework, SpecTRA to generate specifications for NNs using references. We formulate specification generation as an optimization problem and solve it with observations of reference behaviors. SpecTRA clusters similar observations into compact specifications. We present SpecTRA's specifications for NNs as adaptive bit rate and congestion control algorithms. Our specifications aid formal verification and show previously unknown vulnerabilities of NNs for networking systems.