2025-11-10T03:00:57.254697

Decompiling for Constant-Time Analysis

Arranz-Olmos, Barthe, Blatter et al.

Cryptographic libraries are a main target of timing side-channel attacks. A practical means to protect against these attacks is to adhere to the constant-time (CT) policy. However, it is hard to write constant-time code, and even constant-time code can be turned vulnerable by mainstream compilers. So how can we verify that binary code is constant-time? The obvious answer is to use binary-level CT tools. To do so, a common approach is to use decompilers or lifters as a front-end for CT analysis tools operating on source code or IR. Unfortunately, this approach is problematic with current decompilers. To illustrate this fact, we use the recent Clangover vulnerability and other constructed examples to show that five popular decompilers eliminate CT violations, rendering them not applicable with the approach. In this paper, we develop foundations to asses whether a decompiler is fit for the Decompile-then-Analyze approach. We propose CT transparency, which states that a transformation neither eliminates nor introduces CT violations, and a general method for proving that a program transformation is CT transparent. Then, we build CT-RetDec, a CT analysis tool based on a modified version of the LLVM-based decompiler RetDec. We evaluate CT-RetDec on a benchmark of real-world vulnerabilities in binaries, and show that the modifications had significant impact on CT-RetDec's performance. As a contribution of independent interest, we found that popular tools for binary-level CT analysis rely on decompiler-like transformations before analysis. We show that two such tools employ transformations that are not CT transparent, and, consequently, that they incorrectly accept non-CT programs. While our examples are very specific and do not invalidate the general approach of these tools, we advocate that tool developers counter such potential issues by proving the transparency of such transformations.

academic

상수 시간 분석을 위한 디컴파일링

기본 정보

논문 ID: 2501.04183
제목: Decompiling for Constant-Time Analysis
저자: Santiago Arranz-Olmos (MPI-SP), Gilles Barthe (MPI-SP & IMDEA), Lionel Blatter (MPI-SP), Youcef Bouzid (ENS Paris-Saclay), Sören van der Wall (TU Braunschweig), Zhiyuan Zhang (MPI-SP)
분류: cs.PL (프로그래밍 언어)
발표 시간: 2025년 1월 (arXiv 사전 인쇄본)
논문 링크: https://arxiv.org/abs/2501.04183

초록

암호화 라이브러리는 타이밍 사이드 채널 공격의 주요 대상입니다. 이러한 공격으로부터의 방어 방법은 상수 시간(CT) 전략을 준수하는 것입니다. 그러나 상수 시간 코드를 작성하기는 어렵고, 상수 시간 소스 코드도 주류 컴파일러에 의해 취약한 바이너리 코드로 변환될 수 있습니다. 본 논문은 바이너리 코드가 상수 시간 요구 사항을 만족하는지 검증하는 방법을 연구합니다. 일반적인 방법은 디컴파일러를 프론트엔드로 사용하여 바이너리 코드를 소스 코드 또는 중간 표현으로 변환한 후 기존 CT 분석 도구를 적용하는 것입니다. 불행하게도, 이러한 "디컴파일-분석" 방법에는 문제가 있습니다. 본 논문은 Clangover 취약점 등의 사례를 통해 5가지 인기 있는 디컴파일러가 모두 CT 위반을 제거하여 분석 결과를 신뢰할 수 없게 만든다는 것을 증명합니다.

연구 배경 및 동기

문제 배경

타이밍 사이드 채널 공격 위협: 암호화 구현은 타이밍 사이드 채널 공격에 취약하며, 공격자는 프로그램 실행 시간을 관찰하여 비밀 정보를 추론할 수 있습니다
상수 시간 전략: CT 전략은 프로그램 실행 시간이 비밀 입력에 의존하지 않아야 하며, 비밀에 의존하는 메모리 접근 및 분기 점프를 실행하지 않아야 합니다
컴파일러 보안 결함: 주류 컴파일러의 최적화는 안전한 소스 코드를 CT 위반이 있는 바이너리 코드로 컴파일할 수 있습니다

핵심 문제

기존의 "디컴파일-분석" 방법에는 근본적인 결함이 있습니다: 디컴파일러는 변환 과정에서 CT 위반을 제거할 수 있으므로, 분석 도구가 취약한 바이너리 코드를 잘못되게 안전하다고 판단할 수 있습니다.

연구 동기

실제 필요성: 바이너리 코드에 대한 CT 분석이 필요하지만 기존 도구는 주로 소스 코드를 대상으로 합니다
방법 결함: 디컴파일러를 프론트엔드로 사용하는 현재 방법은 신뢰할 수 없습니다
이론 부재: 프로그램 변환이 CT 분석에 적합한지 평가하는 이론적 프레임워크가 부족합니다

핵심 기여

문제 발견 및 증명: Clangover 등의 사례를 통해 5가지 주류 디컴파일러가 모두 CT 위반을 제거하여 분석 결과를 신뢰할 수 없게 만든다는 것을 증명합니다
CT 투명성 이론 제시: CT 투명성 개념을 형식화하여 정의합니다. 즉, 프로그램 변환이 CT 위반을 제거하지도 도입하지도 않습니다
증명 기법 개발: 프로그램 변환의 CT 투명성을 증명하기 위한 시뮬레이션 기반 범용 방법을 제시합니다
실용 도구 구축: 수정된 RetDec 디컴파일러를 기반으로 하는 CT-RetDec 도구를 개발하여 신뢰할 수 있는 바이너리 CT 분석을 수행합니다
도구 결함 발견: 기존 CT 분석 도구(CT-Verif 및 BinSec)가 내부적으로 사용하는 변환도 투명하지 않으며 보안 결함이 있음을 증명합니다

반사성(Reflection): $\llbracket P \rrbracket$ 이 φ-CT이면 P는 φ-CT입니다
보존성(Preservation): P가 φ-CT이면 $\llbracket P \rrbracket$ 은 φ-CT입니다
투명성(Transparency): 반사성과 보존성을 동시에 만족합니다

시뮬레이션 기법

잠금 단계 시뮬레이션과 완화된 시뮬레이션 두 가지 방법을 채택합니다:

잠금 단계 시뮬레이션: 출력 프로그램의 각 단계가 입력 프로그램의 한 단계에 대응됩니다

시뮬레이션 관계: $s \sim t$
관찰 변환기: $T : O_s \to O_t$
핵심 조건: T는 단사 함수여야 합니다

완화된 시뮬레이션: 입력 및 출력 프로그램이 다른 단계 수로 실행되도록 허용합니다

단계 함수: $ns : PC \to \mathbb{N}_{>0}$
접미사 함수: $sf : PC \to O_s^*$
PC 단사성: 각 프로그램 포인트에서 관찰 변환기는 단사 함수입니다

기술 혁신점

PC 단사성 개념: 각 프로그램 포인트에서 관찰 변환기가 단사 함수임을 요구하여 기존 CT 보존 기법을 확장합니다
통합 프레임워크: 여러 프로그램 변환을 동일한 이론적 프레임워크 하에서 분석합니다
실용성 지향: 이론 분석뿐만 아니라 실제 사용 가능한 도구를 개발합니다

실험 설정

데이터 세트

디컴파일러 테스트: Clangover 취약점 및 구성된 최소 반례를 사용하여 5가지 디컴파일러를 테스트합니다
벤치마크 세트: 160개의 바이너리 프로그램(10가지 알려진 타이밍 사이드 채널 취약점 포함)
- 컴파일러: Clang 10/14/18/21
- 최적화 수준: -O0, -Os
- 아키텍처: x86-32, x86-64