Partial Specification of Routing Configurations

The formal analysis of routing protocol configurations for safety properties is well established. Methods exist to identify potential protocol oscillations by analysis of the network topology and route preference information. However, if not all of this information is available, then the existing theory does not apply. We present an analysis of partial specification of protocol instances and apply it to eBGP and iBGP examples, so that potential oscillations can be detected from the incomplete data. This technique is applicable to the incremental design of network configurations, where some parts of the design have been specified but others are not yet known. We also anticipate that automated tools could be used to ‘fill in the blanks’ of a partial configuration in some optimal way. To that end, we show how our analysis can be used to derive constraints on an IGP weight matrix, characterizing the set of possible weights that do not lead to BGP oscillation. We propose that these integer constraints could be used as part of a link weight optimization engine, to achieve some traffic engineering goal while not violating global stability.