Ethereum: Công bố 5 lộ trình giảm phạm vi tin cậy của client

Năm lộ trình thiết kế và triển khai xác minh hình thức nhằm giảm nền tảng điện toán tin cậy (TCB) của client Ethereum(ETH) đã được công bố.

George Kadianakis và Kev Wedderburn, các thành viên Ethereum Foundation, đã đăng bài viết liên quan trên diễn đàn nghiên cứu Ethereum ngày 25, trình bày cách thu hẹp phạm vi thành phần cần tin cậy trong client Ethereum bằng xác minh hình thức.

TCB là tập hợp các thành phần, đặc tả, công cụ và giả định được sử dụng dựa trên tiền đề phải tin cậy, thay vì đã được xác minh. Bài viết cho rằng xác minh hình thức không thể loại bỏ hoàn toàn TCB nhưng có thể giảm phạm vi mà con người phải trực tiếp tin cậy.

Các tác giả đề xuất chia client đã được trừu tượng hóa thành nhiều mô-đun, sau đó xác minh riêng vai trò và phạm vi bảo đảm của từng mô-đun. Khi các bảo đảm của từng mô-đun được kết nối thông qua giao diện, có thể kiểm tra các thuộc tính bảo mật của toàn bộ client.

Phân loại cốt lõi là 'mô-đun thuần' và 'mô-đun không thuần'. Những lĩnh vực có ít tác dụng phụ và cấu trúc toán học rõ ràng như mật mã học, SSZ và quy tắc lựa chọn fork được xếp vào nhóm mô-đun thuần, phù hợp với xác minh hình thức. Trong khi đó, các lĩnh vực có nhiều hoạt động nhập xuất và trạng thái bên ngoài như mạng lưới, nơi phải xử lý thứ tự thông điệp, gián đoạn kết nối và độ trễ, được xem là mô-đun không thuần.

Các tác giả đề xuất thiết kế mô-đun không thuần theo hướng không mặc định tin cậy ngay từ đầu. Chẳng hạn, thay vì tin cậy trực tiếp chữ ký do mô-đun mạng lưới truyền đến, hệ thống có thể xử lý lại chữ ký đó trong một mô-đun xác minh chữ ký thuần. Theo cách này, lỗi của mô-đun mạng lưới có thể được xử lý giống như một đầu vào bên ngoài độc hại.

Về dài hạn, bài viết cũng đề xuất đưa ranh giới xác minh đến gần mạng lưới hơn. Thay vì mô hình hóa toàn bộ mạng lưới, phương án này ưu tiên xác minh bộ phân tích cú pháp, quy tắc gossip và logic đồng bộ hóa nhằm ngăn thông điệp sai khiến hệ thống dừng hoạt động hoặc tiêu tốn quá nhiều tài nguyên.

Mối liên kết giữa đặc tả và tệp thực thi cũng được nêu là một nhiệm vụ riêng. Các tác giả phân biệt việc viết đặc tả hình thức và chứng minh thuộc tính bằng Lean4 với việc chứng minh triển khai thực tế tuân thủ đặc tả đó. Người dùng quan tâm đến độ an toàn của mã chạy trên máy tính của mình hơn là các định lý trong Lean4, vì vậy cả hai bước đều cần thiết.

Năm lộ trình triển khai được đề xuất gồm: △ tự động chuyển đổi mã viết bằng Rust và các ngôn ngữ khác sang Lean4 △ trích xuất mô-đun viết bằng Lean4 thành mã C △ viết toàn bộ client bằng Lean4 và chỉ kết nối các mô-đun có nhiều tác dụng phụ bằng ngôn ngữ khác △ viết trực tiếp các mô-đun cốt lõi bằng hợp ngữ RISC-V △ sử dụng trình biên dịch đã được xác minh.

Nếu chuyển đổi mã Rust sang Lean4, bộ chuyển đổi và trình biên dịch Rust tạo ra tệp nhị phân cuối cùng vẫn nằm trong TCB. Khi trích xuất mã Lean4 sang C hoặc viết phần lớn client bằng Lean4, bộ trích xuất, trình biên dịch C và giao diện hàm bên ngoài sẽ trở thành các thành phần cần tin cậy.

Việc viết các mô-đun cốt lõi bằng hợp ngữ RISC-V có thể loại trình biên dịch thông thường khỏi TCB, nhưng mô hình hình thức của tập lệnh RISC-V và công cụ chuyển hợp ngữ thành mã cho bộ xử lý khác sẽ trở thành các thành phần cần tin cậy mới. Nếu sử dụng trình biên dịch đã được xác minh, bộ trích xuất và trình biên dịch C có thể được loại khỏi TCB.

Các tác giả cho rằng không cần áp dụng một phương thức duy nhất cho mọi mô-đun. Những mô-đun có cấu trúc toán học chặt chẽ có thể được xác minh bằng Lean4, trong khi các mô-đun có cấu trúc dữ liệu phức tạp hoặc quy mô lớn có thể sử dụng bộ chuyển đổi hay trình biên dịch đã được xác minh, tạo thành phương án kết hợp.

Bài viết không phải là thông báo cho thấy toàn bộ client Ethereum đã hoàn tất xác minh hình thức. Đây là nghiên cứu đưa ra định hướng thiết kế về cách chia nhỏ và mở rộng hoạt động xác minh từ đặc tả hình thức đến triển khai và quy trình biên dịch.