Accession Number:

AD1024606

Title:

Formalizing Routing Models in ACL2

Descriptive Note:

Technical Report

Corporate Author:

University of Texas at Austin Austin United States

Report Date:

2008-03-19

Pagination or Media Count:

54.0

Abstract:

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.

Subject Categories:

  • Computer Systems

Distribution Statement:

APPROVED FOR PUBLIC RELEASE