2 options
Automated formal analysis of internet routing configurations.
- Format:
- Book
- Thesis/Dissertation
- Author/Creator:
- Wang, Anduo.
- Language:
- English
- Subjects (All):
- Computer science.
- 0984.
- Penn dissertations--Computer and Information Science.
- Computer and Information Science--Penn dissertations.
- Local Subjects:
- Penn dissertations--Computer and Information Science.
- Computer and Information Science--Penn dissertations.
- 0984.
- Physical Description:
- 173 pages
- Contained In:
- Dissertation Abstracts International 75-01B(E).
- System Details:
- Mode of access: World Wide Web.
- text file
- Summary:
- Today's Internet interdomain routing protocol, the Border Gateway Protocol (BGP), is increasingly complicated and fragile due to policy misconfigurations by individual autonomous systems (ASes). To create provably correct networks, the past twenty years have witnessed, among many other efforts, advances in formal network modeling, system verification and testing, and point solutions for network management by formal reasoning. On the conceptual side, the formal models usually abstract away low-level details, specifying what are the correct functionalities but not how to achieve them. On the practical side, system verification of existing networked systems is generally hard, and system testing or simulation provide limited formal guarantees. This is known as a long standing challenge in network practice---formal reasoning is decoupled from actual implementation.
- This thesis seeks to bridge formal reasoning and actual network implementation in the setting of the Border Gateway Protocol (BGP), by developing the Formally Verifiable Routing (FVR) toolkit that combines formal methods and programming language techniques. Starting from the formal model, FVR automates verification of routing models and the synthesis of faithful implementations that carries the correctness property. Conversely, starting from large real-world BGP systems with arbitrary policy configurations, FVR automates the analysis of Internet routing configurations, and also includes a novel network reduction technique that scales up existing techniques for automated analysis. By developing the above formal theories and tools, this thesis aims to help network operators to create and manage BGP systems with correctness guarantee.
- Notes:
- Thesis (Ph.D. in Computer and Information Science) -- University of Pennsylvania, 2013.
- Source: Dissertation Abstracts International, Volume: 75-01(E), Section: B.
- Advisers: Boon Thau Loo; Andre Scedrov.
- Local Notes:
- School code: 0175.
- ISBN:
- 9781303396946
- Access Restriction:
- Restricted for use by site license.
The Penn Libraries is committed to describing library materials using current, accurate, and responsible language. If you discover outdated or inaccurate language, please fill out this feedback form to report it and suggest alternative language.