[논문 정리] SCASE: Automated Secret Recovery via Side-Channel-Assisted Symbolic Execution

서론

심볼릭 실행을 공부하면서 이게 어떻게 사용되는지 좀 더 알고싶어 관련 논문을 찾아보았다.

 

그 중에 부 채널 공격시에 심볼릭 실행이 사용된다는걸 보고 "심볼릭 실행이 어떻게 부 채널 공격에서도 사용되는거지?" 하는 궁금증이 생겨 읽게 되었다.

 

시험기간이 걸쳐져서 좀 오래 걸리긴 했는데 이번에도 정리해서 올려보려고 한다.

그럼 시작하겠다.

원문

Weber, Daniel, et al. "{SCASE}: Automated Secret Recovery via {Side-Channel-Assisted} Symbolic Execution." 34th USENIX Security Symposium (USENIX Security 25). 2025.

https://www.usenix.org/conference/usenixsecurity25/presentation/weber

SCASE: Automated Secret Recovery via Side-Channel-Assisted Symbolic Execution | USENIX

Abstract

최근 몇 년간 소프트웨어 기반의 부채널 공격에 대한 폭발적인 연구가 이루어졌지만, 두 가지 한계가 있었다.

1. 민감한 정보를 얻기 위해서 대상 프로그램에 대한 깊은 이해가 필요.
2. 비밀 값 복구의 자동화가 어려움

이 논문에서는 불투명한 타겟 바이너리에서 구체적인 부채널 트레이스를 이용한 심볼릭 실행으로 비밀 값을 가져오는 새로운 방법인 SCASE와, PoC 프레임워크인 Athena를 사용한다.

 

핵심 아이디어는 심볼릭 실행 공간을 효율적으로 줄이기 위해 부채널 트레이스에서 관찰된 메모리 접근 정보를 활용하는 것이다.

대상 알고리즘	추출 데이터	소요 시간	특이 사항
RSA	2048-bit Key	4분 이내	SGX 엔클레이브 환경
RC4	256-bit Key	5분 이내	KSA 구현체 타겟
AES	256-bit Key	-	OpenSSL S-box 공격
BEEA	Input Value	-	알고리즘 입력값 복구

 

Athena는 별도의 사전 지식 없이 다음 암호 키들을 빠른 시간 내에 복구한다.

 

이 연구는 부채널 트레이스를 통해 심볼릭 실행을 제약하는 것이 대상 프로그램에 대한 깊은 이해 없이 소프트웨어 기반의 부채널 공격을 자동화하는 효과적인 방법임을 보여준다.

Introduction

기존 연구는 다음과 같은 한계가 있었다

• 공격자가 소스 코드의 취약점이나 바이너리 레이아웃을 포함한 타겟 프로그램에 대한 전문적인 지식이 필요함.
• 취약점을 찾는 도구는 많지만 False Positive, 즉 오탐률이 높아 실제로 해킹이 되는지 확인하기 위해서는 수동 검증이 필요함.
• 심볼릭 실행은 모든 경우의 수를 다 계산하는거다보니 너무 느렸음.

이에 따라 SCASE (side-channel-assisted symbolic execution)는 state explosion을 완화하면서 점진적으로 경로의 제약 조건을 수집하여 constraint solver가 자동적으로 비밀 값을 구채화할 수 있도록 한다.

 

또한 이 과정에서 타겟 프로그램에 대한 이해가 비밀값과 어떻게 연관되는지에 대한 사전 지식을 요구하지 않으며 단지 다음 두 가지만을 필요로 한다.

1. 대상 코드와 데이터 접근을 기록하는 자동화된 부채널 트레이스 추출 프레임워크
2. 타겟 바이너리 내의 비밀 값 위치의 주석처리.

이를 위해 PoC 프레임워크인 Athena를 개발했으며 이를 이용하여 위의 표와 같이 암호화 알고리즘에 대해 빠른 시간 내에 비밀 값을 복구할 수 있었다.

Background

Software-based side-channel attacks

부채널 공격은 프로그램의 실행에 대해서 메타데이터를 누출하는 종류의 공격을 말한다.

 

CPU 캐시부터 시작하여, CPU 내부 구조의 상태, CPU 실행 유닛의 경합, 그리고 전력 소모와 같은 다양한 정보를 사용한다.

현대 소프트웨어 기반 부채널 공격은 강력하고, 높은 정확도와 throughput을 보인다.

Symbolic Execution

심볼릭 실행은 시스템적으로 가능한 모든 입력값에 대해서 도달가능한 모든 실행 상태를 조사는 정적 프로그램 분석 기술이다.

 

심볼릭 실행 엔진 (Symbolic execution engine)은 구체적인 값일수도 있고 관련된 제약조건으로 표현되는 심볼릭 값일수도 있다.

 

심볼릭 실행은 일반적으로 두 단계로 구성된다

• Path exploration phase
  • 프로그램의 모든 가능한 실행 경로를 에뮬레이션하여 제어 흐름 그래프 (CFG)를 탐색한다.
  • 구체적인 입력으로 결정할 수 없는 분기를 만나면 SEE는 두 경로를 fork하여 모든 분기를 탐색한다.
  • 이 때 분기 조건의 심볼릭 값들은 현재 상태에 도달하는 결과를 얻을 수 있도록 제약된다.
• Solving phase
  • SAT solver와 같은 logic solver를 활용하여 위의 심볼릭 값들에 대한 구체적인 값을 계산한다.
  • 심볼릭 실행은 소스코드나 바이너리 레벨에서도 진행될 수 있다.

이러한 장점에도 불구하고 심볼릭 실행은 state explosion이라는 문제를 가진다.

💡

State explosion

프로그램의 가능한 분기에 대해서 모두 계산을 진행할 때 메모리 상태와 제약조건이 기하급수적으로 늘어나 결국 계산하지 못하는 현상. 이에 따라 RSA, AES와 같은 암호 알고리즘은 수학적으로 매우 복잡한 조건으로 인해 해결하지 못하는 것으로 고려된다.

Intel Software Guard Extensions

Intel의 Software Guard Extensions (SGX)는 런타임에서 하드웨어 독립적인 메모리 구역의 기밀성과 무결성을 제공하는 신뢰 실행 환경 (TEE)으로 엔클레이브 (enclave)라고 불린다.

 

SGV 엔클레이브는 다음과 같은 특징이 있다

• 일반적인 사용자 프로세스 내에 있다
• 대상 플랫폼의 권한 있는 소프트웨어를 제어하는 루트 공격자에 대해서 보호된 상태를 유지한다

SGX의 격리모델과 작은 신뢰 컴퓨팅 기반은 암호 라이브러리와 같은 높은 보안 작업을 이상적으로 만든다.

 

또한 이 엔클레이브는 ECALL함수라고 불리는 진입점을 통해서 접근할 수 있으며, OCALL함수는 신뢰할 수 없는 호스트 프로세스에 구현되어 신뢰할 수 없는 콜백 역할을 수행한다.

 

SGX는 광범위한 부채널 공격의 대상이 되어왔기때문에 실전에서 실전에서 검증된 (battle-tested) TEE라고 지칭하게 되었다.

Controlled-Channel Attacks

TEE에 대한 부채널 공격으로는 제어 채널 공격 (Controlled-Channel attack)이 있다.

 

제어 채널 공격에서는 TEE 엔클레이브가 메모리 페이지를 설정할 때 이미 공격자가 제어권을 가지고있는 OS에 의존하는걸 응용한다.

• 공격자가 Page-table entry를 조작하여 fault가 발생하게함.
• 이 경우 엔클레이브는 실행을 중단하고 제어권을 OS에 넘김
• 이 과정에서 엔클레이브는 레지스터 값을 모두 지우지만, 특정 page table entry를 접근한 정보는 남게됨

또 다른 공격 기법으로는 single stepping이 있다.

• Single stepping
  • 엔클레이브 코드가 정확히 하나의 명령어를 실행한 직후에 타이머 인터럽트가 발생함.
  • 이에따라 공격자는 엔클레이브의 실행을 정밀하게 제어할 수 있음.

해당 공격은 SGX뿐만 아니라 Intel TDX, AMD SEV와 같은 다른 TEE 및 VM에도 적용될 수 있다.

SCASE

SCASE (Side-Channel-Assisted Symbolic Execution)은 대상 프로그램에 대해 비밀 값을 자동적으로 복구하도록 하는 기법으로, 부채널 공격으로 얻은 정보를 SEE에 전달해 기존의 한계와 비밀 키 복구가 자동적으로 이루어지게 도움을 준다.

General Threat Model

여기서 위협 모델은 다음과 같이 가정했다.

• 공격자가 타겟의 바이너리에 접근할 수 있음.
  • 이를 통해 타겟을 심볼릭하게 (모든 경로를 분석) 실행할 수 있도록 함.
• 공격자는 비밀 값을 바로 가져올 수 없으며, 오직 누출된 메타데이터만 사용가능함.
• 하드웨어와 소프트웨어에는 메타데이터 누출 이외의 취약점은 없다.
• 공격자는 이 정보를 모니터링할 수 있는 능력이 있다.

Overview

SCASE는 부채널 공격과 심볼릭 실행을 결합한 기법으로, 부채널 공격에서 얻은 메모리 트레이스를 바탕으로 SEE가 경로 탐색과 제약 조건을 생성하도록 한다.

 

이를 통해 탐색 공간을 획기적으로 줄여 상징화된 비밀키를 복구한다.

 

이 접근은 online과 offline 단계로 구성된다.

• Online phase
  • 부채널 공격이 대상 프로그램에 수행되어 메모리 접근 패턴에 관한 가능한 한 많은 정보를 추론한다.
  • 공격을 통해 복구한 정보를 memory trace라고 부른다.
    • memory trace에는 메모리에 대한 제어 흐름과 데이터 흐름의 내용이 포함되며, 각각을 control-flow trace, data-flow trace라 부른다.

• Offline phase
  • online 과정에서 얻은 트레이스들로 SEE가 대상의 비밀 값을 복구할 수 있도록 하는 과정이다.
    • control-flow trace는 대상이 어떤 분기를 선택했는지에 대한 정보를 전달한다.
      • 이를 통해 대상이 online phase에서 실행하지 않은 경로는 줄일 수 있다.
      • 비밀값에 의존하는 제어 흐름은 트레이스에 인코딩된 비밀값에 대한 제약조건으로 이어진다.
    • data-flow trace는 어떤 메모리 위치에 접근했는가에 대한 정보를 전달한다.
      • 데이터 흐름 접근 패턴을 알면, SEE는 관찰된 패턴과 일치하지 않는 상태를 줄일 수 있다. → 즉 state space를 줄일 수 있다
  • 이러한 과정을 통해 SEE는 online 과정에서 얻은 메타 정보로 비밀 값을 효율적으로 계산해낼 수 있다.

Majoir Challenges

비밀 값 추출을 자동화하기 위해서 많은 난관이 있었다.

1. State Explosion

가능한 모든 경로를 탐색하는데 필요한 state space가 기하급수적으로 증가하는 문제. 모든 상태를 확인할 수 있다는게 SEE의 장점이지만, 복잡한 프로그램에 대해서는 효율적이지 못함

 

특히 암호 알고리즘의 보안 보장이 방대한 state space에 기반하고있기 때문에, 전형적인 암호화 어플리케이션의 비밀 값 의존적 제어흐름 (secret dependent control-flow)은 state explosion을 증가시킨다.

 

또 다른 문제는 SEE가 결국 비밀 값을 알아야 한다는 것이다. 심볼릭 실행으로 결과를 얻었다고 할지라도, 결국 그 값은 어떤 값을 넣으면 이런 결과가 나올 수 있다는 수 많은 선택지가 생길 뿐이고, 결국 입력값인 비밀 값을 알아내기 위해서는 암호 알고리즘에 의해 생성된 암호문이 필요하다.

 

이 문제는 온라인 단계 (부채널 공격)에서 얻은 메모리 접근 정보를 바탕으로 SEE가 탐색해야할 공간을 줄여나가는 방법으로 해결했다.

 

   2. Map Side-Channel Information to the SEE’s State Space

 

SEE에서 부채널의 정보를 활용하기 위해서는 각 실행 단계에서의 매핑이 정확히 이루어져야한다.

 

SEE의 어떤 상태와 정확히 매핑되는 메모리 트레이스의 항목이 존재한다 (왜냐하면 결국 실행 흐름에 따라 메모리 트레이스가 생기기 때문에). → 그러므로 SEE와 메모리 트레이스의 단사 매핑(injective mapping)을 구축해야한다.

 

이 때 프로그램 내의 한 어셈블리 명령어는 여러번 호출될 수 있기 때문에 시간적 요소를 고려하여 매핑이 고려되어야한다.

 

부채널 공격중에 노이즈가 섞일 수 있는데, 이 경우 제대로된 매핑이 되지 않으니 노이즈가 없는 정확한 매핑이 중요하다.

💡

injective mapping

단사 매핑. 일대일 함수를 의미한다

 

   3. Seperating Control- and Data-Flow Related Memory Accesses

 

제어 및 데이터 흐름 관련 메모리 접근은 모두 SEE에게 정보를 제공하지만, 실행에는 서로 다른 방식으로 영향을 미친다.

 

실행을 더욱 정밀하게 돕기 위해서는 두 가지 메모리 접근 방식을 구분할 수 있어야한다.

1. 해당 메모리가 명령어 패치 (fetching of an instruction)에 의해서 접근이 되었는지
2. 해당 메모리가 명령어 실행에 의해서 접근이 되었는지

이 방식의 구분이 필수적인건 아니지만, pruning과 제약조건 생성에 도움이 된다

SCASE: Recovering Secrets from Memory Traces using Symbolic Execution

위에서 언급한 문제점들을 해결하는 과정을 설명한다.

Splitting Memory Traces into Control- and Data-Flow Memory Traes

명령어 페치(fetch)는 현재 명령어의 주소가 메모리 트레이스의 다음 항목과 일치해야함을 의미 (PC와 일치)

 

명령어 실행은 메모리 트레이스 항목이 메모리 접근 명령어의 의미론적 동작과 일치해야함.

 

예를 들어서, 메모리 트레이스 항목에 0x1234라는 주소가 있고, 거기에 매핑되는 항목이 심볼릭 수식이라면 해당 수식은 0x1234여야한다

 

이 둘을 분리하는 방법은 부채널 공격자의 역량에 달려있다.

• TEE 위협 모델처럼 강한 공격자 모델일 경우
  • 공격자는 대상의 PTE를 제어하는 비트인 메모리 페이지 permission bits를 읽을 수 있다
  • 이 비트들은 해당 페이지가 쓰기 또는 실행 가능한지를 제어한다.
  • PoC 구현체인 Athena는 이 방식의 분리를 사용한다
• 권한이 낮은 공격자
  • 마이크로 아키텍처 컴포넌트의 상태를 관찰하여 메모리 접근이 CPU 프론트엔드에서 비롯됐는지 추론한다
  • I-cache나 iTLB는 프론트엔드의 명령어 페치에 의해서만 영향을 받으므로, 이런거를 관찰해서 메모리 접근을 구분한다

Creating a Mapping between Memory Trace Entries and Emulated States

위에서 말했듯이 메모리 트레이스에 노이즈가 섞이면 제대로된 분석이 불가능하다. 따라서 오류가 없도록 보장하는 방법이 몇 가지 있다

1. 교차검증 (cross-verify)
   • 부 채널 공격을 여러 번 하고 해당 데이터를 교차검증한다
2. 제어 채널 공격처럼 애초에 에러가 존재하지 않는 부 채널 공격을 사용한다

메모리 트레이스에 오류가 없다면 각 메모리 트레이스에 대한 항목을 SEE의 state space에 매핑해야한다.

 

이를 구현하는 가장 간단한 방법은 가상 메모리 주소를 기반으로 매핑하는거다.

실행중에 한 명령어는 여러 번 실행될 수 있기 때문에 정확한 시점에 매핑이 중요하다.

 

따라서 SEE에 의해 에뮬레이션 되는 모든 탐색에 대해서 제어 및 실행 흐름 메모리 트레이스의 현재 위치를 유지해야한다. → 조건 분기에 의해 fork될 때 메모리 트레이스의 위치도 함께 fork되어야한다.

 

이를 구현하는 방법은 에뮬레이션된 메모리 접근에 대해서 해당 메모리 트레이스의 인덱스를 증가시키고, 상태공간의 모든 포크마다 다른 인덱스를 유지하는거다.

 

가상 메모리 주소가 유일한 답은 아니지만 여러 부 채널 공격에 사용될 수 있으며, 대안으로 단사 매핑이 있다.

Pruning the State Space and Adding Additional Constraints

SEE와 매핑된 트레이스들은 실제 실행중에 도달하지 않은 상태를 pruning하고, 추가적인 constraint를 만드는데 사용된다.

 

단, 제어 흐름 메모리 트레이스가 모든 분기 결정에 대해 선택된 경로 정보를 항상 포함하고 있는건 아니다. (캐시된 데이터 접근, 메모리 접근이 없는 분기 등)

 

경로 탐색이 끝나면 SEE는 만들어진 제약 조건들을 솔버를 사용해 구체화하여 결국 비밀 값을 복구한다.

어플리케이션의 메모리 접근 동작에 의존하는 모든 유형의 공격은 이 방식을 통해 자동화가 가능하다.

Athena Framework

Athena는 제어 채널 공격을 부 채널로 활용하여 SCASE를 구현한다.

 

대상은 부 채널 취약점이 있는 Intel SGX 엔클레이브이며, 물론 이런 일반적인 TEE에만 적용되는건 아니지만 제어 채널 공격은 노이즈가 없는 트레이스를 얻기 위한 온라인 단계를 자동화하는 방법이 있다.

 

Athena는 두 가지 주요 부분으로 구현되어있다

1. single stepping과 액세스 비트 모니터링을 기반으로 하는 Intel SGX용 자동 제어 채널 공격 (온라인 단계)
2. SEE인 angr을 위한 탐색전략 (오프라인 단계)

Athena의 위협 모델은 커널 모듈을 로드할 수 있는 권한을 가진 native-code 공격자를 가정한다.

 

대상 데이터를 제외한 엔클레이브에 대한 모든 내용을 알 수 있어, 공격자는 실제 비밀 정보가 없는 상태에서 대상 어플리케이션의 복사본을 debug enclave하거나 에뮬레이팅할 수 있다.

Offline phase

Emulating the Target

Athena는 Guardian을 사용해서 angr가 Intel SGX 엔클레이브 바이너리와 호환가능하게 만든다. (Intel SGX 엔클레이브가 ELF파일로 표현되기 때문에 가능)

💡

angr은 원래 .exe이나 .so파일 등을 처리하도록 만들어졌지만, Guardian은 엔클레이브와 같은 환경과의 통신 인터페이스를 연결해주기 때문에 angr이 엔클레이브를 분석할 수 있도록 한다

 

이렇게 공격자는 호스트 어플리케이션이 엔클레이브에 제공하는 기능인 OCALL을 탈취하여 더미을 반환하게 할 수 있다

더미만으로는 제대로 작동하지 않는 경우, angr의 SymProcedures 기능을 사용하여 커스텀 훅을 만들 수 있다.

 

일반적으로 OCALL의 결과가 비밀을 도출하거나 기밀 계산의 일부로 사용되지는 않는다.

 

또한 보통 원격 검증 (remote attestation) 이후에만 보안 원격 인스턴스로부터 비밀 데이터가 로드되기 때문에, 엔클레이브 바이너리를 에뮬레이션하는 것만으로는 비밀 데이터를 추출하기 어렵다.

💡

Intel SGX 기술은 인증을 로컬이 아닌 서버에서 직접 인증을 하는 방법이라 여기서 비밀값을 알아내기는 어렵다.

Mapping the Leakage to angr’s State.

제어 및 데이터 흐름 메모리 관련 접근은 서로 다르게 처리해야하는 정보를 가지고 있기 때문에 메모리 트레이스를 두 단계로 나눈다.

1. 제어 흐름 관련 메모리 접근 (어떻게 분기 결정을 했는지 정보를 전달하는 과정)
   • angr의 커스텀 서브클래스인 ExplorationTechnique로 심볼릭 실행을 더 정밀히 제어한다
   • 이 클래스의 핵심 멤버 함수인 step은 basic block에 도달할때마다 호출되어 실제 트레이스 기록과 대조하여 실행된 경로만 따라가도록 한다.
   • 현재 basic block에 포함된 명령어의 개수로 트레이스의 인덱스를 증가시켜, 제어 흐름 트레이스 내의 위치를 추적한다
   • 메모리 트레이스와 일치하지 않는 분기를 잘라내어 필요한 분기만 인코딩해 솔버에 전달한다
2. 데이터 흐름 관련 메모리 접근
   • 제어 흐름과는 다르게, 메모리 접근에 대한 명시적인 제약조건을 추가한다. 즉, 데이터의 값을 강제하는 제약조건을 추가한다
   • 이를 모델링 하기 위해 Athena는 angr에서 발생하는 모든 메모리 읽기 쓰기에 callback을 등록한다
   • 콜백 내의 코드는 특정 실행 상태에 대한 데이터 흐름 트레이스의 현재 위치를 추적한다. 콜백이 호출될때마다 실행 상태의 값을 1씩 올려주기만 하면 된다

남은 작업은 솔버가 데이터 흐름 트레이스와 일치하는 메모리 접근을 하도록 제약조건을 부여하는것이다.

 

이를 위해 다음과 같은 제약조건을 SAT solver에 추가한다

mActual AND NEG64-bit(0xFFF) == mTrace

=> mActual AND 0xFFFFFFFFFFFFF000 == mTrace // mActual의 상위 52비트만 남겨서 mTrace와 비교한다

• mActual: 실행 중 특정 지점에서 실제로 접근한 메모리 주소
• mTrace: 데이터 흐름 트레이스에 기록된 page-aligned entry
• $NEG_{64-bit}$: 64비트 정수의 binary negation

이 공식은 페이지 크기를 4kB로 가정한다.

 

실행 상태의 한 구체적인 시점에 발생하는 메모리 접근에 대해서만 제약을 추가한다. 즉, 루프 내부의 메모리 로드의 경우 매 반복마다 메모리 주소가 같더라도 접근하는 값이 다르면 서로 다른 제약 조건을 가질 수 있다

💡

보통 운영체제에서는 4kB를 하나의 페이지 단위로 사용하고있으며, 0xFFF는 4kB크기의 메모리 페이지 오프셋을 의미한다. 따라서 오프셋을 제외한 상위 주소와 mTrace를 비교하겠다는 의미이다.

Symbolizing and Constraining the Secret

비밀 정보를 복구하기 위해서, Athena는 먼저 비밀 바이트가 저장된 메모리 범위를 상징화 (symbolize)하고 대상 프로그램의 CFG를 탐색하면서 메모리 접근 트레이스에서 파생된 데이터 및 제어 흐름 제약 조건을 상징화된 비밀 정보에 추가한다.

 

이 방식은 부 채널 트레이스가 비밀 값을 완전히 찾아낼 수 없어도 비밀 값의 일부를 복구할 수 있게 한다.

 

이러한 접근 방식은 심볼릭 탐색과 구체적인 실행 트레이스를 통합한다는 점에서 concolic 또는 DSE의 새로운 형태라고 볼 수 있다.

Online Phase

Athena에서는 세밀한 메모리 트레이스를 얻어내기 위해 제어 채널 공격을 사용하며, single-stepping하면서 페이지 테이블 엔트리의 접근 비트 (access bits)를 모니터링한다.

💡

single-stepping

프로그램의 명령어 한 개씩 끊어서 실행하는 디버깅/공격기법

 

페이지 테이블 엔트리는 NX (Non-Executable) 비트를 기준으로 두 그룹으로 나눌 수 있다.

1. 만약 페이지가 NX라면 해당 페이지는 데이터만 담고있으니 데이터 흐름 트레이스로 추적된다
2. 만약 페이지가 NX가 아니라면 해당 페이지는 코드를 담고있으니 제어 흐름 트레이스로 추적된다

참고로 이런 구분법은 꼭 권한이 있어야하는게 아니라 권한이 없는 공격자 모델에서도 memory map만 안다면 가능하다. memory map 정보를 얻을 수 없다고 해도, 정적으로 정의된 모든 메모리 페이지에 대해서는 ELF파일이 구조 정보를 모두 제공한다

 

메모리 접근 패턴에 대해 의미있는 정보를 주지 못하는 엔클레이브 TCS 페이지같은 메모리 페이지들은 추적하지 않는다.

 

트레이스는 이러한 방식으로 얻어진다

1. single-step으로 명령어 하나만 실행
2. check bit 확인
3. check bit가 활성화되어있다면 이를 해당하는 트레이스에 추가
4. 엔클레이브 실행 재개 전에 해당 비트 초기화
5. 다음 명령어 실행

이 과정을 반복하면 제어, 데이터 흐름 접근 패턴에 대응하는 리스트 두 개를 얻을 수 있다

Usage

Athena는 트레이서가 대상 엔클레이브의 취약한 ECALL을 호출하도록 이를 실행하는 콜백 함수만 구현해주면 비밀 값을 복구하는 모든 과정을 자동화해준다.

 

오프라인 단계에서는 Athena 파이썬 모듈을 호출하여 비밀을 추출한다. 이 단계에서는 단순히 RDI 레지스터에 복구해야할 비밀 값이 무엇인지만 명시해주면 된다.

 

만약 대상이 바뀌더라도 콜백함수와 RDI만 바꾸면 되기 때문에 PoC 생성이 더 쉬워진다.

Alternative Side-Channel Traces

Athena는 제어 채널 공격을 사용해서 대상 프로그램을 모니터링하는데, 다른 소프트웨어 기반의 부 채널 공격도 비슷하게 작동할 수 있다

Space Resolution

제어 채널 공격은 대부분의 페이지를 관찰 가능하다는 장점이 있지만 그 단위가 페이지이다 보니 세밀한 추적은 힘들다. 하지만 다른 소프트웨어 기반 부 채널 공격은 일부 페이지만 보는 대신, 캐시 라인 단위로 추적이 가능하다는 장점이 있다.

 

Athena는 모든 페이지를 확인하지 않는 부 채널 공격 방법에 대해서도 쉽게 적응할 수 있는데 그 이유는 다음과 같다.

• 공격자가 자신이 모니터링하고 있는 메모리 집합이 뭔지 알고있다
• 따라서 모든 메모리 접근에 대한 제약 조건을 모니터링된 페이지 집합으로 제한할 수 있다.

Athena는 가상 주소 뿐만 아니라 마이크로아키텍처 구조에서 작동하는 부 채널 공격을 지원하도록 확장될 수 있다.

 

이를 위해서는 모니터링되는 캐시 세트의 상태가 어떻게 변하는지 시뮬레이션해야한다. → 캐시의 동작 원리는 다 알고 있으니 구현이 문제다.

Dealing with Noise

제어 채널 공격과 다른 부 채널 공격의 차이점은, 후자는 노이즈에 취약하는거다.

예를 들어서, 캐시 공격은 FP나 FN의 영향을 받을 수 있다.

 

이런 공격들을 여러 번 반복하여 신뢰할 수 있는 정보를 추출하여 유의미한 수치를 내는걸 증명하기 위해 square-and-multiply 알고리즘에 대해 flush-reload 공격을 구현했고, 100개의 트레이스 중에 68개가 완전히 오류가 없었다. → 3번의 공격 후 majority vote 방식으로 오류가 없는 트레이스를 만들어낼 수 있다.

 

이렇게 노이즈가 심한 부 채널 공격에 대해서도 힘들긴 하지만 노이즈 없는 트레이스를 추출할 수 있기 때문에 Athena는 부 채널 공격이 아니더라도 사용될 수 있다.

Evaluation

이 섹션에서는 Athena에 초점을 맞춰서 SCASE를 다음에 맞춰 평가한다

1. 인공적인 트레이스를 사용하여 메모리 트레이스 기반 심볼릭 실행이 잘 수행되는지 평가
2. 실제 SGX 트레이스를 사용하여 Athena의 성능을 분석
3. 네 가지 추가적인 현실적인 사례를 통해 Athena를 평가

Efficiency of Secret Recovery

메모리 트레이스에 따른 Athena의 angr의 경로 탐색 능력을 평가한다.

 

비밀 값에 종속적인 jump table을 통해 제어 및 데이터 흐름 유출을 동시에 보이게 해, SEE에 미치는 영향을 통제되고 정밀한 방식으로 측정할 수 있다

• 대상 프로그램: 암호학적 대사에 미치는 영향을 보기 위해 square-and-multiply 알고리즘을 구현한 프로그램을 목표로 한다.
• 다양한 세밀도(granularity)의 메모리 트레이스를 생성할 수 있는 angr 기반 메모리 트레이싱 도구를 사용
• 32GB 메모리와 Intel Core i7-9700K CPU를 사용
• 점프 테이블은 16개의 항목을 가지고있고, 각 항목은 버퍼에 서로 다른 숫자 값을 작성하는 함수를 가리킨다.

💡

세밀도

코드 분석 단위. Athena에서는 일반적으로 4kB크기의 페이지 단위로 분석을 한다.

점프 테이블 실험에서는 다양한 세밀도로 측정을 진행

 

다음은 세밀도에 따른 Athena의 64바이트 비밀 값 복구 시간을 나타낸다. 각 데이터 포인트는 서로 다른 virtual random secret을 사용한 10회 실행의 평균값이다. Y축은 log scale이다

• 무시되는 비트가 많아질수록 (최대 12비트, 4kB 페이지의 오프셋값) 실행시간은 지수함수적으로 증가.
• Athena의 실행 시간은 대부분 path exploration 단계에서 소요되었으며, solving 단계에서의 시간은 무시할 수 있는 수준
• 메모리 트레이스에 정보가 많을수록 SEE가 state를 더 효과적으로 잘라낼 수 있기 때문이다.

다음은 비밀 값의 길이에 따른 Athena의 복구 능력을 테스트했다. 마찬가지로 Y축은 로그스케일이다. 또한 이번에는 가이던스가 없는 일반적인 angr의 성능도 측정했다.

가이던스가 없는 경우에는 3바이트 키의 길이에도 불구하고 $10^3$초 내에 복구하는데 실패하였으며, 다른 모델의 경우 길이가 증가함에 따라 시간도 선형적으로 증가하는걸 보였다.

SGX Traces with Athena

Athena를 이용하여 square-and-multiply의 비밀 값을 복구하는걸 평가한다

• 8GB DRAM을 가진 Intel Core i3-7100T CPU에서 SGX 엔클레이브 실행
• 오프라인 단계는 104GB DRAM을 가진 Intel Core i9-12900K CPU에서 실행

그 결과 Athena는 10번의 실험 모두 100% 성공률로 비밀 값의 2048비트를 모두 복구해냈다.

• 평균 실행 시간: 195.7초
• 최소 실행 시간: 194.3초
• 최대 실행 시간: 196.8초
• 솔빙에 소요된 시간은 10ms 미만
• DRAM 사용량은 최대 62GB

Recovering AES S-Box Keys

OpenSSL의 AES S-Box를 대상으로 실험을 진행하고 AES 마스터 키를 복구해냈다.

💡

AES는 보통 AES라운드 또는 알고리즘의 단일 단계에 대해 미리 계산된 값을 가지고 있는 lookup table을 사용한다. (이걸 S-Box)라고 한다.

이 S-Box에서 조회되는 값은 마스터 키로부터 파생된 라운드 키에 의존하기 때문에 여기에 접근하는 것은 곧 마스터 키에 대한 정보를 유출한다는걸 의미.

 

S-Box는 크기가 256바이트이므로 매우 세밀하게 트레이스를 추출해야하며, 여러 라운드 키의 조합으로부터 마스터키를 재구성해야한다.

해당 결과는 정밀도에 따른 Athena 실행 시간과 복구율을 나타낸다.

• Athena가 데이터 흐름 트레이스만 추출했을 때, 결과는 동일하게 유지.
• 하지만 제어 흐름만 추출했을 때 제어 흐름이 어떤 비밀 값에도 의존하지 않기 때문에 복구에 실패.

여기서 복구되지 않은 나머지 비트들에 대해서 어느 비트가 복구되지 않았는지 알 수 있기 때문에 그 부분에만 bruteforce 기법을 시도해볼 수 있음.

Exploiting OpenSSL’s Binary Extended Euclidean Algorithm

다음 타겟은 OpenSSL의 BEEA (Binary Extended Euclidean Algorithm)이다.

BEEA는 RSA, DSA< ECDSA와 같은 암호화 알고리즘의 키 생성 과정에 사용되는 알고리즘이다.

 

Athena는 구체적인 비밀 값에 따라 수 시간에서 수 일 내에 비밀 입력값을 복구했다.

 

대신, 데이터 흐름 트레이스만, 또는 제어 흐름 트레이스만 사용했을 때 두 경우 모두 비밀 값을 복구하지 못했으며, 이를 통해 두 유형의 트레이스를 결합하는 것이 유익하다는 점을 확인할 수 있음.

• 8-a) SEE에서 동시에 활성화된 state의 수. 1에서 10 사이를 진동하는 모습을 확인할 수 있음.
  • 누출된 정보에 의해 추가된 제약 조건이 state를 줄이는데 도움이 되는걸 확인할 수 있었음
• 8-b) 그렇게 줄어든 state는 탐색 횟수가 증가함에 따라 꾸준히 증가함.

시간에 지남에 따라 데이터 흐름의 제약 조건의 양이 증가하는걸 확인할 수 있다.

Attacking RC4 KSA

부 채널 노출을 이용해서 RC4 KSA에 대한 전체 키 복구를 보여주는건 처음이다.

 

Athena는 lookup table 접근에 의해 발생하는 누출로부터 비밀 키를 자동으로 북구한다.

 

RC4의 비밀 값을 추출하기 위해서는 매우 세밀한 누출 정보가 필요하기 때문에 바이트 단위의 데이터 흐름 트레이스는 수동으로 추출했지만, 키를 복구하는 과정은 자동으로 이루어졌다.

• Intel Core i7-1165G7 CPU와 16GB RAM의 일반 노트북에서 키를 100% 복구
• 평균 복구 시간: 4분 35초
• 솔빙 단계에서 소요된 시간: 10ms 미만

Recovering Poker Cards

보안적인 타겟 (암호 키) 뿐만 아니라 복잡한 데이터 구조를 가진 소프트웨어에서도 비밀 정보를 캐낼 수 있음을 보여줬다.

Discussion

Related Work

Machine Learning for Side-Channel Attack Automation

머신러닝 기반 방식은 확률론적이고 정확도가 낮은 반면에, Athena는 결정론적이며 정확도도 매우 높다.

 

또한 부 채널 공격은 환경마다 노이즈가 다른데, ML은 단순히 학습한 데이터를 가지고 추론하여 실제 트레이스에서는 무너지는 반면에, Athena는 심볼릭 실행을 따르므로 더 robust하다

Symbolic Execution for Side-Channel Attack Automation

• phan et al. 은 부 채널 누출을 최대화하기 위한 입력값 생성을 자동화하는 방식
• Athena는 트레이스를 보고 비밀 값을 재구성하는 방식.
• Dubrova는 딥러닝 기반의 power 분석과 SAT 솔빙을 결합하여 AES-128만을 공격.
• Athena는 일반적인 바이너리의 메모리 접근 트레이스로 제약 조건 생성을 자동화.

Differential Fault Analysis

• 기존 방식은 프로그램이 루프를 돌면서 같은 조건에 따라 서로 다른 메모리 접근 패턴을 보일때만 유효.
• Athena는 루프가 아니라도 한 번의 메모리 접근이 비밀 값과 연관된 제약 조건을 만들어낼 수 있음.

Limitations

1. 화이트박스를 가정
   • 바이너리나 코드가 있어야한다는 한계. 하지만 Kerckhoff의 원칙에 따르면 공격자는 모르는 게 없기때문에 정당한 보안 모델.
2. SAT 솔버의 물리적 한계
   • 암호 알고리즘 자체가 부 채널 정보와 키 사이의 관계를 수학적으로 복잡하다면 타임아웃이 발생함
3. 데이터 의존성
   • 정보 누출이 없다면 비밀 키를 복구할 수 없다
4. 단일 실행의 한계
   • 현재 Athena는 한 번 실행해서 나온 트레이스를 분석하는데 최적화되어있다.
   • 여러 번 입력을 바꾸는 Interactive Attack은 수동 작업이 많이 필요하다.

Conclusion

부 채널 공격으로부터 비밀 키를 추론하는 SCASE는 부 채널 트레이스를 통해 SEE를 가이드 하는 방식이다.

 

이를 선보이기 위해 SGX 엔클레이브를 타겟으로 하는 PoC 구현체인 Athena를 배라했으며 여러 알고리즘에 대해서 비밀 키를 복구하였다. 

 

이 뿐만 아니라 다른 복잡한 구조의 알고리즘에서도 값을 복구할 수 있음을 보였으며 이 기술이 대상 어플리케이션에 대한 깊은 이해 없이 비밀 값을 복구하는데에 있어 실용적이다.

 

후기

부 채널 공격이 어떻게 이루어지는지, 또 어떻게 심볼릭 실행을 사용하는지 알 수 있었다.

 

fuzzolic에서는 솔버가 퍼징의 원리를 적용했다면 SCASE는 부 채널 트레이스를 통해 솔버에게 정확한 제약 조건 값을 줌으로써 path explosion을 방지했다.

 

그러면 퍼징시에 multi-byte 조건문을 통과하기 힘든데, 이 때 트레이스를 제공하는걸로도 우회가 가능할거같다.