TC: Large: A Formal Platform for Analyzing Internet Routing

可靠的反应式路由系统 沃伦小亨特饰Sandip Ray 计算机科学系 德克萨斯大学奥斯汀分校 {hunt，sandip}@cs.utexas. edu反应式并发系统（例如路由器）由许多交互进程组成，这些进程在接收和传输消息时执行非终止计算。 这种路由系统的设计是容易出错的，并且非并发通信所固有的非确定性使得很难检测或诊断这种错误。 我们的工作是开发基于ACL 2的工具，以确保大规模反应式路由系统的可靠执行。我们的目标是开发一个可扩展的，机械化的基础设施，以证明反应式路由系统实现的正确和安全执行，通过：一个通用的框架，用于在许多抽象层上建模和指定系统;并开发一套工具和技术，在统一的逻辑基础上实现这种分析的机械化和自动化。 我们的研究利用ACL 2的通用推理引擎，同时增加了一个精简的建模和规范方法的工具套件。 我们将开发一系列有针对性的工具来验证这些系统的安全性、活性和安全属性，同时保持在一个单一的逻辑和证明系统中。为了便于验证协议层之间的对应关系，我们建议基于BDD和SAT技术的进步，使用自动验证工具来增强ACL 2的推理引擎。 归纳不变量的发明和证明是反应式系统验证中最耗时的活动之一，我们将在ACL 2中集成一个通用的符号模拟能力;这种技术可以在大量的计算步骤上符号模拟系统模型，从而通常避免单步归纳不变量的构建。 预期的结果将有助于自动化的反应系统，如路由器和CPS的mechanicalverification。

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.