TC: Large: A Formal Platform for Analyzing Internet Routing

University Of Texas At Austin, Austin TX

Investigators

Abstract

Trustworthy Reactive Routing Systems Warren A. Hunt, Jr. and Sandip Ray Department of Computer Sciences University of Texas at Austin {hunt,sandip}@cs.utexas.edu Reactive concurrent systems, such as routers, consist of a number of interacting processes that perform non-terminating computations while receiving and transmitting messages. The design of such routing systems is error-prone, and non-determinism inherent in concurrent communications makes it hard to detect or diagnose such errors. Our effort will develop ACL2-based tools for ensuring trustworthy execution of large-scale reactive routing systems. We aim to develop a scalable, mechanized infrastructure for certifying correct and secure execution of reactive routing system implementations through: a generic framework for modeling and specifying systems at a number of abstraction layers; a compositional methodology for mathematically analyzing such models; and developing a suite of tools and techniques to mechanize and automate such analysis within a unified logical foundation. Our research exploits ACL2's general-purpose reasoning engine while augmenting the tool suite with a streamlined modeling and specification methodology. We will develop a collection of targeted tools for verifying safety, liveness, and security properties of such systems while staying within a single logic and proof system. To facilitate verification of correspondence between protocol layers, we propose to enhance ACL2's reasoning engine with automated verification tools based on advances in BDD- and SAT-based techniques. The invention and proof of inductive invariants is one of the most time-consuming activities in reactive system verification, and we will integrate into ACL2 a general-purpose symbolic simulation capability; this technique can symbolically simulate system models over a large number of computation steps, thereby often obviating the construction of single-step inductive invariants. The expected results will help automate the mechanical verification of reactive systems such as routers and CPSs.