Các nhà nghiên cứu của Zcash đã công bố một bộ hơn 2.700 định lý được kiểm tra bằng máy nhằm ngăn chặn các lỗi làm giả không thể phát hiện trong bản nâng cấp giao thức Ironwood sắp tới. Công trình này, được thực hiện bởi nhóm phát triển đằng sau loại tiền điện tử tập trung vào quyền riêng tư, sử dụng phương pháp xác minh hình thức để đảm bảo rằng các lỗ hổng làm giả không thể tồn tại trong mã nguồn.
Các định lý nhắm vào điều gì
Các định lý tập trung vào Ironwood, một bản nâng cấp được lên kế hoạch cho giao thức Zcash. Làm giả là một lỗ hổng nghiêm trọng cho phép kẻ tấn công tạo ra tiền từ hư vô — một thảm họa đối với bất kỳ loại tiền điện tử nào. Bằng cách sử dụng xác minh hình thức, các nhà nghiên cứu có thể chứng minh bằng toán học rằng các thuộc tính nhất định đúng với mọi lần thực thi mã, thay vì chỉ dựa vào kiểm toán thủ công hoặc thử nghiệm.
2.700 định lý bao phủ logic cốt lõi của các giao dịch ẩn danh (shielded transactions) của Ironwood, nơi số dư và số tiền giao dịch được mã hóa. Các chứng minh kiểm tra rằng hệ thống thực thi các bất biến về nguồn cung — nghĩa là không thể tạo ra nhiều Zcash hơn mức giao thức cho phép — ngay cả trong điều kiện có kẻ thù. Các nhà nghiên cứu cho biết phương pháp này phát hiện các trường hợp ngoại lệ mà việc xem xét mã truyền thống có thể bỏ sót.
Tại sao các chứng minh được kiểm tra bằng máy lại quan trọng
Xác minh hình thức hiếm khi được sử dụng trong phát triển tiền điện tử vì nó tốn thời gian và đòi hỏi chuyên môn cao. Hầu hết các dự án dựa vào tiền thưởng lỗi và kiểm toán thủ công, có thể để lại khoảng trống. Zcash đã sử dụng các phương pháp hình thức trước đây — cho bản nâng cấp Sapling ban đầu — nhưng nỗ lực Ironwood là ứng dụng lớn nhất cho đến nay đối với mạng lưới này.
Các định lý được viết bằng một ngôn ngữ gọi là Lean, một trợ lý chứng minh kiểm tra từng bước suy luận. Nếu một định lý vượt qua, điều đó có nghĩa là thuộc tính được đảm bảo cho mọi đầu vào. Các nhà nghiên cứu đã công bố toàn bộ bộ chứng minh cùng với đặc tả Ironwood, cho phép cộng đồng xác minh độc lập.
“Đây là về việc đưa ra sự đảm bảo mạnh nhất có thể rằng toán học đằng sau Ironwood là đúng đắn,” nhóm nghiên cứu cho biết trong một tuyên bố. “Chúng tôi muốn người dùng biết rằng nguồn cung được chứng minh là cố định, không chỉ được giả định.”
Ironwood vẫn đang trong quá trình phát triển. Công trình xác minh hình thức là một cột mốc quan trọng, nhưng bản nâng cấp vẫn phải trải qua quy trình quản trị của Zcash và được các thợ đào cũng như người vận hành nút chấp nhận. Các nhà nghiên cứu dự định sẽ tiếp tục mở rộng bộ định lý khi các tính năng mới được thêm vào.
Việc công bố các định lý không thay đổi gì đối với người dùng Zcash hiện tại. Mạng lưới tiếp tục chạy trên giao thức hiện có. Nhưng công trình này tạo ra một tiền lệ cho cách các bản nâng cấp trong tương lai có thể được xác thực — với sự chắc chắn toán học thay vì chỉ là sự tin tưởng.
Bước tiếp theo là giai đoạn xem xét của cộng đồng, sau đó mã Ironwood sẽ được đề xuất để kích hoạt. Chưa có ngày cụ thể nào được ấn định.
