คำอธิบายทางเทคนิคโดยละเอียด: การตรวจสอบ HyperEnclave ของ Ant Group อย่างเป็นทางการขั้นสูงของ CertiK
เมื่อสัปดาห์ที่แล้ว CertiK ประกาศว่าได้เสร็จสิ้นการตรวจสอบขั้นสูงอย่างเป็นทางการของ HyperEnclave ซึ่งเป็น Trusted Execution Environment (TEE) ข้ามแพลตฟอร์มที่เป็นนวัตกรรมและเปิดกว้าง ซึ่งพัฒนาโดยทีมงานเทคโนโลยีเนทิฟที่เชื่อถือได้ของ Ant Group
เพื่อให้บรรลุภารกิจในการรักษาความปลอดภัยให้กับโลกของ Web 3 CertiK ใช้วิธีการวิเคราะห์ที่หลากหลายในระหว่างกระบวนการตรวจสอบ ซึ่งรวมถึงแต่ไม่จำกัดเพียงการตรวจสอบโค้ดอย่างละเอียดและเข้มงวดโดยผู้ตรวจสอบที่เป็นมนุษย์ การค้นพบจุดบกพร่องของโปรแกรมผ่านการทดสอบฟัซซี่และการวิเคราะห์แบบคงที่ และการพิสูจน์ทางคณิตศาสตร์ของความถูกต้องของโปรแกรมสำหรับโปรโตคอลมาตรฐานโดยใช้การตรวจสอบแบบจำลอง หนึ่งในวิธีที่มีประสิทธิภาพมากที่สุดคือการใช้การพิสูจน์ด้วยเครื่อง (เช่น การตรวจสอบอย่างเป็นทางการ)
การตรวจสอบอย่างเป็นทางการรวมถึงการตรวจสอบคุณสมบัติมาตรฐานแบบอัตโนมัติ เช่น การใช้การตรวจสอบแบบจำลอง และการตรวจสอบขั้นสูงเพิ่มเติม ซึ่งคุณสมบัติความปลอดภัยแบบกำหนดเองได้รับการกำหนดและพิสูจน์แล้วสำหรับโครงการเฉพาะ
ดังที่แสดงในแผนภาพด้านล่าง แอปพลิเคชัน Web 3 อาศัยส่วนประกอบทุกเลเยอร์บนสแต็กซอฟต์แวร์ ตรรกะทางธุรกิจของสัญญาอัจฉริยะเขียนด้วยภาษาโปรแกรมระดับสูง คอมไพล์เป็นโค้ดไบต์ และรันโดยเครื่องเสมือน bytecode บนโหนดบล็อกเชน โหนดของห่วงโซ่ดำเนินการโค้ดเฉพาะเพื่อคำนวณการกำหนดค่า เช่น คำมั่นสัญญา และอัลกอริธึมที่เป็นเอกฉันท์ นอกจากนี้ โหนดบล็อกเชนยังทำงานบนโครงสร้างพื้นฐานบนคลาวด์ทางกายภาพ ซึ่งรวมถึงซอฟต์แวร์ระบบ เช่น ระบบปฏิบัติการ การตรวจสอบเครื่องเสมือน และสภาพแวดล้อมการดำเนินการที่เชื่อถือได้
เมื่อพูดถึงเรื่องความปลอดภัยสำหรับ Web 3 ผู้คนมักจะมุ่งเน้นไปที่สัญญาอัจฉริยะที่อยู่ด้านบนของกลุ่มซอฟต์แวร์ ส่วนประกอบซอฟต์แวร์ในระดับต่ำกว่าจะใช้ร่วมกันโดยแอปพลิเคชัน Web 3 ที่แตกต่างกัน ดังนั้นจึงได้รับการทดสอบมากกว่าและมีโอกาสน้อยที่จะมีจุดบกพร่อง
แต่ในขณะเดียวกัน สิ่งนี้ยังทำให้พวกเขามีความสำคัญมากยิ่งขึ้น: จุดบกพร่องในโค้ดของโหนดบล็อกเชนอาจเป็นอันตรายต่อแอปพลิเคชันทั้งหมดบนบล็อกเชนนั้น และจุดบกพร่องในโครงสร้างพื้นฐานของระบบอาจเป็นอันตรายต่อทั้งโลกของ Web 3
งานของ CertiK เกี่ยวกับการพิสูจน์ยืนยันด้วยเครื่องครอบคลุมทุกเลเยอร์ของซอฟต์แวร์ Stack ของ Web 3 ตัวอย่างเช่น:
เราใช้การตรวจสอบแบบจำลองเชิงสัญลักษณ์เพื่อตรวจสอบสัญญา ERC-20 และสัญญา Solidity อื่นๆ ที่ใช้อินเทอร์เฟซมาตรฐานโดยอัตโนมัติ
เราตรวจสอบสัญญาอัจฉริยะสำหรับแอปพลิเคชัน DeFi เช่น UniSwap การตรวจสอบอย่างเป็นทางการเป็นส่วนหนึ่งของการตรวจสอบสัญญาของเราสำหรับ Move และ Cardano และเราตรวจสอบคุณสมบัติที่กำหนดเองสำหรับโครงการ Solidity บางโครงการ
DeepSEA Validation Compiler ของเราได้รับการออกแบบมาเพื่อกำจัดข้อผิดพลาดระหว่างการคอมไพล์
เราได้ตรวจสอบโมดูลธนาคารมาตรฐานของ Cosmos SDK อย่างเป็นทางการ
เราได้ตรวจสอบสัญญาจำนำโซ่หลักของ TON Chain อย่างเป็นทางการ
ชื่อระดับแรก
สภาพแวดล้อมการดำเนินการที่เชื่อถือได้ของ HyperEnclave
Trusted Execution Environment (TEE) ได้รับการออกแบบมาเพื่อปกป้องแอปพลิเคชันจากการโจมตีประเภทที่ท้าทายที่สุดประเภทหนึ่ง: การโจมตีที่สามารถควบคุมระบบปฏิบัติการของคอมพิวเตอร์ได้
TEE ที่โดดเด่นที่สุดบางส่วน ได้แก่ SGX ของ Intel, Arm TrustZone และ AMD SEV ทำงานโดยให้ CPU พิสูจน์ด้วยการเข้ารหัสว่ามีการโหลดแอปพลิเคชันที่ปลอดภัยเฉพาะ (enclave) และป้องกันไม่ให้ซอฟต์แวร์อื่นรบกวนแอปพลิเคชันนั้น
TEE ได้รับการบูรณาการเข้ากับชีวิตดิจิทัลในหลาย ๆ ด้าน ซอฟต์แวร์เข้ารหัสดิสก์ เช่น FileVault ของ Apple และแอปตรวจสอบความถูกต้องสองขั้นตอน เช่น Google Authenticator จะจัดเก็บคีย์ไว้ใน TEE ดังนั้นแม้ว่าจะมีคนขโมยและแยกชิ้นส่วนแล็ปท็อปหรือโทรศัพท์ คีย์ก็สามารถป้องกันได้
ในขณะเดียวกัน ใน Web 3 TEE ก็มีความสำคัญมากขึ้นเรื่อยๆ กระเป๋าเงิน Cryptocurrency ยังใช้ TEE เพื่อจัดเก็บคีย์เข้ารหัสอย่างปลอดภัยยิ่งขึ้น ออราเคิลบล็อกเชนแบบกระจายสามารถใช้ TEE เพื่อเพิ่มความถูกต้องและความน่าเชื่อถือของข้อมูล มีข้อเสนอให้ใช้ TEE สำหรับ ระบบ 2 ใน 3 เพื่อช่วยกู้คืนจากข้อผิดพลาดในการดำเนินการพิสูจน์ความรู้เป็นศูนย์
นอกจากนี้ยังมีโปรเจ็กต์บล็อกเชนบางโปรเจ็กต์ เช่น LucidiTEE, SubstraTEE, Oasis Network และ AntChain ซึ่งเสนอให้ใช้ TEE เพื่อให้การปกป้องความเป็นส่วนตัวของข้อมูลสำหรับผู้ใช้
ปัจจุบัน TEE ส่วนใหญ่เป็นแหล่งที่มาแบบปิดและเชื่อมโยงกับผู้จำหน่ายฮาร์ดแวร์รายใดรายหนึ่ง ตัวอย่างเช่น หากต้องการใช้ Intel SGX แอปพลิเคชันจะต้องทำงานบน CPU ของ Intel และได้รับการอนุมัติและอนุญาตพิเศษโดย Intel แต่การพัฒนาฮาร์ดแวร์นั้นช้ามาก ดังนั้น TEE จึงมีชุดฟีเจอร์ที่เล็กกว่า และปัญหาด้านความปลอดภัยจำเป็นต้องอัปเดตเฟิร์มแวร์ของ CPU ในทางตรงกันข้าม HyperEnclave ถูกนำมาใช้ในซอฟต์แวร์เป็นส่วนใหญ่ โดยใช้ประโยชน์จากความสามารถด้านฮาร์ดแวร์ที่มีอยู่อย่างกว้างขวางสองประการ
ขั้นแรก Trusted Platform Module (TPM) ของคอมพิวเตอร์ที่ใช้กันทั่วไปในการใช้ UEFI Secure Boot) จะถูกนำมาใช้เพื่อตรวจสอบว่า HyperEnclave และชุดของ Secure Enclaves (enclaves) เฉพาะกำลังทำงานอยู่ ประการที่สอง HyperEnclave ใช้ส่วนขยายการจำลองเสมือนของ CPU เพื่อปกป้องเครือข่าย (โดยทั่วไปจะใช้โดยการตรวจสอบเครื่องเสมือน เช่น VMware, VirtualBox, Hyper-V, KVM ฯลฯ) สำหรับฮาร์ดแวร์คอมพิวเตอร์ HyperEnclave ดูเหมือนไฮเปอร์ไวเซอร์อื่นๆ แต่สำหรับ Enclave นั้น มี API ที่เข้ากันได้กับ SGX ซึ่งช่วยให้แอปพลิเคชันที่เขียนขึ้นสำหรับ SGX สามารถปรับให้ทำงานบน HyperEnclave ได้อย่างง่ายดาย ด้วยการใช้เทคโนโลยีเวอร์ช่วลไลเซชั่นมาตรฐาน ทำให้สามารถรองรับแอพพลิเคชั่นประสิทธิภาพสูงที่มีการโต้ตอบกับระบบปฏิบัติการอย่างใกล้ชิดได้อย่างง่ายดาย
ส่วนที่สำคัญที่สุดของ HyperEnclave คือจอภาพที่เรียกว่า RustMonitor ซึ่งปกป้องวงล้อมจากอันตรายจากวงล้อมอื่นและจากระบบปฏิบัติการ วงล้อมและระบบปฏิบัติการในระบบเสมือนจริง"guest"โหมดซึ่งหมายความว่าทุกครั้งที่พวกเขาพยายามเข้าถึงหน่วยความจำ ที่อยู่หน่วยความจำที่เข้าถึงจะถูกแปลเป็นครั้งแรกผ่านตารางเพจที่จัดการโดย RustMonitor ด้วยการวางวงล้อมไว้ในภูมิภาคต่างๆ ของหน่วยความจำกายภาพ RustMonitor สามารถมั่นใจได้ว่าจะไม่สามารถอ่านหรือเขียนทับข้อมูลที่เป็นของวงล้อมอื่นได้ แต่นี่ไม่สามารถเป็นเพียงการแยกแบบคงที่ง่ายๆ ได้: ที่อยู่หน่วยความจำบางส่วนต้องได้รับอนุญาตให้ทับซ้อนกันเพื่อให้เครือข่ายสามารถสื่อสารกับระบบปฏิบัติการได้ และแผนผังที่อยู่จะได้รับการอัปเดตเมื่อมีการจัดการตัวแบ่งหน้า
นักพัฒนาของ HyperEnclave ได้เขียนชุด คุณสมบัติคงที่ที่ตารางเพจต้องปฏิบัติตาม ซึ่งกำหนดวิธีการทำงานของตารางการแมปที่อยู่หน่วยความจำ ซึ่งรวมถึง ตัวอย่างเช่น คุณลักษณะ เช่น ที่อยู่เสมือนจะถูกแมปกับเพจจริงใน EPC หากอยู่ใน ELRANGE โปรดดูรายงานการตรวจสอบอย่างเป็นทางการสำหรับคุณสมบัติโดยละเอียด ข้อผิดพลาดใดๆ ที่ละเมิดเงื่อนไขเหล่านี้อาจทำให้การรับประกันความปลอดภัยของระบบ HyperEnclave ทั้งหมดเป็นโมฆะ
ชื่อระดับแรก
การตรวจสอบอย่างเป็นทางการของ RustMonitor ของ HyperEnclave
โค้ดการจัดการตารางเพจของ RustMonitor เป็นเป้าหมายที่ดีสำหรับการตรวจสอบ เนื่องจากโค้ดมีขนาดเล็กและมีความสำคัญด้านความปลอดภัย เช่นเดียวกับกรณีของสัญญาอัจฉริยะของ Web 3 มีความเป็นไปได้ที่จะพยายามตรวจสอบอย่างเป็นทางการ ในโปรเจ็กต์นี้ CertiK เริ่มต้นด้วยคุณสมบัติที่ไม่เปลี่ยนรูปซึ่งตารางเพจต้องปฏิบัติตามและแปลจากภาษาอังกฤษเป็นภาษาข้อกำหนดอย่างเป็นทางการของ Coq จากนั้นเราจะสร้างหลักฐานที่ตรวจสอบด้วยเครื่องว่าเมื่อโค้ด RustMonitor แก้ไขตาราง ตารางผลลัพธ์จะยังคงเป็นไปตามคุณสมบัติที่ไม่แปรเปลี่ยนทั้งหมด
ในความเป็นจริง งานพัฒนาของเราดำเนินต่อไป เนื่องจากเราต้องการให้แน่ใจว่าการออกแบบค่าคงที่เหล่านี้ถูกต้อง และการแปลภาษา Coq ของเรานั้นถูกต้อง ด้วยเหตุนี้ เราจึงระบุเพิ่มเติมใน Coq ถึงข้อมูลที่โค้ดไคลเอ็นต์ควรสามารถสังเกตได้ และใช้คุณสมบัติที่ไม่แปรเปลี่ยนเพื่อพิสูจน์ว่าจะไม่มีการไหลของข้อมูลอื่น ("ทฤษฎีบทความไม่เกี่ยวข้อง"). หลักฐานทั้งหมดนี้นำมารวมกันเป็นการรับประกันว่าการจัดการตารางเพจนั้นถูกต้องทั้งโดยการออกแบบและโดยการนำไปปฏิบัติ
อย่างไรก็ตาม การพิสูจน์ความถูกต้องของโปรแกรมติดตาม TEE ไม่ใช่เรื่องเล็กน้อย โปรแกรมระดับระบบ เช่น เครื่องมอนิเตอร์การจำลองเสมือนและเคอร์เนลของระบบปฏิบัติการใช้โค้ดระดับต่ำอย่างหนักซึ่งเกี่ยวข้องกับโครงสร้างข้อมูลด้วยพอยน์เตอร์ ข้ามนามธรรมของประเภท และได้รับการปรับให้เหมาะสมที่สุดเพื่อประสิทธิภาพ จนถึงทุกวันนี้ การตรวจสอบโปรแกรมดังกล่าวยังคงเป็นปัญหาการวิจัยที่กำลังได้รับความนิยมซึ่งสมควรได้รับการตีพิมพ์ในวารสารวิทยาการคอมพิวเตอร์ชั้นนำ และการพิสูจน์ว่าโค้ดแต่ละบรรทัดต้องใช้ความพยายามอย่างมาก
ตัวอย่างเช่น การพิสูจน์เบื้องต้นของ seL 4 ใช้เวลา 20 คนต่อปี ในขณะที่โคโมโดใช้เวลา 2 คนต่อปีในการตรวจสอบรหัสการประกอบที่สอดคล้องกับรหัส C ประมาณ 650 บรรทัด รหัสในโครงการเหล่านี้ได้รับการเขียนใหม่โดยเฉพาะเพื่อทำให้การตรวจสอบง่ายขึ้น ซึ่งแตกต่างจาก HyperEnclave ซึ่งมีอยู่แล้วในการผลิตและเขียนด้วยสำนวน Rust เมื่อพิจารณาจากความทันสมัย การตรวจสอบโค้ดทั้งหมดจึงไม่สามารถทำได้ในเชิงเศรษฐกิจ ปัญหาอีกประการหนึ่งคือ toolchain การตรวจสอบของ Rust นั้นยังไม่สมบูรณ์เมื่อเทียบกับภาษาโปรแกรมอื่นๆ ภาระในการตรวจสอบสามารถบรรเทาลงได้โดยการเขียนโค้ด โมเดล ด้วยตนเองแทนโค้ดจริง ตัวอย่างคือ Sanctum TEE ซึ่งเป็นโครงการวิจัยการตรวจสอบความถูกต้อง ข้อเสียของแนวทางนี้คือความไม่ตรงกันระหว่างโค้ดและโมเดลนามธรรมอาจทำให้คุณสมบัติด้านความปลอดภัยหรือความถูกต้องเกี่ยวกับโมเดลลดลงหรือทำให้คุณสมบัติความถูกต้องไม่ถูกต้อง
CertiK อยู่ในตำแหน่งที่โดดเด่นในการแก้ปัญหานี้ ผู้ก่อตั้งสองคนของเรา ศาสตราจารย์ Shao Zhong และศาสตราจารย์ Gu Ronghui เป็นผู้คิดค้นวิธีการตรวจสอบ Concurrent Certification Abstraction Layer (CCAL) พวกเขาใช้วิธีนี้เพื่อตรวจสอบเคอร์เนลระบบปฏิบัติการที่ได้รับการรับรองพร้อมกันครั้งแรกของโลก CertiKOS และตรวจสอบ KVM virtualization monitor seKVM และ สถาปัตยกรรมคอมพิวเตอร์ที่เป็นความลับของ ARM แนวคิดพื้นฐานของ CCAL คือการแบ่งฟังก์ชันทั้งหมดในโปรแกรมออกเป็น เลเยอร์ จำนวนมาก เขียนโมเดลนามธรรมสำหรับแต่ละเลเยอร์ จากนั้นพิสูจน์ว่าโค้ดจริงของฟังก์ชันใช้โมเดลนามธรรม ซึ่งจะช่วยลดความเสี่ยงของ รหัสไม่ตรงกับพฤติกรรมของโมเดลนามธรรม วิธีการแบบเป็นชั้นจะจัดการกับปัญหาการพิสูจน์โค้ดและปัญหาการทำงานพร้อมกันได้ง่ายกว่าการพยายามตรวจสอบโปรแกรมทั้งหมดเป็นหินใหญ่ก้อนเดียว งานก่อนหน้านี้เกี่ยวกับ seKVM และ Arm CCA ได้ดึงความสนใจไปที่การตรวจสอบโครงการซอฟต์แวร์ระบบระดับอุตสาหกรรมที่ก่อนหน้านี้มีขนาดใหญ่เกินไปสำหรับการตรวจสอบอย่างเป็นทางการ
ทีมการตรวจสอบอย่างเป็นทางการของ HyperEnclave ประกอบด้วยผู้ที่เคยเข้าร่วมในการตรวจสอบ CertiKOS และ seKVM มาก่อน และเราพยายามใช้ประสบการณ์นี้เพื่อสร้างสมดุลที่ดีระหว่างการประกันความปลอดภัยและทรัพยากรการตรวจสอบ ในการดำเนินการนี้ เราใช้วิธีการตรวจสอบแบบยืดหยุ่นตามข้อกำหนด CCAL: เฟรมเวิร์กของเรารองรับการตรวจสอบว่าโค้ดฟังก์ชันสอดคล้องกับโมเดล แต่เราเลือกที่จะดำเนินการตรวจสอบนี้กับชุดย่อยของฟังก์ชันเท่านั้น (ฟังก์ชัน 49 รายการที่เกี่ยวข้องกับหน้าหน่วยความจำโดยตรง ตาราง) สำหรับฟังก์ชันอื่นๆ เราถือว่าการแปล Coq ของโค้ด Rust ที่ประดิษฐ์ขึ้นด้วยมือนั้นถูกต้อง และเพียงพิสูจน์ความถูกต้องในการทำงานของโมเดล Coq เหล่านี้เท่านั้น ระดับนามธรรมของโครงสร้างข้อมูลที่เข้าถึงในซอร์สโค้ดที่นี่จะกำหนดว่าแต่ละฟังก์ชันจำเป็นต้องตรวจสอบว่าโค้ดนั้นสอดคล้องกับโมเดลหรือไม่ เมื่อ HyperEnclave ใช้โครงสร้างข้อมูล Rust ระดับสูง เราจะแปลโครงสร้างเหล่านั้นเป็น Coq โดยตรง แต่เมื่อใช้รูปแบบตารางเพจแบบไบต์ระดับต่ำ เราจะใช้ความพยายามมากขึ้นในการพิสูจน์ความเทียบเท่ากับโมเดลการทำงานระดับสูง (ดูเต็ม รายงานการตรวจสอบอย่างเป็นทางการ) ในกรณีของ RustMonitor หมายความว่าเราโค้ดพิสูจน์โมดูล หน่วยความจำ ที่จัดการการแสดงตารางเพจ ใช้โมเดลนามธรรมสำหรับโมดูล Enclave ที่จัดการสถานะวงล้อม จากนั้นจึงรวมโมเดลผลลัพธ์ทั้งหมดเพื่อพิสูจน์ทฤษฎีบทไม่แปรเปลี่ยนและ ทฤษฎีบทความปลอดภัยระดับบนสุด
อีกส่วนที่น่าสนใจของการตรวจสอบนี้คือวิธีการพิสูจน์โค้ด รหัส HyperEnclave ที่จัดการตารางเพจเป็นโค้ดระดับต่ำ และไม่มีเครื่องมือตรวจสอบที่มีอยู่ใดที่สามารถจัดการได้ดี ด้วยเหตุนี้ เราได้พัฒนาเฟรมเวิร์กเพื่อตรวจสอบโค้ด Rust โดยการแปลงเป็นภาษากลาง MIR (การเป็นตัวแทนระดับกลางระดับกลาง) และใช้เพื่อตรวจสอบฟังก์ชันหลักเหล่านั้น เนื่องจาก MIR เป็นภาษาขนาดเล็ก เราจึงสามารถเขียนความหมายเชิงปฏิบัติการที่แม่นยำได้ และทำการตรวจสอบโค้ด MIR ที่สร้างโดยคอมไพเลอร์ได้อย่างแม่นยำ ซึ่งช่วยให้การพิสูจน์โค้ดของเรามีรากฐานที่มั่นคงมากกว่าการพึ่งพานักแปลโดยพลการ
สรุป
สรุป
Trusted Execution Environments (TEE) เป็นเทคโนโลยีพื้นฐานสำหรับการประมวลผลบนคลาวด์และแอปพลิเคชัน Web 3 ดังนั้นการสร้างความปลอดภัยจึงเป็นสิ่งสำคัญ สำหรับโปรเจ็กต์นี้ CertiK ใช้เทคนิคการตรวจสอบอย่างเป็นทางการขั้นสูงเพื่อตรวจสอบส่วนประกอบที่สำคัญที่สุด โดยให้การรับประกันอย่างแน่นหนาว่าโค้ดทำงานตามที่คาดหวังและตรงตามคุณสมบัติความปลอดภัยที่ต้องการอย่างแท้จริง
งานตรวจสอบอย่างเป็นทางการนี้เป็นเพียงส่วนหนึ่งของการรักษาความปลอดภัยของคอมพิวเตอร์ส่วนตัว โดยครอบคลุมเฉพาะส่วนการจัดการตารางเพจของ RustMonitor ซึ่งเป็นเพียงองค์ประกอบเดียวในระบบโดยรวม ในอนาคต เราจะดำเนินการตรวจสอบโค้ด ทดสอบ และยืนยันองค์ประกอบการประมวลผลความเป็นส่วนตัวอื่นๆ อย่างเป็นทางการ ด้วยการตรวจสอบส่วนหลัก เราได้วางรากฐานที่มั่นคงสำหรับการประมวลผลบนคลาวด์เพื่อความเป็นส่วนตัว
