거대한, 북적이는 초고층 빌딩(클라우드)을 상상해 보세요. 이곳에는 수백 개의 서로 다른 기업(테넌트)들이 사무실 층을 임대하고 있습니다. 일반적인 건물에서는 건물 관리인(하이퍼바이저)이 모든 문을 열 수 있고, 모든 금고를 들여다볼 수 있으며, 모든 책상 위의 서류를 읽을 수 있는 마스터 키를 가지고 있습니다. 만약 관리인이 정직하다면 모두가 괜찮을 것입니다. 하지만 만약 관리인이 스파이이거나 해킹을 당한다면 어떻게 될까요? 갑자기 모든 회사의 비밀이 위험에 처하게 됩니다.

이를 해결하기 위해 기업들은 건물 내부에 **보안 방(Secure Rooms)**을 만들기 시작했습니다. 이것들은 **신뢰 실행 환경(Trusted Execution Environments, TEE)**이라고 불립니다. 특히, 이 논문은 AMD SEV(Secure Encrypted Virtualization)라고 불리는 고도의 기술이 적용된 버전의 방에 초점을 맞춥니다.

연구진이 수행한 작업은 다음과 같이 쉽게 설명할 수 있습니다.

1. 문제점: "믿어달라"는 말만으로는 부족하다

AMD SEV 기술는 벽이 투명하지만 깨지지 않는 유리로 만들어진 초보안 사무실과 같습니다. 건물 관리인(하이퍼바이저)조차 내부를 들여다보거나 손을 댈 수 없습니다. 컴퓨터 하드웨어 자체가 데이터를 암호화하기 때문에, 누군가 하드 드라이브를 훔치려 해도 그저 뒤섞인 암호문 덩어리만을 얻게 될 뿐입니다.

하지만 이 방을 만든 사람들은 이 방이 어떻게 작동하는지 설명하는 매뉴얼(사양서)을 작성했습니다. 그러나 매뉴얼은 단지 종이 위의 글자일 뿐입니다. 그것이 방이 실제로 안전하다는 것을 증명하지는 않습니다. 유리벽에 아주 작은 틈이 있을 수도 있고, 설계자가 언급하는 것을 잊어버린 비밀 문이 있을 수도 있습니다. 보안의 세계에서 "우리는 안전하다고 생각한다"는 것은 충분하지 않습니다. 수학적 증명이 필요합니다.

2. 해결책: "수학적 청사진"

저자들은 추측하는 것을 멈추고 증명하기로 했습니다. 그들은 **형식 검증 프레임워크(formal verification framework)**를 구축했습니다.

이것은 건물의 그림을 그리는 것에 그치지 않고, 건물의 완벽한 수학적 시뮬레이션을 만드는 건축가와 같습니다. 그런 다음, 이 시뮬레이션에 '디지털 스트레스 테스트'를 실시하여 어떤 가능한 공격에도 무너지지 않는지 확인합니다.

그들은 두 가지 주요 방식으로 이 작업을 수행했습니다:

• 설계 추상화(Design Abstraction): 그들은 AMD SEV의 복잡하고 무질서한 기술 매뉴얼을 깔끔하고 단순화된 수학적 모델로 변환했습니다. 이는 500페이지짜리 지침서를 명확한 순서도로 바꾸는 것과 같습니다.
• 속성 검사(Property Checking): 그들은 방이 안전하다고 간주되기 위해 반드시 따라야 하는 "규칙"(속성) 목록을 작성했습니다. 그런 다음, 컴퓨터 프로그램(Rosette이라 불림)을 사용하여 수학적 모델이 이 규칙을 위반하는 경우가 있는지 확인했습니다.

3. 게임의 세 가지 규칙 (CIA)

연구진은 CIA라고 알려진 세 가지 주요 목표를 기준으로 AMD SEV 방의 보안을 점검했습니다.

• 기밀성 (Confidentiality, "비밀 유지자"):

  • 규칙: 건물 관리인을 포함한 그 누구도 내부에서 일어나는 일을 읽을 수 없어야 합니다.
  • 테스트: 내부를 엿보려는 스파이를 시뮬레이션했습니다. 스파이가 게스트의 "프라이빗 메모리"나 "CPU 레지스터"(컴퓨터의 뇌)를 볼 수 있는지 확인했습니다.
  • 결과: 14가지 서로 다른 규칙을 검증했습니다. 수학적으로, AMD 하드웨어가 설계대로 작동하는 한 스파이는 비밀을 볼 수 없음을 증명했습니다.

• 무결성 (Integrity, "변조 방지 봉인"):

  • 규칙: 아무도 방 안의 문서를 몰래 수정하거나 가짜 문서로 교체할 수 없어야 합니다.
  • 테스트: 게스트의 코드를 재작성하거나 시스템을 속여 오래되고 취약한 버전의 소프트웨어가 현재 버전인 것처럼 속이려는 사보타주 공격자를 시뮬레이션했습니다.
  • 결과: 7가지 규칙을 검증했습니다. 수학적 결과, 시스템은 "역방향 맵 테이블"(엄격한 보안 로그와 같은 역할)을 가지고 있어 누군가가 페이지를 바꾸거나 시간을 되돌려 보안이 취약한 상태로 만드는 것을 방지함을 보여주었습니다.

• 가용성 (Availability, "전원 스위치"):

  • 규칙: 방은 당신이 필요할 때 작동해야 하며, 건물 관리인은 필요할 경우 이를 끌 수 있어야 합니다.
  • 테스트: 두 가지를 확인했습니다:
    1. 관리자가 항상 제어권을 되찾을 수 있는가? 예. 수학적으로 관리자는 항상 게스트를 일시 중지하거나 중단할 수 있음이 증명되었습니다.
    2. 게스트가 시간 부족 없이 항상 실행될 수 있는가? 아니요. 수학적으로 관리인이 악의적이라면, 게스트를 실행되지 않도록 선택할 수 있다는 것이 증ка되었습니다. 시스템은 관리자가 당신을 멈출 수 있다는 것은 보장하지만, 관리자가 당신을 실행시켜 줄 것이라는 것은 보장하지 않습니다. 이는 알려진 기술적 한계입니다.

4. 그들이 테스트한 "업그레이드"

이 논문은 단순히 기본 버전의 AMD SEV만 살펴본 것이 아닙니다. 더 강력한 두 가지 최신 업그레이드 버전도 테스트했습니다:

• SEV-ES: 컴퓨터의 "뇌"(CPU 레지스터)를 위한 보호 계층을 추가합니다. 이전에는 관리자가 컴퓨터가 일시 중지될 때 무엇을 생각하고 있었는지 볼 수 있었습니다. 이제는 그 생각조차 암호화됩니다.
• SEV-SNP: 메모리 페이지를 위한 "공증인" 시스템을 추가합니다. 이는 메모리 페이지가 올바른 사람의 소유이며 교체되거나 변조되지 않았음을 보장합니다.

5. 결론

연구진은 AMD SEV 시스템의 디지털 트윈을 성공적으로 구축했으며, 이를 23가지의 서로 다른 보안 테스트라는 가혹한 과정에 통과시켰습니다.

• 기밀성: 모든 테스트 통과.
• 무결성: 모든 테스트 통과.
• 가용성: 관리자의 제어권에 대한 테스트는 통과했으나, 게스트가 관리자가 자신을 실행하도록 강제할 수 없다는 점을 정확히 식별했습니다 (이는 버그가 아닌 설계상의 특징입니다).

요약하자면

이 논문은 고도의 기술이 집약된 금고를 가져와서, 그 금고의 완벽한 수학적 모델을 만들고, 수학의 법칙에 따라 건물 관리인이 그 금고를 열 수 없음을 세상에 증명한 법의학 엔지니어 팀과 같습니다. 그들은 단순히 "안전해 보인다"라고 말한 것이 아닙니다. "우리는 그것을 깨뜨릴 수 있는 모든 가능한 방법을 계산했으며, 그것이 깨질 수 없음을 증명했다"라고 말한 것입니다.

이는 클라우드 사용자들이 자신의 데이터가 안전하다는 것에 대해 훨씬 더 높은 수준의 확신을 가질 수 있게 해줍니다. 설령 클라우드 제공업체의 자체 소프트웨어가 해킹당하더라도 말입니다.