Formalizing Routing Models in ACL2
University of Texas at Austin Austin United States
Pagination or Media Count:
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.
- Computer Systems