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.