基于抽象解释的IP网络中的分组流分析
Packet flow analysis in IP networks via abstract interpretation
摘要：
IP网络模型的静态分析（也称为离线分析）对于理解、调试和验证网络的分组流属性是有用的。在文献中已经提出了基于模型检验和图可达性的网络的静态分析方法。抽象解释是一种典型地应用于程序的静态分析的方法。我们提出了一种新的，抽象的解释为基础的方法来分析网络。我们形式化我们的方法，提到它的正确性保证，并展示了它的灵活性，在解决多个网络分析问题，以前已经解决了通过量身定制的方法。最后，我们研究了我们的分析应用到一个新的问题-推断一个高层次的网络策略-这在过去只在受限的单路由器设置中得到了解决。
英文摘要：
Static analysis (aka offline analysis) of a model of an IP network is useful for understanding, debugging, and verifying packet flow properties of the network. There have been static analysis approaches proposed in the literature for networks based on model checking as well as graph reachability. Abstract interpretation is a method that has typically been applied to static analysis of programs. We propose a new, abstract-interpretation based approach for analysis of networks. We formalize our approach, mention its correctness guarantee, and demonstrate its flexibility in addressing multiple network-analysis problems that have been previously solved via tailor-made approaches. Finally, we investigate an application of our analysis to a novel problem -- inferring a high-level policy for the network -- which has been addressed in the past only in the restricted single-router setting.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
