Paper: Explainable Network Verification via Localized Subspecification
Authors: Yongzheng Zhang, Yaxuan Lin, Haoxian Chen, Ruize Ma, Amirmohammad Nazari, Mukund Raghothaman, Peng Zhang
Presenter: Mengqi Fu, Xiamen University
Guest of Honor: Yongzheng Zhang, ShanghaiTech University
Q：What feedback did you receive from the engineers and students in the user study? What were the most common suggestions for improving the explanations, and was there any feedback that particularly surprised you?
A：Some participants thought subspecifications were useful for network management, especially when operators trusted the results. However, some engineers felt that the subspecifications were still complicated and not sufficiently practical for real networks. One important issue is that real networks contain many configuration elements, and even after filtering there can still be many non-empty subspecifications for operators to inspect. A possible future direction is therefore to further reduce the number of non-empty subspecifications and highlight only the most meaningful configuration locations and explanations for operators.
Q：What motivated you to focus on explainability, especially since explainability can be difficult to quantify? Were you inspired by ideas or techniques from software engineering or program analysis?
A：Network management requires very high reliability. Although tools such as network verification, synthesis, and repair can automate parts of network management, they are unlikely to completely replace network operators in the near future. Explanations can help operators understand and trust the results produced by these tools, and understand why a configuration satisfies or violates a network intent. This can make automated tools easier to use in practice. Similar ideas may also apply to software or program analysis. For example, if all other functions are fixed, characterizing the valid inputs and outputs of one selected function could help users understand that function’s behavior.
Q：Have you considered comparing Speculant with provenance-based approaches such as NetCov for identifying configuration lines that are relevant to a network intent? Such approaches may use more heuristic techniques and potentially achieve better performance, while subspecifications provide a more formal characterization.
A：Speculant’s subspecifications preserve the observed stable state rather than directly preserving the network intent, so the two approaches are somewhat different. Generating subspecifications can also be expensive because the system needs to compute them for many configuration locations. However, comparing the approaches in terms of which configuration locations they identify, as well as their accuracy and performance, is an interesting direction that the authors would like to explore.
Q：Can Speculant be used to explain or fix configuration errors? Configuration errors may be especially important in practical network operations.
A：Although this was not discussed in detail in the paper, Speculant can also be used to explain misconfigurations. Speculant takes the configuration and its resulting routing table as inputs. Even when the configuration violates the intent, the simulated routing table can still represent the stable state produced by that configuration. Therefore, Speculant can explain how individual configuration elements contribute to an incorrect stable state or routing table. However, actually fixing the error is more difficult because changing one configuration element may affect routing protocols and introduce dependencies on other routers, routing policies, or route attributes. Explaining these deeper routing dependencies and supporting network repair are directions the authors are currently working on.
Q：How did you arrive at the idea of using the router-level stable state as an interface for modular reasoning instead of reasoning about the entire network configuration at once?
A：Initially, the authors tried to compute subspecifications over the entire network, but that approach was too expensive and could take hours or even longer as the network grew. The idea was then to use the stable state obtained from model checking or simulation as an intermediate interface and perform modular reasoning based on that state. This avoids repeatedly reasoning about the complete network and significantly improves scalability. The authors consider this automatic modular reasoning approach to be one of the key ideas behind the system.
Q：In the example where the configuration is overly restrictive, could a conventional data-plane verifier using header-space analysis also identify the problem? If so, is the main advantage of Speculant that it explains the valid configuration range rather than merely detecting the issue?
A：The author had not evaluated that example using header-space analysis and said that they would try it and examine the result. The discussion suggested that a data-plane verifier with header-space analysis may indeed be able to identify that there is a problem, but it may not provide the same explanation of why the configuration is problematic or characterize the safe range of configuration values. The authors agreed that this distinction should be clarified in future revisions of the work.