Preventing Timing Side-Channels via Security-Aware Just-In-Time Compilation

TL;DR

This paper introduces a formal framework and an automated method to prevent timing side-channels caused by JIT compilation, ensuring constant-time security properties in Java programs.

Contribution

It proposes a formal semantics, a sound type system, and an automated tool for eliminating JIT-induced timing leaks in constant-time programs.

Findings

DeJITLeak effectively eliminates JIT-induced leaks.

The approach is efficient on multiple datasets.

Fine-grained JIT compilation enhances security without significant performance loss.

Abstract

Recent work has shown that Just-In-Time (JIT) compilation can introduce timing side-channels to constant-time programs, which would otherwise be a principled and effective means to counter timing attacks. In this paper, we propose a novel approach to eliminate JIT-induced leaks from these programs. Specifically, we present an operational semantics and a formal definition of constant-time programs under JIT compilation, laying the foundation for reasoning about programs with JIT compilation. We then propose to eliminate JIT-induced leaks via a fine-grained JIT compilation for which we provide an automated approach to generate policies and a novel type system to show its soundness. We develop a tool DeJITLeak for Java based on our approach and implement the fine-grained JIT compilation in HotSpot. Experimental results show that DeJITLeak can effectively and efficiently eliminate JIT-induced leaks on three datasets used in side-channel detection