Giải thích kỹ thuật chi tiết: Xác minh chính thức nâng cao của CertiK đối với HyperEnclave của Ant Group

Tuần trước, CertiK thông báo rằng họ đã hoàn thành quá trình xác minh chính thức nâng cao của HyperEnclave, một Môi trường thực thi tin cậy (TEE) đa nền tảng sáng tạo và mở được phát triển bởi nhóm công nghệ bản địa đáng tin cậy của Ant Group.

Để đạt được sứ mệnh bảo mật thế giới Web 3, CertiK đã sử dụng nhiều phương pháp phân tích trong quá trình kiểm tra. Điều này bao gồm nhưng không giới hạn ở việc đánh giá mã chi tiết và nghiêm ngặt bởi con người, phát hiện lỗi chương trình thông qua kiểm tra lông tơ và phân tích tĩnh cũng như bằng chứng toán học về tính đúng đắn của chương trình đối với các giao thức chuẩn sử dụng kiểm tra mô hình. Một trong những cách hiệu quả nhất trong số này là việc sử dụng các bằng chứng được xác minh bằng máy (tức là xác minh chính thức).

Xác minh chính thức bao gồm cả xác minh tự động các thuộc tính tiêu chuẩn, chẳng hạn như sử dụng kiểm tra mô hình, cũng như xác minh nâng cao hơn, trong đó các thuộc tính bảo mật tùy chỉnh được xây dựng và chứng minh cho các dự án cụ thể.

Như được hiển thị trong sơ đồ bên dưới, ứng dụng Web 3 dựa trên tất cả các lớp thành phần trên ngăn xếp phần mềm của nó. Logic nghiệp vụ của hợp đồng thông minh được viết bằng ngôn ngữ lập trình cấp cao, được biên dịch thành mã byte và được điều hành bởi máy ảo mã byte trên nút blockchain. Các nút của chuỗi thực thi mã cụ thể của nó để tính toán các cấu hình như cam kết và thuật toán đồng thuận. Ngoài ra, các nút blockchain chạy trên cơ sở hạ tầng đám mây vật lý, bao gồm phần mềm hệ thống như hệ điều hành, màn hình máy ảo và môi trường thực thi đáng tin cậy.

Khi thảo luận về bảo mật cho Web 3, mọi người thường tập trung vào các hợp đồng thông minh nằm ở đầu phần mềm của nó. Các thành phần phần mềm ở cấp độ thấp hơn được chia sẻ bởi một số ứng dụng Web 3 khác nhau, do đó chúng được kiểm tra nhiều hơn và ít có khả năng xảy ra lỗi hơn.

Nhưng đồng thời, điều này cũng khiến chúng càng trở nên quan trọng hơn: một lỗi trong mã của một nút blockchain có thể gây nguy hiểm cho tất cả các ứng dụng trên blockchain đó, và một lỗi trong cơ sở hạ tầng hệ thống có thể gây nguy hiểm cho toàn bộ thế giới Web 3.

Công việc của CertiK về các bằng chứng được xác minh bằng máy bao gồm mọi lớp của ngăn xếp phần mềm Web 3. Ví dụ:

• Chúng tôi sử dụng kiểm tra mô hình tượng trưng để tự động xác minh các hợp đồng ERC-20 và các hợp đồng Solidity khác triển khai giao diện tiêu chuẩn

• Chúng tôi đã xác minh hợp đồng thông minh cho các ứng dụng DeFi như UniSwap, xác minh chính thức là một phần trong quá trình kiểm tra hợp đồng của chúng tôi cho Move và Cardano, đồng thời chúng tôi đã xác minh các thuộc tính tùy chỉnh cho một số dự án Solidity

• Trình biên dịch xác thực DeepSEA của chúng tôi được thiết kế để loại bỏ lỗi trong quá trình biên dịch

• Chúng tôi đã chính thức xác minh mô-đun ngân hàng tiêu chuẩn của Cosmos SDK

• Chúng tôi chính thức xác minh hợp đồng cam kết chuỗi chính của TON Chain

danh hiệu cấp một

Môi trường thực thi tin cậy HyperEnclave

Môi trường thực thi đáng tin cậy (TEE) được thiết kế để bảo vệ các ứng dụng khỏi một trong những loại tấn công thách thức nhất: những loại thậm chí có thể chiếm quyền kiểm soát hệ điều hành của máy tính.

Một số TEE đáng chú ý nhất bao gồm SGX, Arm TrustZone của Intel và AMD SEV. Chúng hoạt động bằng cách cho phép CPU chứng minh bằng mật mã rằng một ứng dụng (vỏ) bảo mật cụ thể đã được tải và ngăn phần mềm khác can thiệp vào ứng dụng đó.

TEE đã được tích hợp vào nhiều khía cạnh của cuộc sống số. Phần mềm mã hóa ổ đĩa như FileVault của Apple và các ứng dụng xác minh hai bước như Google Authenticator lưu trữ khóa trong TEE, để ngay cả khi ai đó đánh cắp và tháo rời máy tính xách tay hoặc điện thoại, khóa vẫn có thể được bảo vệ.

Đồng thời, trong Web 3, TEE cũng ngày càng trở nên quan trọng. Ví tiền điện tử cũng sử dụng TEE để lưu trữ khóa mã hóa an toàn hơn. Các oracle blockchain phân tán có thể sử dụng TEE để tăng tính xác thực và độ tin cậy của dữ liệu. Có những đề xuất sử dụng TEE cho 2 trong 3 hệ thống để giúp khắc phục các lỗi triển khai bằng chứng không có kiến ​​thức.

Ngoài ra còn có một số dự án blockchain, chẳng hạn như LucidiTEE, SubstraTEE, Oasis Network và AntChain, đề xuất sử dụng TEE để bảo vệ quyền riêng tư dữ liệu cho người dùng.

Hiện tại, hầu hết TEE đều là nguồn đóng và gắn liền với một nhà cung cấp phần cứng cụ thể. Ví dụ: để sử dụng Intel SGX, các ứng dụng phải chạy trên CPU Intel và được Intel phê duyệt cũng như đưa vào danh sách trắng. Tuy nhiên, quá trình phát triển phần cứng vốn đã chậm nên TEE có bộ tính năng nhỏ hơn và các vấn đề bảo mật yêu cầu phải cập nhật chương trình cơ sở CPU. Ngược lại, HyperEnclave được triển khai chủ yếu bằng phần mềm, tận dụng hai khả năng phần cứng sẵn có rộng rãi.

Đầu tiên, Mô-đun nền tảng đáng tin cậy của máy tính (TPM, thường được sử dụng để triển khai Khởi động an toàn UEFI) được sử dụng để xác minh rằng HyperEnclave và một nhóm các vùng bảo mật (vùng) cụ thể đang chạy. Thứ hai, HyperEnclave sử dụng các phần mở rộng ảo hóa của CPU để bảo vệ khu vực (thường được sử dụng bởi các màn hình máy ảo như VMware, VirtualBox, Hyper-V, KVM, v.v.). Đối với phần cứng máy tính, HyperEnclave trông giống như bất kỳ phần mềm ảo hóa nào khác, nhưng đối với các phần bao bọc, nó cung cấp API tương thích với SGX giúp các ứng dụng được viết cho SGX dễ dàng điều chỉnh để chạy trên HyperEnclave. Bằng cách sử dụng các công nghệ ảo hóa tiêu chuẩn, nó có thể dễ dàng hỗ trợ các ứng dụng hiệu suất cao tương tác chặt chẽ với hệ điều hành.

Phần quan trọng nhất của HyperEnclave là một màn hình có tên RustMonitor, giúp bảo vệ vùng này khỏi những nguy hiểm từ các vùng khác và từ hệ điều hành. enclave và hệ điều hành trong ảo hóa"guest"chế độ, có nghĩa là mỗi lần họ cố gắng truy cập bộ nhớ, địa chỉ bộ nhớ được truy cập trước tiên sẽ được dịch thông qua các bảng trang do RustMonitor quản lý. Bằng cách đặt các vùng trong các vùng khác nhau của bộ nhớ vật lý, RustMonitor có thể đảm bảo rằng chúng không bao giờ có thể đọc hoặc ghi đè dữ liệu thuộc sở hữu của các vùng khác. Nhưng đây không thể chỉ là một sự phân tách tĩnh đơn giản: một số địa chỉ bộ nhớ phải được phép chồng lên nhau để vùng này có thể giao tiếp với hệ điều hành và bản đồ địa chỉ được cập nhật khi xử lý ngắt trang.

Các nhà phát triển của HyperEnclave đã viết một tập hợp các thuộc tính bất biến mà bảng trang phải tuân theo, xác định cách hoạt động của các bảng ánh xạ địa chỉ bộ nhớ. Ví dụ: điều này bao gồm các thuộc tính như một địa chỉ ảo sẽ được ánh xạ tới một trang vật lý trong EPC khi và chỉ khi nó nằm trong ELRANGE. Vui lòng tham khảo báo cáo xác minh chính thức để biết các thuộc tính chi tiết. Bất kỳ lỗi nào vi phạm các điều kiện này có thể làm mất hiệu lực các đảm bảo bảo mật của toàn bộ hệ thống HyperEnclave.

danh hiệu cấp một

Xác minh chính thức RustMonitor của HyperEnclave

Mã quản lý bảng trang của RustMonitor là mục tiêu tốt để xác minh vì nó vừa nhỏ vừa quan trọng về mặt an toàn. Tương tự như trường hợp hợp đồng thông minh Web 3, việc nỗ lực xác minh chính thức chúng là khả thi. Trong dự án này, CertiK bắt đầu với các thuộc tính bất biến mà bảng trang phải tuân theo và dịch chúng từ tiếng Anh sang ngôn ngữ đặc tả hình thức Coq. Sau đó, chúng tôi đưa ra bằng chứng được máy kiểm tra rằng khi mã RustMonitor sửa đổi bảng, bảng kết quả vẫn đáp ứng tất cả các thuộc tính bất biến.

Trên thực tế, công việc phát triển của chúng tôi còn tiến xa hơn vì chúng tôi cũng muốn đảm bảo rằng thiết kế của những bất biến này là chính xác và bản dịch ngôn ngữ Coq của chúng tôi về chúng là chính xác. Để đạt được mục đích này, chúng tôi chỉ định thêm trong Coq thông tin mà mã máy khách có thể quan sát và sử dụng thuộc tính bất biến để chứng minh rằng sẽ không có luồng thông tin nào khác ("định lý không liên quan"). Tất cả những bằng chứng này được thực hiện cùng nhau cung cấp một sự đảm bảo mạnh mẽ rằng việc quản lý bảng trang là chính xác cả về thiết kế lẫn cách thực hiện.

Tuy nhiên, việc chứng minh tính đúng đắn của chương trình giám sát TEE không phải là một nhiệm vụ đơn giản. Các chương trình cấp hệ thống như màn hình ảo hóa và nhân hệ điều hành sử dụng nhiều mã cấp thấp liên quan đến cấu trúc dữ liệu bằng con trỏ, bỏ qua các kiểu trừu tượng và được tối ưu hóa cao cho hiệu suất. Cho đến ngày nay, việc xác minh các chương trình như vậy vẫn là một vấn đề nghiên cứu nóng hổi đáng được công bố trên các tạp chí khoa học máy tính hàng đầu và việc chứng minh từng dòng mã đòi hỏi nỗ lực rất lớn.

Ví dụ, bằng chứng ban đầu của seL 4 mất 20 năm người, trong khi Komodo mất 2 năm người để xác minh mã lắp ráp tương ứng với khoảng 650 dòng mã C. Mã trong các dự án này được viết lại cụ thể để đơn giản hóa việc xác minh, không giống như HyperEnclave, vốn đã được sản xuất và viết bằng ngôn ngữ Rust. Dựa trên công nghệ hiện đại, việc xác minh tất cả mã là không thực tế về mặt kinh tế. Một vấn đề khác là chuỗi công cụ xác minh của Rust chưa hoàn thiện so với các ngôn ngữ lập trình khác. Gánh nặng xác thực có thể được giảm bớt bằng cách viết mã mô hình thủ công thay vì mã thực tế. Một ví dụ là Sanctum TEE, một dự án nghiên cứu xác nhận. Nhược điểm của phương pháp này là sự không khớp giữa mã và mô hình trừu tượng có thể làm suy yếu hoặc thậm chí làm mất hiệu lực bất kỳ thuộc tính an toàn hoặc chính xác nào về mô hình.

CertiK được định vị độc đáo để giải quyết vấn đề này. Hai nhà sáng lập của chúng tôi, Giáo sư Shao Zhong và Giáo sư Gu Ronghui, là những người phát minh ra phương pháp xác minh Lớp trừu tượng chứng nhận đồng thời (CCAL). Họ đã sử dụng phương pháp này để xác minh hạt nhân hệ điều hành chứng nhận đồng thời đầu tiên trên thế giới CertiKOS và đã xác minh màn hình ảo hóa KVM seKVM và Kiến trúc điện toán bí mật của ARM. Ý tưởng cơ bản của CCAL là chia tất cả các hàm trong một chương trình thành nhiều lớp, viết mô hình trừu tượng của nó cho mỗi lớp, sau đó chứng minh rằng mã thực tế của hàm thực hiện mô hình trừu tượng, điều này làm giảm đáng kể nguy cơ mã không khớp với hành vi của mô hình trừu tượng. Cách tiếp cận theo lớp xử lý các vấn đề về bằng chứng mã và tính đồng thời dễ dàng hơn so với việc cố gắng xác minh toàn bộ chương trình dưới dạng một khối duy nhất. Công việc trước đây về seKVM và Arm CCA đã thu hút sự chú ý đến việc xác minh các dự án phần mềm hệ thống quy mô công nghiệp mà trước đây quá lớn để xác minh chính thức.

Nhóm xác minh chính thức của HyperEnclave bao gồm những người trước đây đã tham gia xác minh CertiKOS và seKVM và chúng tôi cố gắng sử dụng trải nghiệm này để đạt được sự cân bằng tốt giữa các tài nguyên xác minh và đảm bảo an ninh. Để thực hiện điều này, chúng tôi đã sử dụng phương pháp xác minh linh hoạt dựa trên đặc tả CCAL: khung của chúng tôi hỗ trợ xác minh rằng mã chức năng phù hợp với mô hình, nhưng chúng tôi đã chọn chỉ thực hiện xác minh này trên một tập hợp con các hàm (49 hàm xử lý trực tiếp trang bộ nhớ những cái bàn). Đối với các chức năng khác, chúng tôi giả định rằng bản dịch Coq thủ công của mã Rust là chính xác và chỉ chứng minh tính đúng đắn về mặt chức năng của các mô hình Coq này. Mức độ trừu tượng của cấu trúc dữ liệu được truy cập trong mã nguồn ở đây xác định xem mỗi hàm có cần xác minh rằng mã của nó có tuân thủ mô hình hay không. Khi HyperEnclave sử dụng cấu trúc dữ liệu Rust cấp cao, chúng tôi dịch chúng trực tiếp sang Coq, nhưng khi nó sử dụng định dạng bảng trang dựa trên byte cấp độ thấp, chúng tôi dành nhiều nỗ lực hơn để chứng minh sự tương đương của nó với mô hình chức năng cấp cao (xem toàn bộ Báo cáo xác minh chính thức). Trong trường hợp của RustMonitor, điều này có nghĩa là chúng tôi mã hóa bằng chứng cho mô-đun Bộ nhớ xử lý việc biểu diễn bảng trang, sử dụng mô hình trừu tượng cho mô-đun Enclave quản lý trạng thái bao quanh, sau đó kết hợp tất cả các mô hình kết quả để chứng minh các định lý bất biến và Định lý bảo mật cấp cao nhất.

Một phần thú vị khác của việc xác minh này là cách thực hiện việc chứng minh mã. Mã HyperEnclave xử lý các bảng trang là mã cấp thấp và không có công cụ xác minh hiện có nào xử lý tốt mã này. Để đạt được mục đích này, chúng tôi đã phát triển một khung để xác minh mã Rust bằng cách chuyển đổi nó sang ngôn ngữ trung gian MIR (Trình bày trung gian cấp trung) và sử dụng khung đó để xác minh các chức năng chính đó. Vì MIR là một ngôn ngữ nhỏ nên chúng tôi có thể viết ngữ nghĩa hoạt động chính xác cho nó và thực hiện xác minh chính xác mã MIR do trình biên dịch tạo ra, điều này cho phép các bằng chứng mã của chúng tôi có nền tảng vững chắc hơn là dựa vào một trình dịch tùy ý cho các tệp .

Tóm tắt

Tóm tắt

Môi trường thực thi đáng tin cậy (TEE) là công nghệ nền tảng cho điện toán đám mây và các ứng dụng Web 3, vì vậy việc xây dựng tính bảo mật của chúng là rất quan trọng. Trong dự án này, CertiK đã áp dụng các kỹ thuật xác minh chính thức nâng cao để xác minh các thành phần quan trọng nhất của nó, mang lại sự đảm bảo chắc chắn rằng mã của nó hoạt động như mong đợi và thực sự đáp ứng các đặc tính bảo mật mong muốn.

Công việc xác minh chính thức này chỉ là một phần của việc bảo mật máy tính cá nhân; nó chỉ bao gồm phần quản lý bảng trang của RustMonitor, đây chỉ là một thành phần trong hệ thống tổng thể. Trong tương lai, chúng tôi cũng sẽ tiến hành đánh giá mã, thử nghiệm và xác minh chính thức các thành phần điện toán bảo mật khác. Bằng cách xác minh phần cốt lõi, chúng tôi đã đặt nền tảng vững chắc cho điện toán đám mây về quyền riêng tư.