Hook
Cuối tuần trước, Zcash im lặng phát hành một tuyên bố kỹ thuật. Không có airdrop, không có quan hệ đối tác, không có video hoạt hình. Chỉ có một con số khô khan: 2.700+ định lý kiểm tra bằng máy, tất cả đều nhằm chứng minh rằng bản nâng cấp Ironwood sắp tới không có lỗi làm giả không thể phát hiện được.
Đối với những người đã theo dõi các vụ hack DeFi trị giá hàng trăm triệu đô la, con số đó chẳng có nghĩa lý gì. Nhưng đối với bất kỳ ai hiểu được điểm mù lớn nhất của mật mã học — con người — thì con số này là một tín hiệu. Nó không chỉ là một báo cáo kiểm tra; nó là một sự tái cấu trúc triệt để của giả định tin cậy.
Context
Zcash là một blockchain tập trung vào quyền riêng tư, sử dụng zk-SNARKs (Đối số Kiến thức Không tiết lộ Ngắn gọn và Không tương tác) để ẩn người gửi, người nhận và số tiền giao dịch. Sức mạnh của nó cũng là điểm yếu của nó. Nếu có một lỗ hổng trong mạch zk-SNARK, kẻ tấn công có thể tạo ra ZEC từ hư vô — một vụ làm giả không thể phát hiện được — và không ai trên mạng lưới có thể nhìn thấy.
Năm 2018, Zcash đã có một lỗ hổng như vậy. Lỗ hổng BCTV14 cho phép tạo ra các đồng tiền giả, mặc dù nó đã được vá trước khi bị khai thác, nhưng nỗi ám ảnh về “lỗ hổng làm giả” vẫn còn đó. Đó là nỗi sợ hãi hiện sinh của mọi giao thức bảo mật.
Ironwood là bản nâng cấp giao thức quan trọng tiếp theo của Zcash. Và thay vì chỉ dựa vào kiểm toán truyền thống, nhóm nghiên cứu của Zcash — bao gồm một số nhà mật mã học hàng đầu thế giới — đã thực hiện một bước đi triệt để hơn nhiều: hình thức hóa việc xác minh.
Core: 2.700+ định lý và ý nghĩa của chúng
Sự phá vỡ tương quan giữa kiểm toán và bảo mật chính là tín hiệu. Hầu hết mọi người trong crypto đều nghĩ rằng “kiểm toán” là đủ. Nhưng kiểm toán là con người xem xét mã. Con người thì mắc lỗi. Đặc biệt là trong mật mã học, nơi mà một lỗi logic duy nhất trong một mạch có thể khiến toàn bộ giao thức sụp đổ.
Zcash đã chọn con đường hình thức hóa. Họ viết các định lý bằng một ngôn ngữ hình thức (rất có thể là Coq hoặc Isabelle, dựa trên nền tảng của nhóm nghiên cứu), và sau đó để máy tính kiểm tra từng bước suy luận. Nếu máy tính chấp nhận định lý, thì về mặt toán học, không có lỗ hổng “làm giả không thể phát hiện” nào tồn tại trong phạm vi các định lý đó.
Con số 2.700+ nghe có vẻ ấn tượng, nhưng con số quan trọng hơn là phạm vi bao phủ. Các định lý này có bao phủ toàn bộ mạch zk-SNARK cho Ironwood không? Hay chỉ phần cốt lõi của giao thức? Dựa trên kinh nghiệm kiểm toán của tôi, tôi nghi ngờ rằng nó bao phủ phần quan trọng nhất: các ràng buộc về tính hợp lệ của giao dịch. Nếu bạn có thể chứng minh rằng không có cách nào để tạo ra một giao dịch hợp lệ ngoài việc chi tiêu các đồng tiền thực sự tồn tại, thì bạn đã loại bỏ được nỗi sợ lớn nhất.
Hãy xem xét một đoạn mã giả đơn giản hóa của một ràng buộc zk-SNARK:
def verify_transaction(tx, state):
# Giả sử 'cm' là cam kết đầu ra
# 'sn' là số serial của đầu vào
# 'rt' là gốc của Merkle tree
proof = tx.proof# Các ràng buộc cốt lõi: assert verify_merkle_membership(proof, rt, cm) # Đầu ra tồn tại trong cây assert not is_nullifier_used(sn) # Đầu vào chưa được sử dụng assert sum(inputs) == sum(outputs) + fee # Bảo toàn giá trị ```
Một lỗi làm giả sẽ xảy ra nếu một trong các ràng buộc này bị bỏ qua hoặc có thể bị qua mặt. Bằng chứng hình thức hóa của Zcash đảm bảo rằng không có con đường nào tồn tại để vi phạm ba ràng buộc này đồng thời mà không tạo ra một giao dịch bị từ chối.
Điều mà đường cong đảo ngược của rủi ro bảo mật có nghĩa là: Trong kiểm toán truyền thống, rủi ro giảm dần theo thời gian khi có nhiều người xem xét mã. Với hình thức hóa, rủi ro giảm đột ngột xuống gần bằng 0 ngay khi định lý được chứng minh.
Contrarian: Vở kịch phi tập trung dừng lại khi...
... người dùng vẫn phải tin tưởng vào mã máy kiểm tra và công cụ hình thức hóa. Đây là điểm mù tinh vi nhất.
Các định lý kiểm tra bằng máy chỉ đúng nếu bản thân máy kiểm tra (kernel của Coq hay Isabelle) không có lỗi. Và nếu mô hình hóa bài toán là sai. Bạn có thể viết một định lý hoàn hảo cho một mạch không chính xác. Nói cách khác, đây là sự dịch chuyển của lòng tin: từ nhà phát triển sang nhà thiết kế giao thức và nhà phát triển công cụ.
Hơn nữa, hình thức hóa chỉ loại bỏ “lỗi làm giả không thể phát hiện”. Nó không giải quyết được các cuộc tấn công từ chối dịch vụ, lỗi của người xác thực, hay các cuộc tấn công vào lớp mạng. Nhưng đối với một giao thức bảo mật, đây là ưu tiên cao nhất. Loại bỏ được nó là một chiến thắng lớn.
Cuối cùng, có một sự thật khó chịu: Không ai trong số 99% người dùng crypto sẽ đọc các định lý này. Giá trị của chúng là gián tiếp, thông qua sự tự tin mà chúng mang lại cho các nhà phát triển và các tổ chức có thể quan tâm đến việc sử dụng Zcash. Nó không giải quyết được vấn đề thanh khoản của ZEC hay sự thống trị của Monero về mặt áp dụng.
Takeaway
2.700 định lý không làm cho Zcash trở thành blockchain “tốt nhất”. Nhưng nó làm cho Zcash trở thành blockchain có nền tảng toán học vững chắc nhất trong lĩnh vực bảo mật. Đây là một tài sản vô hình, nhưng trong một thế giới nơi các lỗ hổng trị giá hàng trăm triệu đô la bị khai thác hàng tháng, có lẽ tài sản vô hình này xứng đáng được định giá cao hơn nhiều so với mức thị trường hiện tại.
Nhưng câu hỏi vẫn còn đó: Liệu một “bằng chứng” toán học có đủ sức mạnh để thay đổi câu chuyện về quyền riêng tư trong crypto, hay nó chỉ là một dòng ghi chú trong lịch sử kỹ thuật?