ObliCheck: Efficient Verification of Oblivious Algorithms with Unobservable State
ObliCheck: Efficient Verification of Oblivious Algorithms with Unobservable State
复制标题
DOI：
--
复制
发表时间：
2021
期刊：
影响因子：
--
通讯作者：
Jeongseok Son;G. Prechter;Rishabh Poddar;Raluca A. Popa;Koushik Sen
中科院分区：
文献类型：
--
作者：
Jeongseok Son;G. Prechter;Rishabh Poddar;Raluca A. Popa;Koushik Sen
对机密数据进行加密可防止对手通过观察传输的数据来获取敏感信息。然而，即使数据本身已加密，攻击者仍可观察内存、磁盘和网络的哪些位置被访问，并推断出大量机密信息。为了防范基于这种访问模式泄露的攻击，人们已经设计了许多不经意算法。这些算法以一种访问序列与机密输入数据无关的方式改变访问模式。由于不经意算法往往速度较慢，算法设计者常用的一种优化方法是利用攻击者无法观察到的空间。然而，在这个过程中，人们很容易忽略一个细微的细节，从而违反不经意特性。在本文中，我们提出了ObliCheck，一种用于验证给定算法是否确实具有不经意特性的检查器。与现有的检查器不同，ObliCheck区分算法的可观察状态和不可观察状态。它采用符号执行来检查所有执行路径是否表现出相同的可观察行为。为了实现准确性和高效性，ObliCheck引入了两项关键技术：乐观状态合并，用于快速检查算法是否具有不经意特性；迭代状态拆分，如果算法被报告为不具有不经意特性，则用于迭代地细化其判断。ObliCheck在不牺牲准确性的情况下，相较于传统的符号执行实现了4850倍的性能提升。
Encryption of secret data prevents an adversary from learning sensitive information by observing the transferred data. Even though the data itself is encrypted, however, an attacker can watch which locations of the memory, disk, and network are accessed and infer a significant amount of secret information. To defend attacks based on this access pattern leakage, a number of oblivious algorithms have been devised. These algorithms transform the access pattern in a way that the access sequences are independent of the secret input data. Since oblivious algorithms tend to be slow, a go-to optimization for algorithm designers is to leverage space unobservable to the attacker . However, one can easily miss a subtle detail and violate the oblivious property in the process of doing so. In this paper, we propose ObliCheck, a checker verifying whether a given algorithm is indeed oblivious. In contrast to existing checkers, ObliCheck distinguishes observable and unobservable state of an algorithm. It employs symbolic execution to check whether all execution paths exhibit the same observable behavior. To achieve accuracy and efficiency, ObliCheck introduces two key techniques: Optimistic State Merging to quickly check if the algorithm is oblivious, and Iterative State Unmerging to iteratively refine its judgment if the algorithm is reported as not oblivious. ObliCheck achieves × 4850 of performance improvement over conventional symbolic execution without sacrificing accuracy.