이 논문은 Triosecuris라는 새로운 방어 메커니즘을 소개하며, 이는 Spectre BTB(Branch Target Buffer), RSB(Return Stack Buffer), PHT(Pattern History Table) 공격에 대해 형식적으로 검증된 보호를 제공합니다. Triosecuris 는 인텔 CET(Control-flow Enforcement Technology) 스타일의 하드웨어 지원 제어 흐름 무결성 (CFI) 과 컴파일러가 삽입하는 Ultimate SLH(Speculative Load Hardening) 를 결합한 혁신적인 접근법입니다.

다음은 논문의 주요 내용을 기술적으로 요약한 것입니다.

1. 문제 정의 (Problem)

• Spectre 공격의 위협: Spectre 는 프로세서의 예측 실행 (Speculative Execution) 기능을 악용하여 민감한 데이터를 유출하는 사이드 채널 공격입니다. 특히 Spectre BTB (간접 분기 예측 악용) 와 Spectre RSB (반환 주소 예측 악용) 는 제어 흐름을 임의로 조작하여 코드 내의 임의의 '가젯 (gadget)'을 실행하게 만들어 비밀 정보를 유출할 수 있습니다.
• 기존 방어책의 한계:
  • **CFI **(Control-Flow Integrity) 기존 CFI 는 메모리 손상 공격을 방어하기 위해 설계되었으며, 간접 호출의 타겟을 정적 집합으로 과대 추정 (overapproximation) 합니다. 이는 공격자가 정적 집합 내에 속하지만 의도하지 않은 함수를 호출하도록 유도하여 방어 우회가 가능하게 합니다.
  • Serberus 등의 대안: BTB 와 RSB 를 모두 방어하는 Serberus 와 같은 기존 연구조차도 정적 과대 추정을 사용하므로, 복잡한 강제 메커니즘 (프로시저별 스택, 레지스터 정리 등) 이 필요하고 제한 사항 (값으로 전달된 비밀 보호 불가 등) 이 존재합니다.
  • SLH 의 부족: Ultimate SLH 는 PHT 공격에는 효과적이지만, BTB 나 RSB 에 의해 제어 흐름이 완전히 다른 경로로 전환될 경우 (예: SLH 가 삽입된 분기 전에 BTB 가 잘못된 함수로 점프하는 경우) 보호를 무력화할 수 있습니다.

2. 방법론 (Methodology)

Triosecuris 는 CET-style 하드웨어 보호와 컴파일러 삽입 Ultimate SLH를 결합하여 정밀한 미스프레딕션 (misspeculation) 감지를 가능하게 합니다.

핵심 아이디어: 정밀한 미스프레딕션 감지

기존의 정적 라벨 기반 CFI 와 달리, Triosecuris 는 동적 호출 타겟을 직접 비교하여 미스프레딕션을 감지합니다.

1. **BTB **(간접 호출)

   • 호출자 (Caller) 는 간접 호출 직전에 호출하려는 함수 포인터를 전용 레지스터 (callee) 에 저장합니다.
   • 피호출자 (Callee) 의 시작 부분에는 ctarget 명령어 (CET 의 유효 타겟 마커) 가 삽입됩니다.
   • 피호출자 내부에서는 callee 레지스터의 값이 실제 함수의 시작 주소를 가리키는지 확인합니다.
   • 핵심: 예측 실행 중 BTB 가 잘못된 함수로 점프하면, callee 레지스터의 값과 실제 실행 위치가 불일치하게 되어 **미스프레딕션 플래그 **(msf)가 설정됩니다.

2. **RSB **(반환)

   • 반환 (Return) 직전에 호출 스택의 최상단 (반환 주소) 을 peek 명령어로 읽어 callee 레지스터에 저장합니다.
   • 반환 후 (또는 반환 타겟에서) 저장된 주소와 실제 반환 위치를 비교하여 불일치 시 msf 를 설정합니다.

3. Ultimate SLH 와의 통합:

   • msf 플래그가 설정되면, Ultimate SLH 메커니즘이 메모리 로드 주소, 분기 조건, 연산자 등 모든 민감한 데이터를 **마스크 **(0 으로 대체) 합니다.
   • 이로 인해 공격자가 예측 실행 중에도 민감한 데이터에 접근하거나 캐시 상태를 변경할 수 없게 됩니다.

3. 주요 기여 (Key Contributions)

1. Triosecuris 제안: CET-style 보호 하에서 BTB 와 RSB 미스프레딕션을 **정확하게 **(precisely) 감지하고 SLH 플래그를 설정하는 새로운 방어 체계 개발. 이는 정적 과대 추정이 필요 없음을 의미합니다.
2. **Rocq **(구 Coq)
   • Triosecuris 를 단순한 저수준 언어 (MINIMIR) 에서 CET 와 예측 실행을 모델링한 언어로 변환하는 컴파일러로 형식화했습니다.
   • **상대적 보안 **(Relative Security) 증명을 위해 **정의되지 않은 값 **(Undefined Values, UV) 개념을 도입했습니다. SLH 로 인해 코드 포인터와 정수가 혼재될 때 발생할 수 있는 정의되지 않은 행위를 방지하고, 안전성 (Safety) 을 보존함을 증명했습니다.
3. **종단 간 **(End-to-End)
   • MINIMIR(블록 단위) 에서 MINIMC(기계어/선형화) 로의 변환 단계까지 포함하여, 안전한 입력에 대해 변환된 프로그램이 소스 프로그램보다 더 많은 정보를 유출하지 않음을 기계적으로 검증했습니다.
   • 이 증명은 암호학적 상수 시간 (constant-time) 프로그래밍 규칙을 따르지 않는 임의의 프로그램에도 적용 가능합니다.
4. **안전성 보존 **(Safety Preservation) Triosecuris 변환이 소스 프로그램에서 정의된 행위를 수행하는 입력에 대해, 변환 후에도 정의되지 않은 행위를 발생시키지 않음을 증명했습니다.

4. 결과 (Results)

• 형식적 검증 완료: 약 6,800 줄의 Rocq 코드로 Triosecuris 변환과 보안 증명을 구현했습니다.
• 보안 보장: 변환된 프로그램은 예측 실행 환경에서도 소스 프로그램이 순차 실행 시 유출하는 정보 이상을 유출하지 않습니다. 이는 공격자가 BTB, RSB, PHT 를 모두 제어할 수 있는 강력한 공격 모델 하에서도 성립합니다.
• 실용성: 암호학적 상수 시간 코드가 아닌 일반적인 프로그램에도 적용 가능하며, 기존 Serberus 등의 복잡한 제약 조건 (예: 비밀을 값으로 전달 불가) 을 피합니다.

5. 의의 및 중요성 (Significance)

• 정밀한 방어: Spectre 공격에 대한 방어에서 정적 과대 추정을 제거하고 동적 검사를 통해 정밀한 보호를 실현함으로써, 방어 오버헤드를 줄이고 보안성을 높였습니다.
• 하드웨어 - 소프트웨어 협업: 인텔 CET 와 같은 최신 하드웨어 기능을 컴파일러 최적화 (SLH) 와 효과적으로 결합하여, 하드웨어만으로는 불가능했던 정밀한 제어 흐름 보호를 가능하게 했습니다.
• 형식적 검증의 중요성: Spectre 방어는 구현 오류나 모델링 누락으로 인해 쉽게 우회될 수 있습니다. Triosecuris 는 기계 검증 (Machine-checked proof) 을 통해 이러한 취약점을 근본적으로 제거하고 강력한 보안 보장을 제공합니다.
• 미래 지향성: 이 연구는 LLVM 에 Triosecuris 를 구현하는 기반을 마련했으며, 향후 선택적 SLH(FSLH) 나 소프트웨어 기반 방어 (retpoline 등) 와의 결합을 통해 더 넓은 범위의 프로세서 아키텍처에 적용할 수 있는 가능성을 제시합니다.

요약하자면, Triosecuris 는 하드웨어 지원 CFI 와 소프트웨어 기반 SLH 를 융합하여 Spectre BTB/RSB/PHT 공격에 대해 정밀하고, 형식적으로 검증된, 그리고 범용적인 방어 솔루션을 제시한 획기적인 연구입니다.