기술적 요약: 조건부 독립을 통한 프로빙 보안의 형식적 검증

문제 제기

사이드 채널 공격은 암호 체계의 보안에 중대한 위협을 가하고 있어, 이에 대한 대응책으로 마스킹이 광범위하게 채택되고 있습니다. 마스킹은 비밀 값을 쉐어로 분할하여 중간 값의 어떤 부분 집합에서도 누출이 근본적인 비밀을 드러내지 않도록 보장합니다. 그러나 특히 ISW 프로빙 모델(적대자가 최대 $t$개의 중간 값을 프로브할 수 있는 모델) 하에서 마스킹된 알고리즘의 보안을 증명하는 것은 수동으로 수행할 경우 오류가 발생하기 쉽기로 유명합니다. 수동 보안 증명에서 여러 결함이 발견되어 형식적 검증이 필요해졌습니다.

확률적 분리 논리는 일회용 패드와 같은 입력 독립성과 같은 속성을 검증하는 데 성공적으로 적용되어 왔으나, 마스킹된 알고리즘의 프로빙 보안(특히 $t$-비간섭성)을 검증하는 데는 아직 활용되지 않았습니다. 기존 형식적 검증 도구들은 종종 치환 기반 방법이나 타입 추론에 의존하는데, 이는 마스킹에 내재된 복잡한 조건부 독립 추론에 필요한 모듈성이나 표현력이 부족할 수 있습니다.

방법론

이 연구는 시뮬레이터 기반 보안 정의와 조건부 독립 사이에 엄밀한 연결을 확립함으로써 형식적 검증을 위한 새로운 접근법을 제안합니다. 이 방법론은 조건부 독립에 대해 추론하도록 설계된 확률적 분리 논리인 Lilac에 의존합니다.

1. 이론적 기반: 시뮬레이터와 조건부 독립

저자들은 조건부 독립의 관점에서 비간섭성의 표준 시뮬레이터 기반 정의를 재구성합니다.

• 시뮬레이터 기반 관점: 마스킹된 알고리즘이 안전하다는 것은, 적대자가 관찰하는 임의의 프로브 집합 $O$에 대해, 나머지 비밀 쉐어에 접근하지 않고 입력 쉐어의 부분 집합 $I$만을 사용하여 $O$의 분포를 생성할 수 있는 시뮬레이터가 존재함을 의미합니다.
• 조건부 독립 관점: 이 보안 요구 사항은 공개 입력 쉐어 $I$가 주어졌을 때, 관찰된 값 $O$가 비밀 입력 쉐어 ($\Delta \setminus I$) 와 조건부 독립이라는 진술과 동치입니다. 형식적으로는 $O \perp (\Delta \setminus I) \mid I$로 표현됩니다.

이 논문은 확률 공간의 독립적 결합과 분해 (disintegration) 를 통한 조건부 설정을 모델링하는 Lilac의 의미론적 프레임워크 내에서 이러한 동치가 성립함을 보여줍니다.

2. Lilac 의 확장

프로빙 보안에 Lilac 을 적용하기 위해 저자들은 원래 Lilac 공식에 없었던 특정 증명 규칙으로 논리를 확장합니다.

• 반-그래프roid 공리 (Semi-Graphoid Axioms): 이 논문은 Lilac의 의미론 내에서 조건부 독립을 위한 반-그래프roid 공리 (대칭성, 분해, 약한 합집합, 수축) 가 성립함을 증명합니다. 이러한 공리는 증명 과정에서 조건부 독립 진술을 조작하는 데 필수적입니다.
• 조립성 규칙: 순차 조립과 for-루프에 대해 특히 비간섭성 속성의 조립을 처리하기 위한 새로운 규칙이 도입됩니다. 이러한 규칙은 더 작은 가젯 (gadgets) 으로 구성된 복잡한 알고리즘의 모듈식 검증을 가능하게 합니다.
• 소유권과 약화: 추가 규칙은 확률 변수의 소유권에 대한 추론과 비공유 입력이나 변수 부분 집합을 다룰 때 비간섭성 속성의 약화에 대한 추론을 용이하게 합니다.

3. 검증 프레임워크

검증 과정은 다음을 포함합니다:

1. APPL 확률적 프로그래밍 언어로 작성된 마스킹된 알고리즘을 Lilac 내의 Hoare 삼중항으로 변환합니다.
2. 확립된 동치 (정리 V.1) 를 사용하여 $(I, O)$-비간섭성 검증을 특정 조건부 독립 Hoare 삼중항의 증명으로 축소합니다:
   $$\{ \text{own } \Delta \} \ M \ \{ Y. \ C_{x \leftarrow I}(\text{own}(\Delta \setminus I) * \text{own } O) \}$$
3. 새로운 반-그래프roid 및 조립성 규칙을 포함한 확장된 증명 규칙 세트를 적용하여 필요한 함의를 유도합니다.

주요 기여

1. 형식적 연결: 이 논문은 Lilac 에서 표현 가능한 조건부 독립 속성과 프로빙 보안의 시뮬레이터 기반 정의 사이의 형식적 동치를 확립합니다. 이는 암호학적 보안 개념과 확률적 분리 논리 간의 간극을 메웁니다.
2. Lilac 의 확장: 저자들은 조건부 독립을 위한 반-그래프roid 공리와 순차 조립 및 루프를 위한 조립성 규칙을 포함하여 마스킹된 알고리즘을 검증하는 데 필요한 추가 증명 규칙 세트를 제공합니다.
3. 사례 연구: 이 접근법의 효과는 Lilac 을 사용하여 세 가지 중요한 알고리즘의 프로빙 보안을 형식적으로 검증함으로써 입증됩니다:
   • MINIADDREPNOISE: 마스킹된 값에 균일한 노이즈를 추가하는 서브루틴.
   • REFRESH: 누출 축적을 방지하기 위해 쉐어를 갱신하는 기본 알고리즘.
   • SECMULT: 표준 마스킹 곱셈 알고리즘.
   • ADDREPNOISEER: NIST 포스트 양자 암호 표준화 후보인 Raccoon 서명 체계에서 사용되는 변형으로, $t$-비공유 입력을 가진 $t$-강한 비간섭성 ($t$-SNIU) 속성을 만족함을 증명합니다.

결과

이 논문은 대상 알고리즘에 대한 Hoare 삼중항을 성공적으로 유도하여 그들의 비간섭성 속성을 확인했습니다.

• MINIADDREPNOISE의 경우, 증명 결과 관찰된 입력이 주어졌을 때 출력 쉐어가 관찰되지 않은 입력 쉐어와 조건부 독립임을 보여줍니다.
• REFRESH의 경우, 증명 결과 이 알고리즘이 표준 비간섭성보다 강력한 속성인 $t$-강한 비간섭성 ($t$-SNI) 을 만족함을 검증합니다. 이는 고차 마스킹에서의 조립성에 필수적입니다.
• SECMULT와 ADDREPNOISEER의 경우, 증명들은 이러한 알고리즘에 내재된 중첩된 루프와 복잡한 데이터 종속성을 처리하기 위해 새로운 조립성 규칙을 활용합니다.

ADDREPNOISEER의 검증은 특히 중요합니다. 이는 $t$-SNIU 속성에 의존하는 Raccoon 서명 체계 보안 증명의 핵심 구성 요소를 검증하기 때문입니다.

중요성과 주장

저자들은 이 작업이 마스킹된 알고리즘에 대한 프로빙 보안의 형식적 검증에 확률적 분리 논리 (특히 Lilac) 를 적용한 최초의 사례라고 주장합니다. 보안 증명을 조건부 독립 추론으로 변환함으로써, 이 접근법은 기존 치환 기반 또는 타입 추론 도구에 대한 모듈식이고 논리적으로 엄격한 대안을 제공합니다.

이 논문은 시뮬레이터를 조건부 독립과 연결하는 근본적인 아이디어는 개념적으로 단순하지만, 독립적 결합에 의존하는 논리의 특성상 표준 곱 확률 공간이 아닌 Lilac 에서의 형식화는 기술적으로 단순하지 않다고 강조합니다. 주요 정리의 성공적인 유도와 Raccoon 과 같은 실제 암호 구성 요소에 대한 적용은 이 프레임워크가 복잡한 고차 마스킹 체계를 검증하는 데 실행 가능함을 보여줍니다.

이 작업은 그 범위에 대해 겸손하게, 현재 결과는 프로빙 보안의 정보 이론적 설정으로 제한된다고 명시합니다. 저자들은 이 접근법을 계산적 설정으로 확장하고 상호작용형 정리 증명기에서 이 방법을 구현하는 것을 향후 연구의 중요한 방향으로 꼽습니다. 또한 이 프레임워크가 안전한 다자간 계산에서 발견되는 것과 같은 다른 시뮬레이터 기반 보안 속성에도 적용될 수 있음을 제안합니다.