Zcash đã hoàn tất quá trình xác thực theo cơ chế Ironwood và công bố việc loại trừ bằng chứng Lean để loại bỏ rủi ro giả mạo ZEC.

Zcash chương trình Tachyon đã được công bố vào ngày 29 tháng 7, hoàn tất việc xác minh hình thức đối với pool che chắn Ironwood, và phát hành một chứng minh được xác minh bằng máy, bao gồm hơn 2.700 định lý được viết bằng ngôn ngữ lập trình Lean. Việc xác minh lần này đã thiết lập một thuộc tính bảo mật có tên là “Tính toàn vẹn số dư”, loại trừ một cách hiệu quả khả năng tồn tại các lỗ hổng giả mạo không thể phát hiện trong Ironwood theo các giả định mật mã đã được xác định của nó.

Hoàn tất xác minh hình thức cho chương trình Tachyon: hơn 2700 định lý Lean

Công việc xác minh hình thức của chương trình Tachyon được hoàn thành thông qua sự phối hợp của ba nhà nghiên cứu và một nhóm các chuyên gia mật mã, kéo dài hơn một tháng; chứng minh được xác minh bằng máy được công bố cuối cùng bao gồm hơn 2.700 định lý, toàn bộ đều được viết bằng ngôn ngữ lập trình Lean. Ý nghĩa của lần xác minh này nằm ở chỗ nó là “xác minh bằng máy” — tức là máy tính tự động kiểm tra tính đúng đắn của từng bước logic, thay vì chỉ dựa vào việc duyệt thủ công, từ đó mang lại mức độ chắc chắn cao hơn.

Chương trình Tachyon cho biết, việc xác minh đã hoàn tất thiết lập một bảo đảm toán học rằng pool che chắn Ironwood không chứa các lỗ hổng giả mạo không thể phát hiện trong các giả định mật mã đã được xác định của nó.

Thuộc tính bảo mật “Tính toàn vẹn số dư”: bảo đảm toán học để pool quỹ được bảo vệ không bị chi trả quá mức

“Tính toàn vẹn số dư (Balance Integrity)” là thuộc tính bảo mật cốt lõi được hình thức xác minh lần này thiết lập. Định nghĩa toán học của thuộc tính này là: số tiền mà pool quỹ Ironwood được bảo vệ thanh toán sẽ không vượt quá số tiền được công khai nạp vào. Để đạt được thuộc tính này, các thành phần được bao gồm trong công việc xác minh như sau:

· Hệ thống chứng minh không kiến thức (ZK) của Ironwood

· Quy tắc mạch: các quy tắc tính toán nền tảng cấu thành logic của Ironwood

· Kế toán theo sổ cái: cơ chế theo dõi và ghi sổ quỹ theo toàn bộ lớp mạng

Điều đáng lưu ý là, chứng minh lần này không bao gồm các biện pháp bảo vệ quyền riêng tư độc lập của Ironwood; các nhà nghiên cứu cho biết, việc bảo đảm quyền riêng tư thuộc về một thuộc tính bảo mật độc lập và cần được xác minh thêm.

Bối cảnh lỗ hổng Orchard và cơ chế kế toán công khai “cổng xoay”

Nguyên nhân trực tiếp khiến pool che chắn Ironwood được triển khai là lỗ hổng được phát hiện trong pool bảo mật Orchard — lỗ hổng này về mặt lý thuyết có thể khiến cho hành vi giả mạo ZEC không thể bị phát hiện, từ đó đe dọa tính toàn vẹn của nguồn cung Zcash. Zcash giới thiệu Ironwood trong bản nâng cấp NU6.3; các nhà phát triển cho biết chưa phát hiện bất kỳ bằng chứng nào cho thấy lỗ hổng đã được khai thác thực tế, và pool che chắn mới nhằm khôi phục niềm tin của bên ngoài vào tính toàn vẹn của nguồn cung Zcash.

Các khoản tiền chuyển từ Orchard phải đi qua điểm kiểm tra kế toán công khai có tên “Cổng xoay (Revolving Door)”, với mục đích ngăn chặn bất kỳ token vượt mức giả tưởng nào đi vào Ironwood; khi dòng tiền tiếp tục chảy ra khỏi Orchard, quá trình này cũng có thể dần dần cung cấp thêm bằng chứng để đánh giá liệu pool tiền cũ có từng bị lạm dụng hay không.

Câu hỏi thường gặp

Chương trình Tachyon xác minh hình thức Ironwood bao gồm bao nhiêu định lý và được thực hiện bằng công cụ gì?

Theo thông báo của chương trình Tachyon, lần xác minh hình thức này bao gồm hơn 2.700 định lý, tất cả đều được viết bằng ngôn ngữ lập trình Lean; được hoàn thành trong hơn một tháng bởi ba nhà nghiên cứu và một nhóm chuyên gia mật mã; kết quả cuối cùng là một chứng minh toán học được xác minh bằng máy, trong đó máy tính tự động kiểm tra tính đúng đắn của từng bước logic.

Thuộc tính bảo mật “Tính toàn vẹn số dư” đảm bảo cụ thể điều gì?

“Tính toàn vẹn số dư” bảo đảm rằng số tiền mà pool quỹ Ironwood được bảo vệ thanh toán sẽ không vượt quá số tiền được công khai nạp vào; lần xác minh này bao gồm tất cả các thành phần cần thiết để thực hiện thuộc tính này, bao gồm hệ thống chứng minh không kiến thức của Ironwood, các quy tắc mạch và kế toán theo sổ cái; nhưng lần xác minh này không bao gồm các biện pháp bảo vệ quyền riêng tư độc lập của Ironwood.

Vì sao Zcash cần giới thiệu Ironwood, và liệu lỗ hổng Orchard đã được khai thác chưa?

Ironwood được giới thiệu trong bản nâng cấp NU6.3 của Zcash, nhằm đối phó với một lỗ hổng được phát hiện trong pool bảo mật Orchard — lỗ hổng này về mặt lý thuyết có thể khiến cho hành vi giả mạo ZEC không thể bị phát hiện; các nhà phát triển Zcash cho biết vẫn chưa phát hiện bất kỳ bằng chứng nào cho thấy lỗ hổng đó đã được khai thác thực tế, và pool che chắn mới nhằm khôi phục niềm tin của bên ngoài vào tính toàn vẹn của nguồn cung Zcash.