Principled Unearthing of TCP Side Channel Vulnerabilities
Principled Unearthing of TCP Side Channel Vulnerabilities
复制标题
DOI：
10.1145/3319535.3354250
复制
发表时间：
2019-11
期刊：
影响因子：
--
通讯作者：
Yue Cao;Zhongjie Wang;Zhiyun Qian;Chengyu Song;S. Krishnamurthy;Paul L. Yu
中科院分区：
文献类型：
--
作者：
Yue Cao;Zhongjie Wang;Zhiyun Qian;Chengyu Song;S. Krishnamurthy;Paul L. Yu
最近的工作展示了现代操作系统中存在微妙的 TCP 侧通道，这些侧通道可以被偏离路径的对手利用来发起恶意攻击，例如劫持连接。不幸的是，迄今为止的大多数工作都是手动发现此类侧通道，并随后对其进行修补。在这项工作中，我们问“我们能否开发出一种原则性的方法来自动发现这种难以找到的 TCP 侧通道？”我们发现这种侧通道存在的关键在于违反了同时 TCP 连接之间的不干扰特性，即存在这样的情况：一个连接的状态变化会隐式地将一些信息泄漏到另一个连接（可能由攻击者控制）。为了发现这种不干扰属性的违规行为，我们认为模型检查是一个自然的选择。然而，由于其可扩展性的限制，模型检查的使用存在许多挑战。具体来说，这些挑战涉及 (a) 使 TCP 代码库独立并易于模型检查，以及 (b) 限制模型检查的搜索空间并实现合理的代码覆盖水平。我们开发了一种称为 SCENT（侧通道挖掘工具）的工具，它以自动化的方式解决这些挑战。 SCENT 的核心是一个自动缩减组件，它以一致的方式转换 TCP 代码库，以降低模型检查器遇到的状态空间复杂性以及验证所需的输入数量和类型。我们的广泛评估表明，SCENT 导致在 Linux 和 FreeBSD 内核中发现了 12 个新的侧通道漏洞。特别是，对一类漏洞的现实验证表明，平均而言，偏离路径的攻击者能够在略多于 1 分钟的时间内推断出两个任意主机是否正在相互通信。
Recent work has showcased the presence of subtle TCP side channels in modern operating systems, that can be exploited by off-path adversaries to launch pernicious attacks such as hijacking a connection. Unfortunately, most work to date is on the manual discovery of such side-channels, and patching them subsequently. In this work we ask "Can we develop a principled approach that can lead to the automated discovery of such hard-to-find TCP side-channels?" We identify that the crux of why such side-channels exist is the violation of the non-interference property between simultaneous TCP connections i.e., there exist cases wherein a change in state of one connection implicitly leaks some information to a different connection (controlled possibly by an attacker). To find such non-interference property violations, we argue that model-checking is a natural fit. However, because of limitations with regards to its scalability, there exist many challenges in using model checking. Specifically, these challenges relate to (a) making the TCP code base self-contained and amenable to model checking and (b) limiting the search space of model checking and yet achieving reasonable levels of code coverage. We develop a tool that we call SCENT (for Side Channel Excavation Tool) that addresses these challenges in a mostly automated way. At the heart of SCENT is an automated downscaling component that transforms the TCP code base in a consistent way to achieve both a reduction in the state space complexity encountered by the model checker and the number and types of inputs needed for verification. Our extensive evaluations show that SCENT leads to the discovery of 12 new side channel vulnerabilities in the Linux and FreeBSD kernels. In particular, a real world validation with one class of vulnerabilities shows that an off-path attacker is able to infer whether two arbitrary hosts are communicating with each other, within slightly more than 1 minute, on average.