22 Jun 2020 - Dan Kristiansen
I Graduated from Aalborg University with the highest grade possible. Censor provided very positive feedback about the thesis itself, with room for improvements regarding the presentation.
My thesis demonstrate an approach to Shortest Trace Reachability Analysis of Weighted Pushdown Systems. The Weighted Pushdown Systems are used to model Multiprotocol Label Switching (MPLS) networks in AalWiNes. In particular we analyse MPLS networks. MPLS is a network routing technique that uses short path labels to route traffic rather than long network addresses. This avoids complex look-ups in routing tables, which makes the network traffic more flexible and faster. MPLS is used for creating fast wide area network (WAN) and virtual private networks (VPN), and can be used by network providers to quickly tunnel IP-traffic through their sub-network. The tool provides the opportunity to analyse the network under multiple failures, where a label is pushed on top of the existing labels and used to route the packet via an alternative path. When the packet arrives back on the original path, the extra label is popped.
The main contributions of this thesis are listed and explained below:
We introduced the reachability library (1) as a performance improvement to AalWiNes, that formerly used the tool Moped to perform unweighted nondeterministic PDA reachability analysis and trace generation. The implementation of the library PDAAAL allows the reachability analysis to be an integrated part of the tool, rather than an external Moped binary that introduces performance overhead when parsing. The weighted extension (2) models pushdown systems with weights, allowing for shortest trace queries using a combination of different quantitative properties of the network traces as weights. Queries can be annotated to minimize these properties, the supported properties to minimize in the trace are: number of hops, number of failures, number of tunnels, and the physical distance. A non-trivial problem is to minimize the global property of the maximum stack size during a trace (3).
The early termination check (4) is introduced as a performance improvement in the reachability algorithms of PDAAAL. The early termination check, is implemented as a constant time lookup in the current system, terminating if the goal state is already reached, rather than building the complete set of reachable states. Network manipulation (5) is a contribution to the existing AalWiNes implementation, allowing us to create large, realistic network topologies for testing. The manipulation works as an algebra for combining network topologies with concatenation and injection. Routing generation (6) create for any network topology a routing table, such that there exist label-switched paths between all pairs of routers, and fast reroute paths for all edges. If any edge in the network fails, such a fast reroute path is applied rather than the failing edge. Another performance improvements is introduced by reducing the operation sequence (7). A set of operation sequence reduction rules are defined, such that operation sequences are reduced to smaller sequences with the same behavior.
Finally we conduct an experimental evaluation to compare the performance of our implementation to Moped. The networks used in this experiment are constructed from five different network topologies from Topology Zoo, each manipulated to six different sizes, and annotated with generated routing tables. The experiment is executed on a cluster provided by Aalborg University, and include 200 instances of queries for each of the 30 different networks. The performance experiments capture the verification time of Moped and PDAAAL, and directly compare them in each test case. From the experiment can we conclude that PDAAAL outperforms the state-of-the-art tool Moped. Another experiment include the weighted extension to PDAAAL, and captures the results of verifying the same aforementioned networks and queries. The results show the improvements of annotating the system with weights, e.g. to minimize the number of links in the trace, such that the weighted extension improve the likelihood of a valid trace being found, while there is only little performance overhead of the weighted reachability algorithm.
