자세한 기술 설명: Ant Group의 HyperEnclave에 대한 CertiK의 고급 공식 검증
지난주 CertiK는 Ant Group의 신뢰할 수 있는 기본 기술 팀이 개발한 혁신적이고 개방적인 크로스 플랫폼 TEE(Trusted Execution Environment)인 HyperEnclave의 고급 공식 검증을 완료했다고 발표했습니다.
Web 3 세계를 보호한다는 사명을 달성하기 위해 CertiK는 감사 과정에서 다양한 분석 방법을 사용했습니다. 여기에는 인간 감사자의 상세하고 엄격한 코드 검토, 퍼즈 테스트 및 정적 분석을 통한 프로그램 버그 발견, 모델 검사를 사용한 표준 프로토콜에 대한 프로그램 정확성에 대한 수학적 증명이 포함되지만 이에 국한되지는 않습니다. 그 중 가장 강력한 것 중 하나는 기계로 검증된 증명(즉, 공식 검증)을 사용하는 것입니다.
공식 검증에는 모델 검사 사용과 같은 표준 속성의 자동화된 검증뿐만 아니라 특정 프로젝트에 대해 사용자 지정 보안 속성이 공식화되고 입증되는 고급 검증이 모두 포함됩니다.
아래 다이어그램에 표시된 것처럼 Web 3 애플리케이션은 소프트웨어 스택의 모든 구성 요소 계층에 의존합니다. 스마트 계약의 비즈니스 로직은 고급 프로그래밍 언어로 작성되고 바이트코드로 컴파일되며 블록체인 노드의 바이트코드 가상 머신에 의해 실행됩니다. 체인의 노드는 특정 코드를 실행하여 서약 및 합의 알고리즘과 같은 구성을 계산합니다. 또한 블록체인 노드는 운영 체제, 가상 머신 모니터 및 신뢰할 수 있는 실행 환경과 같은 시스템 소프트웨어를 포함하는 물리적 클라우드 인프라에서 실행됩니다.
Web 3의 보안을 논의할 때 사람들은 종종 소프트웨어 스택의 최상위에 있는 스마트 계약에 초점을 맞춥니다. 하위 계층의 소프트웨어 구성 요소는 여러 다른 Web 3 애플리케이션에서 공유되므로 테스트가 더 많이 이루어지고 버그가 발생할 가능성이 줄어듭니다.
그러나 동시에 이는 더욱 중요합니다. 블록체인 노드 코드의 버그는 해당 블록체인의 모든 애플리케이션을 위험에 빠뜨릴 수 있고 시스템 인프라의 버그는 전체 Web 3 세계를 위험에 빠뜨릴 수 있습니다.
기계 검증 증명에 대한 CertiK의 작업은 Web 3 소프트웨어 스택의 모든 계층을 포괄합니다. 예를 들어:
우리는 표준 인터페이스를 구현하는 ERC-20 계약 및 기타 Solidity 계약을 자동으로 확인하기 위해 기호 모델 검사를 사용합니다.
UniSwap과 같은 DeFi 애플리케이션에 대한 스마트 계약을 확인했고, 공식 검증은 Move 및 Cardano에 대한 계약 감사의 일부였으며 일부 Solidity 프로젝트에 대한 사용자 정의 속성을 확인했습니다.
DeepSEA 검증 컴파일러는 컴파일 중 오류를 제거하도록 설계되었습니다.
Cosmos SDK의 표준 뱅크 모듈을 공식적으로 검증했습니다.
TON Chain의 메인체인 서약 계약을 공식적으로 확인했습니다.
첫 번째 수준 제목
HyperEnclave 신뢰할 수 있는 실행 환경
TEE(신뢰할 수 있는 실행 환경)는 가장 까다로운 공격 유형 중 하나, 즉 컴퓨터 운영 체제를 제어할 수도 있는 공격으로부터 애플리케이션을 보호하도록 설계되었습니다.
가장 주목할만한 TEE로는 Intel의 SGX, Arm TrustZone 및 AMD SEV가 있습니다. 이는 CPU가 특정 보안 애플리케이션(엔클레이브)이 로드되었음을 암호화 방식으로 증명하고 다른 소프트웨어가 이를 방해하지 못하도록 방지함으로써 작동합니다.
TEE는 디지털 생활의 여러 측면에 통합되었습니다. Apple의 FileVault와 같은 디스크 암호화 소프트웨어와 Google Authenticator와 같은 2단계 인증 앱은 키를 TEE에 저장하므로 누군가 노트북이나 휴대폰을 훔쳐 분해하더라도 키를 보호할 수 있습니다.
동시에 Web 3에서는 TEE도 점점 더 중요해지고 있습니다. 암호화폐 지갑은 또한 TEE를 사용하여 암호화 키를 보다 안전하게 저장합니다. 분산형 블록체인 오라클은 TEE를 사용하여 데이터의 신뢰성과 신뢰성을 높일 수 있습니다. 영지식 증명 구현 오류를 복구하는 데 도움이 되도록 2-of-3 시스템에 TEE를 사용하라는 제안이 있습니다.
LucidiTEE, SubstraTEE, Oasis Network 및 AntChain과 같은 일부 블록체인 프로젝트도 TEE를 사용하여 사용자에게 데이터 개인 정보 보호를 제공하도록 제안합니다.
현재 대부분의 TEE는 비공개 소스이며 특정 하드웨어 공급업체에 연결되어 있습니다. 예를 들어, Intel SGX를 사용하려면 애플리케이션이 Intel CPU에서 실행되어야 하며 Intel의 승인 및 화이트리스트에 포함되어야 합니다. 그러나 하드웨어 개발은 본질적으로 느리기 때문에 TEE의 기능 세트가 더 적고 보안 문제로 인해 CPU 펌웨어를 업데이트해야 합니다. 이와 대조적으로 HyperEnclave는 널리 사용되는 두 가지 하드웨어 기능을 활용하여 대부분 소프트웨어로 구현됩니다.
먼저, 컴퓨터의 신뢰할 수 있는 플랫폼 모듈(TPM, UEFI 보안 부팅을 구현하는 데 일반적으로 사용됨)을 사용하여 HyperEnclave 및 특정 보안 Enclave 집합(Enclave)이 실행 중인지 확인합니다. 둘째, HyperEnclave는 CPU의 가상화 확장을 사용하여 엔클레이브를 보호합니다(일반적으로 VMware, VirtualBox, Hyper-V, KVM 등과 같은 가상 머신 모니터에서 사용됨). 컴퓨터 하드웨어의 경우 HyperEnclave는 다른 하이퍼바이저처럼 보이지만 엔클레이브의 경우 SGX용으로 작성된 애플리케이션이 HyperEnclave에서 실행되도록 쉽게 조정할 수 있는 SGX 호환 API를 제공합니다. 표준 가상화 기술을 사용하면 운영 체제와 긴밀하게 상호 작용하는 고성능 애플리케이션을 쉽게 지원할 수 있습니다.
HyperEnclave의 가장 중요한 부분은 RustMonitor라는 모니터로, 다른 엔클레이브 및 운영 체제의 위험으로부터 엔클레이브를 보호합니다. 가상화된 엔클레이브 및 OS"guest"모드는 메모리에 액세스하려고 할 때마다 액세스된 메모리 주소가 먼저 RustMonitor가 관리하는 페이지 테이블을 통해 변환됨을 의미합니다. RustMonitor는 엔클레이브를 물리적 메모리의 다른 영역에 배치함으로써 다른 엔클레이브가 소유한 데이터를 읽거나 덮어쓰지 못하도록 보장할 수 있습니다. 그러나 이는 단순한 정적 분리일 수 없습니다. 엔클레이브가 운영 체제와 통신하려면 일부 메모리 주소가 겹치도록 허용해야 하며 페이지 나누기가 처리될 때 주소 맵이 업데이트됩니다.
HyperEnclave 개발자는 메모리 주소 매핑 테이블이 작동하는 방식을 정의하는 페이지 테이블이 준수해야 하는 고정 속성 집합을 작성했습니다. 예를 들어, 여기에는 가상 주소가 ELRANGE에 있는 경우에만 EPC의 물리적 페이지에 매핑됩니다와 같은 속성이 포함됩니다. 자세한 특성은 정식 검증 보고서를 참조하시기 바랍니다. 이러한 조건을 위반하는 오류는 전체 HyperEnclave 시스템의 보안 보장을 무효화할 수 있습니다.
첫 번째 수준 제목
HyperEnclave의 RustMonitor에 대한 공식 검증
RustMonitor의 페이지 테이블 관리 코드는 작고 안전이 중요하기 때문에 검증하기에 좋은 대상입니다. Web 3 스마트 계약의 경우와 유사하게 공식적인 검증에 노력을 기울이는 것이 가능합니다. 이 프로젝트에서 CertiK는 페이지 테이블이 준수해야 하는 불변 속성으로 시작하여 이를 영어에서 Coq 공식 사양 언어로 변환합니다. 그런 다음 RustMonitor 코드가 테이블을 수정할 때 결과 테이블이 여전히 모든 불변 속성을 충족한다는 기계 검사 증명을 생성합니다.
사실, 우리의 개발 작업은 더 나아가서 이러한 불변의 설계가 올바른지, Coq 언어 번역이 올바른지 확인하고 싶기 때문입니다. 이를 위해 클라이언트 코드가 관찰할 수 있어야 하는 정보를 Coq에 추가로 지정하고 불변 속성을 사용하여 다른 정보 흐름이 없음을 증명합니다("무관 정리"). 이러한 모든 증명을 종합하면 페이지 테이블 관리가 설계와 구현 모두에서 올바르다는 강력한 보증을 제공합니다.
그러나 TEE 모니터링 프로그램의 정확성을 입증하는 것은 간단한 작업이 아닙니다. 가상화 모니터 및 운영 체제 커널과 같은 시스템 수준 프로그램은 포인터가 있는 데이터 구조와 관련된 하위 수준 코드를 많이 사용하고 유형 추상화를 건너뛰며 성능에 고도로 최적화되어 있습니다. 오늘날까지도 이러한 프로그램의 검증은 최고의 컴퓨터 과학 저널에 출판할 가치가 있는 뜨거운 연구 문제로 남아 있으며, 각 코드 줄을 입증하려면 엄청난 노력이 필요합니다.
예를 들어 seL 4의 초기 증명에는 20인년이 걸렸고, 코모도는 약 650줄의 C 코드에 해당하는 어셈블리 코드를 검증하는 데 2인년이 걸렸다. 이러한 프로젝트의 코드는 이미 프로덕션 단계에 있고 Rust 관용어로 작성된 HyperEnclave와는 달리 확인을 단순화하기 위해 특별히 다시 작성되었습니다. 최신 기술을 기반으로 모든 코드를 검증하는 것은 경제적으로 비현실적입니다. 또 다른 문제는 Rust의 검증 툴체인이 다른 프로그래밍 언어에 비해 성숙하지 않다는 것입니다. 실제 코드 대신 수동으로 모델 코드를 작성하면 유효성 검사 부담을 줄일 수 있습니다. 검증 연구 프로젝트인 Sanctum TEE가 그 예입니다. 이 접근 방식의 단점은 코드와 추상 모델 간의 불일치로 인해 모델의 안전성이나 정확성 속성이 약화되거나 심지어 무효화될 수도 있다는 것입니다.
CertiK는 이 문제를 해결할 수 있는 독보적인 위치에 있습니다. 창립자 두 분, Shao Zhong 교수와 Gu Ronghui 교수는 CCAL(Concurrent Certification Abstraction Layer) 검증 방법을 창안한 사람들로, 이 방법을 사용하여 세계 최초 동시 인증 운영 체제 커널 CertiKOS를 검증했으며, 검증된 KVM 가상화 모니터 seKVM 및 ARM 기밀 컴퓨팅 아키텍처. CCAL의 기본 아이디어는 프로그램의 모든 기능을 여러 레이어로 나누고 각 레이어에 대한 추상 모델을 작성한 다음 함수의 실제 코드가 추상 모델을 구현한다는 것을 증명하는 것입니다. 코드가 추상 모델의 동작과 일치하지 않습니다. 계층화된 접근 방식은 전체 프로그램을 단일 단일체로 확인하는 것보다 코드 증명 및 동시성 문제를 더 쉽게 처리합니다. seKVM 및 Arm CCA에 대한 이전 작업은 이전에 공식 검증하기에는 너무 컸던 산업 규모의 시스템 소프트웨어 프로젝트를 검증하는 데 관심을 끌었습니다.
HyperEnclave 정식 검증팀에는 이전에 CertiKOS 및 seKVM 검증에 참여한 사람들이 포함되어 있으며, 이러한 경험을 활용하여 보안 보증과 검증 리소스 간의 균형을 잘 맞추려고 노력합니다. 이를 위해 우리는 CCAL 사양을 기반으로 한 탄력적인 검증 접근 방식을 사용했습니다. 우리 프레임워크는 함수 코드가 모델을 준수하는지 검증하는 것을 지원하지만 함수의 하위 집합(메모리 페이지를 직접 처리하는 49개 함수)에서만 이 검증을 수행하기로 선택했습니다. 테이블). 다른 기능의 경우, 우리는 Rust 코드의 손으로 만든 Coq 번역이 정확하다고 가정하고 이러한 Coq 모델의 기능적 정확성만 증명합니다. 여기 소스 코드에서 액세스되는 데이터 구조의 추상화 수준에 따라 각 함수의 코드가 모델을 준수하는지 확인해야 하는지 여부가 결정됩니다. HyperEnclave가 높은 수준의 Rust 데이터 구조를 사용하는 경우 이를 Coq로 직접 변환하지만, 낮은 수준의 바이트 기반 페이지 테이블 형식을 사용하는 경우에는 높은 수준의 기능 모델과의 동등성을 입증하기 위해 더 많은 노력을 기울입니다. 공식 검증 보고서). RustMonitor의 경우 이는 페이지 테이블 표현을 처리하는 Memory 모듈을 코드 증명하고 enclave 상태를 관리하는 Enclave 모듈에 대한 추상 모델을 사용한 다음 모든 결과 모델을 결합하여 불변 정리와 최상위 보안 정리.
이 검증의 또 다른 흥미로운 부분은 코드 증명이 수행되는 방법입니다. 페이지 테이블을 처리하는 HyperEnclave 코드는 하위 수준 코드이며 기존 검증 도구 중 어느 것도 이를 잘 처리하지 못합니다. 이를 위해 우리는 Rust 코드를 중간 언어인 MIR(Mid-level Intermediate Representation)로 변환하여 검증하고, 이를 사용하여 해당 핵심 기능을 검증하는 프레임워크를 개발했습니다. MIR은 작은 언어이기 때문에 이에 대한 정확한 작동 의미 체계를 작성하고 컴파일러에서 생성된 MIR 코드의 정밀한 검증을 수행할 수 있습니다. 이를 통해 우리의 코드 증명은 .
요약하다
요약하다
TEE(신뢰할 수 있는 실행 환경)는 클라우드 컴퓨팅 및 Web 3 애플리케이션의 기본 기술이므로 보안을 구축하는 것이 중요합니다. 이 프로젝트에서 CertiK는 가장 중요한 구성 요소를 검증하기 위해 고급 공식 검증 기술을 적용하여 코드가 예상대로 작동하고 실제로 원하는 보안 속성을 충족한다는 강력한 보증을 제공했습니다.
이러한 정식 검증 작업은 프라이빗 컴퓨팅 보안의 일부일 뿐이며 전체 시스템의 하나의 구성 요소인 RustMonitor의 페이지 테이블 관리 부분만 다루고 있습니다. 앞으로는 기타 개인 정보 보호 컴퓨팅 구성 요소에 대한 코드 검토, 테스트 및 공식 검증도 수행할 예정입니다. 핵심 부분의 검증을 통해 프라이버시 클라우드 컴퓨팅의 탄탄한 기반을 마련했습니다.
