Analyzing BGP Instances in Maude
International audience Analyzing Border Gateway Protocol (BGP) instances is a crucial step in the design and implementation of safe BGP systems. Today, the analysis is a manual and tedious process. Researchers study the instances by manually constructing execution sequences, hoping to either identif...
Main Authors: | , , , , |
---|---|
Other Authors: | , , , , , , , |
Format: | Conference Object |
Language: | English |
Published: |
HAL CCSD
2011
|
Subjects: | |
Online Access: | https://hal.inria.fr/hal-01583330 https://hal.inria.fr/hal-01583330/document https://hal.inria.fr/hal-01583330/file/978-3-642-21461-5_22_Chapter.pdf https://doi.org/10.1007/978-3-642-21461-5_22 |
id |
ftifiphal:oai:HAL:hal-01583330v1 |
---|---|
record_format |
openpolar |
spelling |
ftifiphal:oai:HAL:hal-01583330v1 2023-05-15T16:49:24+02:00 Analyzing BGP Instances in Maude Wang, Anduo Talcott, Carolyn Jia, Limin Loo, Boon, Scedrov, Andre University of Pennsylvania SRI International Menlo Park (SRI) Carnegie Mellon University Pittsburgh (CMU) University of Pennsylvania School of Veterinary Medicine Roberto Bruni Juergen Dingel TC 6 WG 6.1 Reykjavik,, Iceland 2011-06-06 https://hal.inria.fr/hal-01583330 https://hal.inria.fr/hal-01583330/document https://hal.inria.fr/hal-01583330/file/978-3-642-21461-5_22_Chapter.pdf https://doi.org/10.1007/978-3-642-21461-5_22 en eng HAL CCSD Springer info:eu-repo/semantics/altIdentifier/doi/10.1007/978-3-642-21461-5_22 hal-01583330 https://hal.inria.fr/hal-01583330 https://hal.inria.fr/hal-01583330/document https://hal.inria.fr/hal-01583330/file/978-3-642-21461-5_22_Chapter.pdf doi:10.1007/978-3-642-21461-5_22 http://creativecommons.org/licenses/by/ info:eu-repo/semantics/OpenAccess Lecture Notes in Computer Science 13th Conference on Formal Methods for Open Object-Based Distributed Systems (FMOODS) / 31th International Conference on FORmal TEchniques for Networked and Distributed Systems (FORTE) https://hal.inria.fr/hal-01583330 13th Conference on Formal Methods for Open Object-Based Distributed Systems (FMOODS) / 31th International Conference on FORmal TEchniques for Networked and Distributed Systems (FORTE), Jun 2011, Reykjavik,, Iceland. pp.334-348, ⟨10.1007/978-3-642-21461-5_22⟩ [INFO]Computer Science [cs] [INFO.INFO-NI]Computer Science [cs]/Networking and Internet Architecture [cs.NI] info:eu-repo/semantics/conferenceObject Conference papers 2011 ftifiphal https://doi.org/10.1007/978-3-642-21461-5_22 2023-03-21T20:40:06Z International audience Analyzing Border Gateway Protocol (BGP) instances is a crucial step in the design and implementation of safe BGP systems. Today, the analysis is a manual and tedious process. Researchers study the instances by manually constructing execution sequences, hoping to either identify an oscillation or show that the instance is safe by exhaustively examining all possible sequences. We propose to automate the analysis by using Maude, a tool based on rewriting logic. We have developed a library specifying a generalized path vector protocol, and methods to instantiate the library with customized routing policies. Protocols can be analyzed automatically by Maude, once users provide specifications of the network topology and routing policies. Using our Maude library, protocols or policies can be easily specified and checked for problems. To validate our approach, we performed safety analysis of well-known BGP instances and actual routing configurations. Conference Object Iceland IFIP Open Digital Library (International Federation for Information Processing) Maude ENVELOPE(168.417,168.417,-83.150,-83.150) 334 348 |
institution |
Open Polar |
collection |
IFIP Open Digital Library (International Federation for Information Processing) |
op_collection_id |
ftifiphal |
language |
English |
topic |
[INFO]Computer Science [cs] [INFO.INFO-NI]Computer Science [cs]/Networking and Internet Architecture [cs.NI] |
spellingShingle |
[INFO]Computer Science [cs] [INFO.INFO-NI]Computer Science [cs]/Networking and Internet Architecture [cs.NI] Wang, Anduo Talcott, Carolyn Jia, Limin Loo, Boon, Scedrov, Andre Analyzing BGP Instances in Maude |
topic_facet |
[INFO]Computer Science [cs] [INFO.INFO-NI]Computer Science [cs]/Networking and Internet Architecture [cs.NI] |
description |
International audience Analyzing Border Gateway Protocol (BGP) instances is a crucial step in the design and implementation of safe BGP systems. Today, the analysis is a manual and tedious process. Researchers study the instances by manually constructing execution sequences, hoping to either identify an oscillation or show that the instance is safe by exhaustively examining all possible sequences. We propose to automate the analysis by using Maude, a tool based on rewriting logic. We have developed a library specifying a generalized path vector protocol, and methods to instantiate the library with customized routing policies. Protocols can be analyzed automatically by Maude, once users provide specifications of the network topology and routing policies. Using our Maude library, protocols or policies can be easily specified and checked for problems. To validate our approach, we performed safety analysis of well-known BGP instances and actual routing configurations. |
author2 |
University of Pennsylvania SRI International Menlo Park (SRI) Carnegie Mellon University Pittsburgh (CMU) University of Pennsylvania School of Veterinary Medicine Roberto Bruni Juergen Dingel TC 6 WG 6.1 |
format |
Conference Object |
author |
Wang, Anduo Talcott, Carolyn Jia, Limin Loo, Boon, Scedrov, Andre |
author_facet |
Wang, Anduo Talcott, Carolyn Jia, Limin Loo, Boon, Scedrov, Andre |
author_sort |
Wang, Anduo |
title |
Analyzing BGP Instances in Maude |
title_short |
Analyzing BGP Instances in Maude |
title_full |
Analyzing BGP Instances in Maude |
title_fullStr |
Analyzing BGP Instances in Maude |
title_full_unstemmed |
Analyzing BGP Instances in Maude |
title_sort |
analyzing bgp instances in maude |
publisher |
HAL CCSD |
publishDate |
2011 |
url |
https://hal.inria.fr/hal-01583330 https://hal.inria.fr/hal-01583330/document https://hal.inria.fr/hal-01583330/file/978-3-642-21461-5_22_Chapter.pdf https://doi.org/10.1007/978-3-642-21461-5_22 |
op_coverage |
Reykjavik,, Iceland |
long_lat |
ENVELOPE(168.417,168.417,-83.150,-83.150) |
geographic |
Maude |
geographic_facet |
Maude |
genre |
Iceland |
genre_facet |
Iceland |
op_source |
Lecture Notes in Computer Science 13th Conference on Formal Methods for Open Object-Based Distributed Systems (FMOODS) / 31th International Conference on FORmal TEchniques for Networked and Distributed Systems (FORTE) https://hal.inria.fr/hal-01583330 13th Conference on Formal Methods for Open Object-Based Distributed Systems (FMOODS) / 31th International Conference on FORmal TEchniques for Networked and Distributed Systems (FORTE), Jun 2011, Reykjavik,, Iceland. pp.334-348, ⟨10.1007/978-3-642-21461-5_22⟩ |
op_relation |
info:eu-repo/semantics/altIdentifier/doi/10.1007/978-3-642-21461-5_22 hal-01583330 https://hal.inria.fr/hal-01583330 https://hal.inria.fr/hal-01583330/document https://hal.inria.fr/hal-01583330/file/978-3-642-21461-5_22_Chapter.pdf doi:10.1007/978-3-642-21461-5_22 |
op_rights |
http://creativecommons.org/licenses/by/ info:eu-repo/semantics/OpenAccess |
op_doi |
https://doi.org/10.1007/978-3-642-21461-5_22 |
container_start_page |
334 |
op_container_end_page |
348 |
_version_ |
1766039545740001280 |