paperbot · PL 论文追踪

全部论文 待读 收藏

P2 DeJITLeak: eliminating JIT-induced timing side-channel leaks

DeJITLeak:消除 JIT 引入的时序侧信道泄漏
FSE Proceedings of the 30th ACM Joint European Software Engineering Conference and Symposium on the Foundations of Software Engineering2022匹配度 2/10 · 论文聚焦 JIT 编译引入的时序侧信道,通过形式化时间平衡、类型系统与 HotSpot JVM 实现来消除泄漏,属于 PL/编译/安全方向;它不涉及 LLM/Agent 与静态分析/形式化验证的交叉,也不涉及浮点程序分析或贝叶斯程序分析,因此与用户核心研究方向仅有较弱的 PL 形式化与工程实现偏好上的关联。引用 18 inbox
Qi Qin, JulianAndres JiYang, Fu Song, Taolue Chen, Xinyu Xing
crossref: 2026-09-12

AI 速览

一句话:提出细粒度 JIT 编译与类型系统,自动生成编译策略,消除 JIT 引入的时序侧信道泄漏。

时序侧信道可依据程序执行时间推断秘密。已有工作表明,即使程序在源代码层面满足时间平衡,JIT 编译仍可能引入新的时序侧信道。本文提出消除 JIT 引入泄漏的方法:首先用 time-balancing 概念形式化 JIT 编译下的时序侧信道安全,为推理带 JIT 的程序奠定基础;进而通过细粒度 JIT 编译消除泄漏,给出自动生成编译策略的方法,并设计类型系统保证其可靠性。作者实现面向真实 Java 的工具 DeJITLeak,并在 HotSpot JVM 中集成细粒度 JIT 编译。实验表明,在三个广泛使用的侧信道检测基准上,DeJITLeak 能有效且高效地消除 JIT 引入的泄漏。

问题
JIT 编译可能破坏源码层面的时间平衡,从而引入新的时序侧信道并泄露秘密;如何形式化并消除这类 JIT 引入的泄漏是核心问题。
方法
用 time-balancing 形式化 JIT 下的时序侧信道安全,提出细粒度 JIT 编译,并自动生成编译策略,用类型系统保证策略可靠性;在 HotSpot JVM 上实现 DeJITLeak。
评估
在三个广泛使用的侧信道检测基准上对真实 Java 程序进行评估,验证 DeJITLeak 消除 JIT 引入泄漏的有效性与效率。
原文摘要(Abstract)

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.

链接与引用

DOI 原文 · PDF(开放获取) ·

BibTeX
@inproceedings{paperbot6985,
  title = {DeJITLeak: eliminating JIT-induced timing side-channel leaks},
  author = {Qi Qin and JulianAndres JiYang and Fu Song and Taolue Chen and Xinyu Xing},
  booktitle = {FSE},
  year = {2022},
  doi = {10.1145/3540250.3549150}
}