=================================================== From takhoa@rice.edu Thu Mar 11 10:37:51 2004 =================================================== This paper describes a set of rules to check for when deploying routing protocols. The rules are not that complicated, but it gives a better analysis. The rules provide a good guideline, but it's not easy to determine if an existing protocol abides by a particular rule. For example, to know if BGP satisfies progress, you have to first determine if the route reflector configuration is RR-IGP-Safe. In the paper, the authors mostly use examples and counter examples to demonstrate the case, but it's might take non-obvious case to give example of a violation. The rules are good for designing a new protocol as the authors have mentioned. If the new protocol has an abstraction layer to check these rules, then you can check for violations easier. But the concept of high-level abstraction is not new. Additionally, it's not easy to write a new high-level programming language that can test for all the rules that the authors presented. =================================================== From muhammed@ece.rice.edu Thu Mar 11 15:04:23 2004 =================================================== BGP is a basically a simple path vector protocol which guarantees loop freedom and stable routing. But due to AS routing policies and the freedom to choose a policy and the addition of more features in the updates like the MED's makes BGP more complicated to analyze and contruct formal proofs of claims. This paper proposes a logical reasoning framework which makes the procedure of checking for certain properties in a wide area routing protocol easier. It applies this framework to BGP co-operating with the intradomain routing protocols and comes up with sufficient conditions to guarantee properties like validity, safety, visibility, loop freedom etc. But none of the properties they consider has a time element in it and hence the paper cannot answer questions like "how fast is the dynamics going to stabilize after a perturbation?". Another issue is that they assume hierarchical (scope levels) routing. It is not clear how their methods apply to multihomed destinations. But the paper has a lot of practical significance in that it leads to identification of intradomain routing configurations which lead to violation of desirable properties. In contrast to subjective experimental evaluations of a routing protocol, a formal proof is an objective evaluation and more powerful. =================================================== From mittal@cs.rice.edu Thu Mar 11 18:07:23 2004 =================================================== Towards a Logic for Wide-Area Internet Routing The paper tries to build up a case for applying formal approach to the problem of understanding/improving routing protocols. It begins by motivating the reader for such an approach by listing a number of problems existing in the current implementation of BGP protocols. Then it reasons about how these problems can be identified using a theoretical analysis. The paper presents arguments for three main applications areas which can benefit from such methodology. Firstly, it can be applied to existing legacy implementations to find out if certain policies are being violated. Secondly, it could be used to find if modifications to existing implementations makes it susceptible to violations. Thirdly, it can be used in the design of new protocols. Overall, I feel this is a noble approach to cut-down all the ad-hoc behavior that categorizes existing routing protocols. It also argues for a greater effort from the developers to have a better specification of desired behavior - one that can be analyzed and argued about. =================================================== From gulati@is.rice.edu Fri Mar 12 16:48:37 2004 =================================================== Towards a Routing logic for wide area networking protocols This paper presents a framework to argue about routing protocols. The framework takes the protocol specification and protocol configuration as input and tells if the protocols satisfy certain properties. Authors also define five properties that they consider important for a routing protocol namely validity, visibility, safety, determinism and information flow control. The framework can answer questions about these properties for a protocol. Authors prove certain characteristics of BGP such as safety, determinism, information flow control using counterexamples and the routing logic. Although the routing logic is in a primitive stage right now and it does not consider issues like scalability, traffic engineering and it does not have any support for temporal reasoning, authors beleive that its a useful tool to reason about current routing protocols and developing new routing protocols. I think that the idea of formally verifying protocols is good and would save a lot of time of system designers but its a difficult problem. With the current specifications of routing logic, its not very clear how to use it. So I beleive alot of work needs to be done before any sort of logic can be used to reason about complex protocols. -Ajay =================================================== From amsaha@cs.rice.edu Sat Mar 13 16:58:49 2004 =================================================== The authors have presented a routing logic which is a set of rules which help in proving certain properties about routing protocols. With this logic (i.e. the set of rules) the authors have proven certain known 'properties' of BGP as well as some unknown properties of BGP. The authors do not provide any insight about the completeness or the soundness of the presented set of rules - can it catch all problems, will there be false triggers ? The most important thing has been left to future work and that is 'how to apply the routing logic to evaluate existing routing protocols' because if the existing ones cannot be proven wrong there is no incentive for administrators to accept a new paradigm in designing routing protocols. -Amit