TC: Large: A Formal Platform for Analyzing Internet Routing

可信赖的响应式路由系统Warren a . Hunt, Jr.和Sandip Ray，德克萨斯大学奥斯汀分校计算机科学系，响应式并发系统，如路由器，由许多交互进程组成，这些进程在接收和发送消息时执行非终止计算。这种路由系统的设计容易出错，并且固有的非并发通信的不确定性使得很难检测或诊断此类错误。我们将努力开发基于acl2的工具，以确保大规模响应路由系统的可靠执行。我们的目标是开发一个可扩展的、机械化的基础设施，通过以下方式来证明响应路由系统实现的正确和安全执行：一个用于在多个抽象层建模和指定系统的通用框架；对这类模型进行数学分析的组合方法；并开发一套工具和技术，在统一的逻辑基础上机械化和自动化这种分析。我们的研究利用了ACL2的通用推理引擎，同时用流线型建模和规范方法增强了工具套件。我们将在单一的逻辑和证明体系下，开发一系列有针对性的工具来验证这些系统的安全性、活动性和安全性。为了便于验证协议层之间的通信，我们建议使用基于BDD和sat技术进步的自动验证工具来增强ACL2的推理引擎。归纳不变量的发明和证明是反应系统验证中最耗时的活动之一，我们将在ACL2中集成通用的符号模拟能力；该技术可以在大量的计算步骤上象征性地模拟系统模型，从而通常避免了单步归纳不变量的构造。预期的结果将有助于自动化反应性系统（如路由器和cps）的机械验证。

Trustworthy Reactive Routing Systems Warren A. Hunt, Jr. and Sandip Ray Department of Computer Sciences University of Texas at Austin {hunt,sandip}@cs.utexas.eduReactive concurrent systems, such as routers, consist of a number ofinteracting processes that perform non-terminating computationswhile receiving and transmitting messages. The design of suchrouting systems is error-prone, and non-determinism inherent inconcurrent communications makes it hard to detect or diagnose sucherrors. Our effort will develop ACL2-based tools for ensuringtrustworthy execution of large-scale reactive routing systems.We aim to develop a scalable, mechanized infrastructure forcertifying correct and secure execution of reactive routing systemimplementations through: a generic framework for modeling andspecifying systems at a number of abstraction layers; acompositional methodology for mathematically analyzing such models;and developing a suite of tools and techniques to mechanize andautomate such analysis within a unified logical foundation. Ourresearch exploits ACL2's general-purpose reasoning engine whileaugmenting the tool suite with a streamlined modeling andspecification methodology. We will develop a collection of targetedtools for verifying safety, liveness, and security properties ofsuch systems while staying within a single logic and proof system.To facilitate verification of correspondence between protocollayers, we propose to enhance ACL2's reasoning engine with automatedverification tools based on advances in BDD- and SAT-basedtechniques. The invention and proof of inductive invariants is oneof the most time-consuming activities in reactive systemverification, and we will integrate into ACL2 a general-purposesymbolic simulation capability; this technique can symbolicallysimulate system models over a large number of computation steps,thereby often obviating the construction of single-step inductiveinvariants. The expected results will help automate the mechanicalverification of reactive systems such as routers and CPSs.