Bitcoin(BTC) thử nghiệm chống lượng tử: kết hợp code C với kiểm chứng máy

Nhóm phát triển Bitcoin(BTC) vừa công bố thư viện nghiên cứu chữ ký hậu lượng tử mang tên libshrincs. Đây không phải bản cập nhật áp trực tiếp vào phần lõi Bitcoin, mà là một bằng chứng khái niệm (proof-of-concept) kết hợp code viết bằng ngôn ngữ C với việc kiểm chứng bằng máy cho các chứng minh bảo mật.

Theo Delving Bitcoin đưa tin ngày 12 (giờ Hàn Quốc), nhà nghiên cứu Jonas Nick của Blockstream và nhà phát triển remix7531 đã công bố libshrincs. Thư viện này hiện thực hóa bằng C ngôn ngữ WOTS+C, thành phần chữ ký dùng một lần trong SHRINCS, cơ chế được đề xuất làm hệ thống chữ ký hậu lượng tử cho Bitcoin.

Nhóm phát triển đã hình thức hóa các chứng minh bảo mật bằng Rocq Prover và SSProve. Sau đó, họ dùng VST để kiểm tra xem phần code C có tuân theo đặc tả Rocq hay không. Đáng chú ý, phần lớn công đoạn chứng minh có sự hỗ trợ của mô hình ngôn ngữ lớn (LLM).

Trọng tâm của lần công bố này không nằm ở việc đề xuất một hệ mật mã mới. Đây là một ví dụ cho thấy hướng nghiên cứu ứng dụng AI vào chứng minh toán học đang được nối dài sang việc chứng minh mật mã và kiểm chứng triển khai thực tế trên Bitcoin.

Kho lưu trữ trên GitHub xác định rõ libshrincs là một proof-of-concept. Cả code C lẫn các hợp đồng VST đều ở trạng thái tạm thời và có thể thay đổi trong thời gian tới.

Công cụ triển khai và kiểm chứng được phân chia theo từng vai trò cụ thể. Phần triển khai dùng ngôn ngữ C, chứng minh bảo mật dùng Rocq 9.0 cùng SSProve và MathComp, còn kiểm chứng chức năng dùng Rocq 9.0 kết hợp VST và CompCert. Lệnh “make audit” được thiết kế để chỉ liệt kê dưới dạng bảng các giả định đã được cho phép.

SHRINCS, nền tảng của libshrincs, là hệ thống chữ ký hậu lượng tử dựa trên hàm băm, được thiết kế có tính đến giới hạn dung lượng lưu trữ trên blockchain. Mật mã hậu lượng tử là công nghệ mã hóa được xây dựng để chống lại các cuộc tấn công từ máy tính lượng tử.

Blockstream cho biết ở chế độ có trạng thái (stateful), SHRINCS tạo ra chữ ký có kích thước 324 byte. Với đường dẫn thay thế phi trạng thái (stateless) — dùng khi trạng thái chữ ký bị hỏng hoặc mất — kích thước chữ ký dao động 3-8KB. Blockstream cũng cho biết dữ liệu chữ ký theo phương thức này chiếm ít hơn 97% dung lượng khối so với các phương án thay thế theo chuẩn NIST.

Trước đó, Jonas Nick từng đề xuất phương án đưa chữ ký hậu lượng tử vào Bitcoin bằng cách bổ sung một nhánh chi tiêu riêng trong cây Taproot. Theo cấu trúc này, ở điều kiện bình thường Bitcoin vẫn dùng chữ ký Schnorr hiện có, còn nhánh chữ ký hậu lượng tử chỉ được kích hoạt khi cần thiết.

Taproot cho phép gộp nhiều điều kiện chi tiêu vào một cấu trúc cây và chỉ công khai điều kiện thực sự được sử dụng. Tuy nhiên, để bổ sung một tính năng xác minh chữ ký mới vào phần lõi Bitcoin, cần thay đổi quy tắc đồng thuận và trải qua quá trình thảo luận đề xuất cải tiến Bitcoin (BIP).

Giới hạn của nghiên cứu hiện tại cũng khá rõ ràng. Nhóm phát triển thừa nhận các chứng minh vừa hoàn thiện chưa đạt mức bảo đảm hậu lượng tử đầy đủ theo mô hình QROM, và sử dụng khái niệm bảo mật yếu hơn so với môi trường triển khai thực tế. Đây là lý do libshrincs chưa thể xem là code đã được đưa vào Bitcoin Core.

Chữ ký kiểu có trạng thái đòi hỏi phải lưu trữ an toàn lịch sử sử dụng của cùng một khóa. Nếu bản sao lưu bị dùng trùng lặp hoặc thiết bị bị đưa về trạng thái ban đầu, độ an toàn của chữ ký có thể suy yếu — vì vậy việc quản lý trạng thái trên ví cứng và firmware được xem là bài toán cốt lõi.

Trong phần thảo luận trên Delving Bitcoin, thiết kế kết hợp song song một nhánh phí thấp dùng cho giao dịch thông thường và một nhánh phi trạng thái dùng để khôi phục được đánh giá tích cực. Ngược lại, cộng đồng cũng nêu ra các rủi ro vận hành có thể phát sinh trong thực tế, như lỗi khi khôi phục trạng thái, dùng trùng bản sao lưu hay mất nguồn điện đột ngột.

Jonas Nick giải thích rằng đối với thiết bị đã từng nhập seed, chỉ nên sử dụng nhánh phi trạng thái. Ông cũng cho biết cần thêm phản hồi thực tế từ các nhà phát triển ví để đánh giá khả năng duy trì trạng thái an toàn của ví cứng.

Trên một blog riêng, remix7531 chỉ ra rằng LLM có thể giúp hoàn thành chứng minh nhanh hơn, nhưng cũng tiềm ẩn rủi ro khiến những đặc tả bị viết sai lại được thông qua nhanh hơn. Bình luận đáng chú ý là libshrincs không hướng đến việc làm chứng minh phức tạp hơn, mà được thiết kế theo hướng giảm bớt phần đặc tả và giả định mà con người cần rà soát thủ công.