一句话:提出细粒度 JIT 编译与类型系统,自动生成编译策略,消除 JIT 引入的时序侧信道泄漏。
时序侧信道可依据程序执行时间推断秘密。已有工作表明,即使程序在源代码层面满足时间平衡,JIT 编译仍可能引入新的时序侧信道。本文提出消除 JIT 引入泄漏的方法:首先用 time-balancing 概念形式化 JIT 编译下的时序侧信道安全,为推理带 JIT 的程序奠定基础;进而通过细粒度 JIT 编译消除泄漏,给出自动生成编译策略的方法,并设计类型系统保证其可靠性。作者实现面向真实 Java 的工具 DeJITLeak,并在 HotSpot JVM 中集成细粒度 JIT 编译。实验表明,在三个广泛使用的侧信道检测基准上,DeJITLeak 能有效且高效地消除 JIT 引入的泄漏。
Timing side-channels can be exploited to infer secret information when the execution time of a program is correlated with secrets. Recent work has shown that Just-In-Time (JIT) compilation can introduce new timing side-channels in programs even if they are time-balanced at the source code level. In this paper, we propose a novel approach to eliminate JIT-induced leaks. We first formalise timing side-channel security under JIT compilation via the notion of time-balancing, laying the foundation for reasoning about programs with JIT compilation. We then propose to eliminate JIT-induced leaks via a fine-grained JIT compilation. To this end, we provide an automated approach to generate compilation policies and a novel type system to guarantee its soundness. We develop a tool DeJITLeak for real-world Java and implement the fine-grained JIT compilation in HotSpot JVM. Experimental results show that DeJITLeak can effectively and efficiently eliminate JIT-induced leaks on three widely adopted benchmarks in the setting of side-channel detection.