diff --git a/core/constant-time/standard.md b/core/constant-time/standard.md new file mode 100644 index 0000000..0e42ac5 --- /dev/null +++ b/core/constant-time/standard.md @@ -0,0 +1,378 @@ +# 상수-시간 연산 표준 명세 + +> **크레이트**: `entlib-native-constant-time` +> **대상 플랫폼**: `x86_64`, `aarch64` (no_std) + +--- + +## 1. 설계 목표 및 위협 모델 + +### 위협 모델 + +이 크레이트가 방어하는 공격 유형은 다음과 같다. + +| 공격 유형 | 설명 | 방어 수단 | +|------------------------------------------|------------------------------------|-----------------------------------| +| **타이밍 공격 (Timing Attack)** | CPU 실행 시간 측정을 통한 비밀 데이터 추론 | 조건 분기 제거, 비트 마스크 연산 | +| **분기 예측 공격 (Branch Prediction Attack)** | CPU 파이프라인 미스 예측 패턴으로 비밀 데이터 추론 | `black_box`로 LLVM SELECT 노드 생성 차단 | +| **컴파일러 역최적화 (Compiler De-optimization)** | LLVM InstCombine이 비트 연산을 조건 분기로 치환 | 중간 산출물 `black_box` 적용 위치 엄격 관리 | +| **캐시 타이밍 공격 (Cache Timing Attack)** | 메모리 접근 패턴 측정을 통한 비밀 데이터 추론 | 데이터 독립적 메모리 접근 패턴 보장 | + +### 상수-시간(Constant-Time)의 수학적 정의 + +두 개의 비밀 입력 $s_1$, $s_2$에 대해 프로그램의 관측 가능한 실행 궤적(Execution Trace)을 $\tau(s_1)$, $\tau(s_2)$라 하면, 상수-시간 조건은 다음과 같다. + +$$\forall s_1, s_2 \in \mathcal{S} : \tau(s_1) = \tau(s_2)$$ + +여기서 관측 가능한 실행 궤적 $\tau$는 다음 요소를 포함한다. + +- 실행된 명령어 시퀀스 (제어 흐름) +- 메모리 읽기/쓰기 주소 시퀀스 +- 총 실행 사이클 수 + +--- + +## 2. `Choice` 타입 — 상수-시간 불리언 + +### 불변 조건 (Invariant) + +``` +Choice ∈ {0x00, 0xFF} +``` + +`Choice(u8)` 내부 필드는 반드시 두 값 중 하나만 허용된다. 이 불변 조건이 유지될 때, 비트 연산은 논리 연산과 수학적으로 동치이다. + +| 값 | 의미 | 논리 연산 동치 | +|--------|-------|-------------------------------------------| +| `0x00` | False | `0 & x = 0`, `0 \| x = x`, `!0x00 = 0xFF` | +| `0xFF` | True | `F & x = x`, `F \| x = F`, `!0xFF = 0x00` | + +### 구조 + +```rust +#[derive(Clone, Copy, Debug)] +#[repr(transparent)] +pub struct Choice(u8); +``` + +`#[repr(transparent)]`는 `u8`과 동일한 메모리 레이아웃을 보장하며, FFI 경계에서 단일 바이트로 취급된다. + +### 생성자 + +| 생성자 | 조건 | 설명 | +|----------------------------------|-----------------------|-------------------------------------------------| +| `from_mask(mask: u8)` | `mask ∈ {0x00, 0xFF}` | 정규화된 마스크 직접 구성. 호출자가 불변 조건을 보장해야 한다. | +| `from_mask_normalized(mask: u8)` | 임의 `u8` | 임의 바이트를 `0x00`/`0xFF`로 정규화. `audit_mode` 피처 한정. | + +#### `from_mask_normalized` 정규화 수식 + +임의 바이트 $m$에 대해: + +$$\text{msb\_set} = m \mid (-m)$$ +$$\text{is\_nonzero} = \text{msb\_set} \gg 7$$ +$$\text{result} = -\text{is\_nonzero}$$ + +$m = 0$이면 $\text{result} = 0\text{x00}$, $m \neq 0$이면 $\text{result} = 0\text{xFF}$. + +### 비트 연산 진리표 + +`Choice`에 대한 비트 연산은 논리 연산과 동치이며, 모두 단일 CPU 명령어(AND, OR, XOR, NOT)로 컴파일된다. + +| 연산 | A | B | 결과 | +|-----------|--------|--------|--------| +| AND (`&`) | `0xFF` | `0xFF` | `0xFF` | +| AND (`&`) | `0xFF` | `0x00` | `0x00` | +| AND (`&`) | `0x00` | `0x00` | `0x00` | +| OR (`\|`) | `0xFF` | `0x00` | `0xFF` | +| OR (`\|`) | `0x00` | `0x00` | `0x00` | +| XOR (`^`) | `0xFF` | `0xFF` | `0x00` | +| XOR (`^`) | `0xFF` | `0x00` | `0xFF` | +| NOT (`!`) | `0xFF` | — | `0x00` | +| NOT (`!`) | `0x00` | — | `0xFF` | + +--- + +## 3. 트레이트 명세 + +### `ConstantTimeEq` + +```rust +fn ct_eq(&self, other: &Self) -> Choice; +fn ct_ne(&self, other: &Self) -> Choice; // 기본 구현: !ct_eq +fn ct_is_ge(&self, other: &Self) -> Choice; +``` + +#### `ct_eq` — 동일성 비교 + +**사전 조건**: 없음 +**사후 조건**: `self == other` iff 반환값 `== 0xFF` + +**부호 없는 정수 구현 (u8, u16, u32, u64, u128, usize)**: + +$$v = A \oplus B$$ +$$\text{msb} = (v \mid -v) \gg (\text{BITS} - 1)$$ +$$\text{mask} = -(\text{msb as u8} \oplus 1)$$ + +$v = 0$ (동일) 이면 $\text{msb} = 0$, $\text{mask} = 0\text{xFF}$. +$v \neq 0$ (상이) 이면 $\text{msb} = 1$, $\text{mask} = 0\text{x00}$. + +**`black_box` 적용 위치**: + +```rust +let v = core::hint::black_box(*self ^ *other); +let msb = (v | v.wrapping_neg()) >> (<$t>::BITS - 1); +``` + +`v`에 `black_box`를 적용하는 것이 핵심이다. LLVM InstCombine은 `(v | -v) >> (BITS-1)` 패턴을 `ICMP NE(v, 0)`으로 인식하여 `JNE`/`JE` 조건 분기로 치환한다. `v`를 opaque하게 만들면 컴파일러가 `v`의 기원을 추적할 수 없으므로 패턴 매칭이 불가능해진다. + +**`black_box`를 최종 mask에 적용하면 안 되는 이유**: LLVM은 실행 순서가 아닌 논리적 AST 구조를 먼저 분석한다. `black_box(mask)`는 LLVM이 이미 ICMP 노드를 생성한 이후에 개입하므로 효과가 없다. + +**부호 있는 정수 구현 (i8, i16, i32, i64, i128, isize)**: + +비트 패턴 비교로 위임한다. 부호 없는 정수로 캐스팅하여 산술 시프트(SAR) 취약점을 회피한다. + +```rust +let a = *self as $u_type; +let b = *other as $u_type; +a.ct_eq(&b) +``` + +#### `ct_is_ge` — 대소 비교 (≥) + +**사전 조건**: 없음 +**사후 조건**: `self >= other` iff 반환값 `== 0xFF` + +**부호 없는 정수 구현**: 빌림(Borrow) 방정식을 사용한다. + +$$\text{sub} = A - B \pmod{2^n}$$ +$$\text{borrow} = (\lnot A \land B) \mid (\lnot(A \oplus B) \land \text{sub})$$ +$$\text{borrow\_msb} = \text{borrow} \gg (\text{BITS} - 1)$$ +$$\text{mask} = -(\text{borrow\_msb} \oplus 1)$$ + +$A \geq B$이면 빌림이 없으므로 $\text{borrow\_msb} = 0$, $\text{mask} = 0\text{xFF}$. +$A < B$이면 빌림이 발생하므로 $\text{borrow\_msb} = 1$, $\text{mask} = 0\text{x00}$. + +**`black_box` 적용 위치**: + +```rust +let borrow = core::hint::black_box((!*self & *other) | (!(*self ^ *other) & sub)); +let borrow_msb = (borrow >> (<$t>::BITS - 1)) as u8; +``` + +LLVM은 위 빌림 공식 전체를 `ICMP ULT(A, B)` (Unsigned Less Than)로 인식한다. `borrow` 전체를 opaque하게 만들면 이후 `(opaque >> BITS-1)`은 패턴 매칭 불가 상태가 된다. + +**부호 있는 정수 구현**: 2의 보수 부호 비트 반전 기법을 사용한다. + +$$\text{sign\_mask} = 1 \ll (\text{BITS} - 1)$$ +$$A' = (A \text{ as unsigned}) \oplus \text{sign\_mask}$$ +$$B' = (B \text{ as unsigned}) \oplus \text{sign\_mask}$$ +$$\text{result} = A'\text{.ct\_is\_ge}(B')$$ + +MSB를 반전하면 값의 수학적 대소 순서를 보존하면서 부호 없는 도메인으로 안전하게 매핑된다. + +### `ConstantTimeSelect` + +```rust +fn ct_select(a: &Self, b: &Self, choice: Choice) -> Self; +``` + +**사전 조건**: `choice ∈ {0x00, 0xFF}` +**사후 조건**: `choice == 0xFF` → `a` 반환, `choice == 0x00` → `b` 반환 + +**구현**: 부호 확장(Sign-Extension) 트릭 + +$$\text{mask} = (\text{choice as i8}) \text{ as } T$$ +$$\text{result} = (a \land \text{mask}) \mid (b \land \lnot\text{mask})$$ + +`0xFF as i8 = -1`이므로, `T`로 부호 확장하면 모든 비트가 1인 `0xFFFF...`가 된다. +`0x00 as i8 = 0`이므로, `T`로 확장하면 모든 비트가 0인 `0x0000...`가 된다. + +### `ConstantTimeSwap` + +```rust +fn ct_swap(a: &mut Self, b: &mut Self, choice: Choice); +``` + +**사전 조건**: `choice ∈ {0x00, 0xFF}` +**사후 조건**: `choice == 0xFF` → `a`와 `b` 교환, `choice == 0x00` → 원래 값 유지 + +**구현**: 마스크된 XOR 스왑 + +$$\text{mask} = (\text{choice as i8}) \text{ as } T$$ +$$t = (a \oplus b) \land \text{mask}$$ +$$a' = a \oplus t, \quad b' = b \oplus t$$ + +`mask = 0xFFFF...`이면 $t = a \oplus b$로 표준 XOR 스왑이 수행된다. +`mask = 0x0000...`이면 $t = 0$으로 값이 변경되지 않는다. + +Montgomery Ladder와 같은 암호학적 알고리즘의 조건부 스왑에 사용된다. + +### `ConstantTimeIsZero` + +```rust +fn ct_is_zero(&self) -> Choice; +``` + +**구현**: `self.ct_eq(&0)`으로 위임. + +### `ConstantTimeIsNegative` + +```rust +fn ct_is_negative(&self) -> Choice; +``` + +**사전 조건**: 없음 +**사후 조건**: MSB = 1 iff 반환값 `== 0xFF` + +**구현**: + +$$\text{msb} = (A \gg (\text{BITS} - 1)) \text{ as u8} \land 1$$ +$$\text{mask} = -\text{msb}$$ + +`msb = 1`이면 $\text{mask} = 0\text{xFF}$, `msb = 0`이면 $\text{mask} = 0\text{x00}$. + +단일 우측 시프트(SHR) 명령어만 사용하므로 LLVM이 패턴 매칭할 대상이 없다. `black_box`는 MSB 추출 직후에 적용된다. + +**부호 있는 정수**: 산술 시프트(SAR)의 구현 정의 동작(Implementation-Defined Behavior)을 회피하기 위해 부호 없는 정수로 캐스팅 후 논리 시프트를 수행한다. + +```rust +let u_val = *self as $u_type; +let msb = core::hint::black_box((u_val >> (<$s_type>::BITS - 1)) as u8 & 1u8); +``` + +--- + +## 4. LLVM InstCombine 방어 전략 + +### 문제: LLVM의 패턴 인식과 역최적화 + +LLVM InstCombine 패스는 실행 순서가 아니라 **논리적 AST 구조**를 분석한다. 다음 패턴들이 자동으로 조건 분기로 치환된다. + +| 비트 연산 패턴 | LLVM 인식 결과 | 생성 명령어 | +|---------------------------------------|------------------|--------------| +| `(v \| v.wrapping_neg()) >> (BITS-1)` | `ICMP NE(v, 0)` | `JNE` / `JE` | +| `(!A & B) \| (!(A^B) & (A-B))` | `ICMP ULT(A, B)` | `JB` / `JAE` | + +조건 분기가 비밀 데이터에 의존하면, 두 입력 클래스(동일/상이)가 CPU 파이프라인에서 서로 다른 실행 경로를 밟게 된다. 50% 미스 예측률에서 파이프라인 플러시로 인해 수십 사이클의 타이밍 차이가 발생한다. + +### 해결: 패턴 입력에 `black_box` 적용 + +`core::hint::black_box`는 컴파일러에 대한 불투명 경계(Opaque Barrier)로, `black_box(x)`의 반환값이 `x`와 동일하지만 컴파일러가 `x`의 기원을 추적하지 못하게 한다. + +**핵심 원칙**: `black_box`는 LLVM이 인식할 패턴의 **입력값**에 적용해야 한다. 패턴의 **출력(mask)** 에 적용하면 LLVM이 이미 ICMP 노드를 생성한 이후이므로 효과가 없다. + +| 연산 | `black_box` 적용 대상 | 차단 효과 | +|------------------|---------------------------------------|---------------------------------------| +| `ct_eq` | `v = *self ^ *other` | `(v \| -v) >> BITS-1` → ICMP NE 인식 불가 | +| `ct_is_ge` | `borrow = (!A & B) \| (!(A^B) & sub)` | `borrow >> BITS-1` → ICMP ULT 인식 불가 | +| `ct_is_negative` | `msb = (val >> BITS-1) as u8 & 1u8` | 단일 SHR — 패턴 없음, 예방적 적용 | + +--- + +## 5. 지원 타입 + +| 부호 없는 정수 | 부호 있는 정수 | +|--------------------------------------------|--------------------------------------------| +| `u8`, `u16`, `u32`, `u64`, `u128`, `usize` | `i8`, `i16`, `i32`, `i64`, `i128`, `isize` | + +부호 있는 정수의 `ct_eq`/`ct_is_zero`/`ct_is_negative`/`ct_select`/`ct_swap`은 부호 없는 정수 구현으로 위임한다. +`ct_is_ge`는 MSB 반전을 통한 도메인 변환 후 위임한다. + +--- + +## 6. 피처 플래그 + +| 피처 | 설명 | +|------------------------|-----------------------------------------------------------------------------------| +| `default` | 프로덕션 모드. `black_box` 최적화 방어 활성화. | +| `audit_mode` | `from_mask_normalized` 공개. `wrapper.rs`의 `#[no_mangle]` 감사 심볼 노출. | +| `saw_verify` | `audit_mode` 포함. `unwrap_u8`에서 `black_box`를 우회하여 SAW 기호 실행이 값을 추적할 수 있도록 한다. | +| `valgrind_taint_audit` | Valgrind Memcheck의 오염 추적(Taint Tracking)으로 비밀 데이터가 조건 분기에 영향을 주는지 검증한다. Linux 한정. | + +--- + +## 7. 검증 체계 + +상수-시간 보장은 세 가지 독립적인 방법으로 검증된다. + +### 7.1 정형 검증 — SAW + Cryptol + Z3 + +Galois Software Analysis Workbench(SAW)를 사용하여 Rust LLVM 비트코드와 Cryptol 참조 명세 간의 기능적 동치성을 SMT 솔버(Z3)로 수학적으로 증명한다. + +**검증 범위** (`saw/verify.saw`): + +| 페이즈 | 대상 | 수 | +|---------|---------------------------|-----| +| Phase 1 | Cryptol 명세 속성 증명 | 14개 | +| Phase 2 | LLVM 비트코드 ↔ Cryptol 동치 증명 | 10개 | + +**Cryptol 속성 목록**: + +``` +from_mask_is_boolean : ∀m. from_mask(m) ∈ {0x00, 0xFF} +ct_eq_correct : (A = B) ↔ (ct_eq(A, B) = 0xFF) +ct_eq_reflexive : ct_eq(A, A) = 0xFF +ct_eq_symmetric : ct_eq(A, B) = ct_eq(B, A) +ct_ne_correct : (A ≠ B) ↔ (ct_ne(A, B) = 0xFF) +ct_is_ge_correct : (A ≥ B) ↔ (ct_is_ge(A, B) = 0xFF) +ct_is_ge_reflexive : ct_is_ge(A, A) = 0xFF +ct_is_ge_antisymmetric : ct_is_ge(A,B) ∧ ct_is_ge(B,A) → A = B +ct_is_ge_total : ct_is_ge(A,B) ∨ ct_is_ge(B,A) +ct_is_zero_correct : (A = 0) ↔ (ct_is_zero(A) = 0xFF) +ct_is_negative_correct : (A >> 63 = 1) ↔ (ct_is_negative(A) = 0xFF) +ct_select_true : ct_select(A, B, 0xFF) = A +ct_select_false : ct_select(A, B, 0x00) = B +ct_swap_true : ct_swap(A, B, 0xFF) = (B, A) +ct_swap_false : ct_swap(A, B, 0x00) = (A, B) +choice_not_involution : !!c = c +``` + +**실행**: + +```bash +cd core/constant-time/saw +./docker_verify.sh +``` + +### 7.2 정적 분석 — 어셈블리 검사 + +`cc-constant-time-audit` CI 워크플로를 통해 릴리즈 빌드의 어셈블리를 분석하여 비밀 데이터 의존적 분기 명령어(`JE`, `JNE`, `JB`, `JAE`, `CMOV` 등)가 존재하는지 검사한다. + +### 7.3 동적 타이밍 검증 — DudeCT + +통계적 타이밍 분석으로 실제 하드웨어에서의 타이밍 누출을 검증한다. + +**알고리즘**: Reparaz et al., "dudect: assessing the Constant-Time Property of Code in Practice", CHES 2017 +**방법**: Welch's t-검정 (Welford 온라인 알고리즘, 수치 안정) +**환경**: Ubuntu 24.04 x86_64 베어메탈 (OS 노이즈 최소화) + +| 판정 기준 | $\lvert t \rvert$ 범위 | 의미 | +|-------|-----------------------------------|-------------| +| PASS | $< 4.5$ | 타이밍 누출 없음 | +| WARN | $4.5 \leq \lvert t \rvert < 10.0$ | 주의 — 재검토 필요 | +| FAIL | $\geq 10.0$ | 타이밍 의존성 검출 | + +**측정 파라미터**: $N = 1{,}000{,}000$ 샘플, 상위 5% 이상값 제거, 기본 웜업 10,000회 + +```bash +cargo run --bin dudect-eval --release -- --warmup 50000 +``` + +**측정 정밀도**: `RDTSC + LFENCE` 직렬화로 명령어 재정렬 방지 + +```rust +core::arch::x86_64::_mm_lfence(); +core::arch::x86_64::_rdtsc() +``` + +**PRNG 대칭성 요구사항**: 두 클래스(동일/상이)에서 PRNG 호출 횟수가 동일해야 한다. 비대칭 호출은 CPU 마이크로-아키텍처 상태 편차를 유발하여 위음성 FAIL의 원인이 된다. + +--- + +## 8. 보안 제약 사항 + +1. `Choice` 내부 필드(`u8`)는 절대로 `pub`으로 공개해선 안 된다. +2. `from_mask`의 호출자는 `mask ∈ {0x00, 0xFF}` 불변 조건을 반드시 보장해야 한다. +3. `saw_verify` 피처는 프로덕션 빌드에서 절대 활성화해선 안 된다. `black_box` 우회로 인해 타이밍 공격에 취약해진다. +4. `#[inline(always)]`를 모든 연산에 적용한다. 함수 호출 오버헤드 자체가 타이밍 차이를 유발할 수 있다. +5. 이 크레이트의 연산을 `unsafe` 블록 내에서 호출할 경우, Rust 메모리 안전 보장이 적용되지 않는 경계에서 비밀 데이터 누출 경로를 별도로 검토해야 한다.