Analyzing Internet Routing Security Using Model Checking
Analyzing Internet Routing Security Using Model Checking
复制标题
使用模型检查分析 Internet 路由安全
DOI：
--
复制
发表时间：
2015
期刊：
影响因子：
--
通讯作者：
Gabi Nakibly
中科院分区：
文献类型：
--
作者：
Adi Sosnovich;O. Grumberg;Gabi Nakibly
这项工作的目标是通过对 BGP 路由协议上的流量吸引攻击进行形式化分析来增强互联网安全性。 BGP 是整个 Internet 中用于域间路由的唯一协议，因此非常重要。在吸引攻击中，攻击者发送虚假路由广告来吸引额外流量，从而增加来自客户的收入，丢弃、篡改或窥探数据包。此类攻击在域间路由上最常见。
我们使用模型检查来对 BGP 上的吸引力攻击进行详尽的搜索。由于整个互联网拓扑的可扩展性问题，这需要大幅减少。因此，我们提出了在使用模型检查之前识别并自动减少感兴趣的互联网片段的静态方法。
我们开发了一种称为 BGP-SA 的方法用于 BGP 安全分析，该方法可以从互联网中提取并减少碎片。为了应用模型检查，我们对 BGP 协议进行建模，并对具有预定义功能的攻击者进行建模。我们的规范允许揭示不同类型的吸引攻击。使用模型检查工具，我们可以识别攻击，并表明在建模的攻击者能力下，某些吸引场景在互联网上是不可能的。
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.