Title
Analyzing Internet Routing Security Using Model Checking.
Abstract
The goal of this work is to enhance Internet security by applying formal analysis of traffic attraction attacks on the BGP routing protocol. BGP is the sole protocol used throughout the Internet for inter-domain routing, hence its importance. In attraction attacks an attacker sends false routing advertisements to gain attraction of extra traffic in order to increase its revenue from customers, drop, tamper, or snoop on the packets. Such attacks are most common on the inter-domain routing. We use model checking to perform exhaustive search for attraction attacks on BGP. This requires substantial reductions due to scalability issues of the entire Internet topology. Therefore, we propose static methods to identify and automatically reduce Internet fragments of interest, prior to using model checking. We developed a method, called BGP-SA, for BGP Security Analysis, which extracts and reduces fragments from the Internet. In order to apply model checking, we model the BGP protocol and also model an attacker with predefined capabilities. Our specifications allow to reveal different types of attraction attacks. Using a model checking tool we identify attacks as well as show that certain attraction scenarios are impossible on the Internet under the modeled attacker capabilities.
Year
DOI
Venue
2015
10.1007/978-3-662-48899-7_9
LPAR
Field
DocType
Volume
Internet topology,Default-free zone,Internet security,Model checking,Computer security,Computer science,Computer network,Border Gateway Protocol,Security analysis,IP forwarding,The Internet
Conference
9450
ISSN
Citations 
PageRank 
0302-9743
1
0.35
References 
Authors
3
3
Name
Order
Citations
PageRank
Adi Sosnovich160.91
Orna Grumberg24361351.99
Gabi Nakibly317814.18