Trustworthy Reactive Routing Systems

Background, Motivation, and Goals

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 are developing 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 are enhancing ACL2's reasoning engine with automated verification tools based on advances in BDD- and SAT-based techniques. For instance, the invention and proof of inductive invariants is one of the most time-consuming activities in reactive system verification. To address this, we are integrating into ACL2 a predicate abstraction mechnism and a general-purpose symbolic simulation capability; these techniques often obviate the expensive construction of single-step inductive invariants, by making judicious use of rewriting to "mine" effective predicates and applying symbolic simulation over a large number of computation steps to justify their invariance. The expected results will help automate the mechanical verification of reactive systems such as routers and CPSs.

We are also developing a program logic to facilitate reasoning about multiprocessor programs, under weak memory consistency guarantees. The memory model is based on the X86 multiprocessor memory model and the explicit goal is to facilitate reasoning about inherently racey multiprocessor programs (e.g., concurrent data structure updates).

Funding, Personnel, and Organizations

The research has been funded by the National Science Foundation under Grant CNS-0910913, and by the Defense Advanced Research Projects Agency under Grant CNS-0429591.[1] Here are the people who have been involved in this research so far in various capacities. We're looking for more help, so if you're interested in the work feel free to talk to us.

Publications

The publications below are posted roughly in reverse chronological order.

[1] Any opinions, findings and conclusions or recomendations expressed in this material are those of the authors and do not necessarily reflect the views of the Defense Advanced Research Projects Agency or the National Science Foundation.