BliMe Linter
Hossam ElAtali, Xiaohe Duan, Hans Liljestrand, Meng Xu, N. Asokan
TL;DR
The paper tackles confidentiality risks in outsourced computation by leveraging BliMe hardware, which enforces a taint-tracking policy to prevent secret-dependent leaks. It introduces the BliMe linter, a compiler-based tool built on SVF that analyzes LLVM bitcode and flags potential BliMe violations using a static taint-tracking approach that mirrors hardware behavior. Through evaluations on OISA benchmarks and TensorFlow Lite, the authors demonstrate the linter’s ability to identify real violations and discuss limitations related to scalability and precision, proposing function cloning and future automatic transformations as directions. The work advances practical security tooling for data-oblivious execution, offering a path toward safer deployment of outsourced computation with a focus on static analysis, taint propagation, and program transformations.
Abstract
Outsourced computation presents a risk to the confidentiality of clients' sensitive data since they have to trust that the service providers will not mishandle this data. Blinded Memory (BliMe) is a set of hardware extensions that addresses this problem by using hardware-based taint tracking to keep track of sensitive client data and enforce a security policy that prevents software from leaking this data, either directly or through side channels. Since programs can leak sensitive data through timing channels and memory access patterns when this data is used in control-flow or memory access instructions, BliMe prohibits such unsafe operations and only allows constant-time code to operate on sensitive data. The question is how a developer can confirm that their code will run correctly on BliMe. While a program can be manually checked to see if it is constant-time, this process is tedious and error-prone. In this paper, we introduce the BliMe linter, a set of compiler extensions built on top of SVF that analyze LLVM bitcode to identify possible BliMe violations. We evaluate the BliMe linter analytically and empirically and show that it is sound.