一句话：提出输出敏感非干扰与类型系统，验证泄漏变量泄露不超过公开输出。
常量时间编程通过禁止依赖秘密的内存访问来抵御缓存攻击，但该策略在程序泄露不超过公开输出时可安全放松。本文提出输出敏感非干扰这一新的信息流性质：将变量划分为输入、输出和泄漏变量，要求泄漏变量关于秘密输入所泄露的信息不超过正常的公开输出。作者设计类型系统进行静态检查，其新颖之处在于同时跟踪泄漏变量对输入变量初始值和对输出变量最终值的依赖。该方法被适配到 LLVM IR，并实现了原型工具来验证 LLVM 实现。
Constant-time programming is a countermeasure to prevent cache based attacks where programs should not perform memory accesses that depend on secrets. In some cases this policy can be safely relaxed if one can prove that the program does not leak more information than the public outputs of the computation. We propose a novel approach for verifying constant-time programming based on a new information flow property, called output-sensitive noninterference. Noninterference states that a public observer cannot learn anything about the private data. Since real systems need to intentionally declassify some information, this property is too strong in practice. In order to take into account public outputs we proceed as follows: instead of using complex explicit declassification policies, we partition variables in three sets: input, output and leakage variables. Then, we propose a typing system to statically check that leakage variables do not leak more information about the secret inputs than the public normal output. The novelty of our approach is that we track the dependence of leakage variables with respect not only to the initial values of input variables (as in classical approaches for noninterference), but taking also into account the final values of output variables. We adapted this approach to LLVM IR and we developed a prototype to verify LLVM implementations.
@article{paperbot1336,
title = {Output-sensitive Information flow analysis},
author = {Cristian Ene and Laurent Mounier and Marie-Laure Potet},
journal = {Logical Methods in Computer Science},
volume = {Volume 17, Issue 1},
year = {2021},
doi = {10.23638/lmcs-17(1:15)2021}
}