Formalizing Routing Models in ACL2

W. A. Hunt, Jr., M. Kaufmann, R. B. Krug, and S. Ray

Technical Report TR-08-11, Department of Computer Sciences, University of Texas at Austin, March 2008.


We present two preliminary formalizations of router networks, both expressed in the logic of the ACL2 theorem prover. One formalization focuses on connectivity requirements by formalizing validity, visibility, and a trivial example routing policy, and demonstrates the ability to execute specifications. The other formalization focuses on network security properties, specifically information-flow and non-interference, and includes theorems demonstrating these properties for a simple formalization of a router network.

Relevant files