An ninh của Bitcoin và các blockchain khác, chẳng hạn như Liquid, phụ thuộc vào các thuật toán chữ ký số như ECDSA và chữ ký Schnorr. Một thư viện C gọi là libsecp256k1 cung cấp các thuật toán này và được sử dụng bởi cả Bitcoin Core và Liquid. Các thuật toán này sử dụng một phép toán gọi là nghịch đảo mô-đun, đây là một phần tốn kém trong quá trình.
Trong “Tính toán gcd thời gian không đổi nhanh và nghịch đảo mô-đun,” Daniel J. Bernstein và Bo-Yin Yang đã tạo ra một thuật toán nghịch đảo mô-đun mới gọi là “safegcd.” Thuật toán này đã được Peter Dettman triển khai cho libsecp256k1 vào năm 2021. Blockstream Research đã xác minh chính thức thiết kế của thuật toán bằng cách sử dụng trợ lý chứng minh Coq, cho thấy rằng nó tính toán đúng nghịch đảo mô-đun cho các đầu vào 256 bit.
Tuy nhiên, việc triển khai thuật toán safegcd yêu cầu điều chỉnh mô tả toán học để phù hợp với ngôn ngữ lập trình C, chỉ hỗ trợ nguyên số lên đến 64 bit. Nhiều tối ưu hóa đã được thêm vào để làm cho việc triển khai nhanh, dẫn đến bốn triển khai riêng biệt của thuật toán safegcd trong libsecp256k1.
Để đảm bảo rằng mã C triển khai đúng thuật toán safegcd, Verifiable C, một phần của Bộ công cụ phần mềm đã được xác minh, đã được sử dụng với trình chứng minh định lý Coq. Điều này liên quan đến việc xác định các điều kiện trước và điều kiện sau cho mọi hàm đang được xác minh bằng cách sử dụng logic phân tách. Quá trình xác minh sau đó bắt đầu từ điều kiện trước của hàm và thiết lập một bất biến mới sau mỗi câu lệnh trong thân hàm, cho đến khi điều kiện sau được đạt được ở cuối thân hàm hoặc các câu lệnh trả về.
Hầu hết nỗ lực chính thức được dành cho việc dịch các thao tác thô của mỗi biểu thức C thành các câu lệnh cấp cao hơn về những gì các cấu trúc dữ liệu đang được thao tác đại diện về mặt toán học. Quá trình xác minh đã dẫn đến một chứng minh chính thức, được xác minh bởi trợ lý chứng minh Coq, rằng việc triển khai hàm nghịch đảo mô-đun safegcd của libsecp256k1 với thời gian biến 64 bit là đúng về mặt chức năng.
Tuy nhiên, có một số hạn chế đối với chứng minh tính đúng đắn chức năng. Logic phân tách được sử dụng trong Verifiable C chỉ chứng minh tính đúng đắn một phần, có nghĩa là nó chỉ cho thấy rằng mã C trả về kết quả đúng nếu nó trả về, nhưng không chứng minh sự kết thúc của nó. Để giải quyết vấn đề này, một chứng minh Coq trước đó về các giới hạn của thuật toán safegcd đã được sử dụng để chứng minh rằng giá trị bộ đếm vòng lặp của vòng lặp chính không bao giờ vượt quá 11 lần lặp.
Một hạn chế khác là ngôn ngữ C không có đặc tả chính thức. Thay vào đó, dự án Verifiable C sử dụng dự án biên dịch CompCert để cung cấp đặc tả chính thức cho ngôn ngữ C. Điều này đảm bảo rằng khi một chương trình C đã được xác minh được biên dịch bằng trình biên dịch CompCert, mã lắp ráp kết quả sẽ đáp ứng đặc tả của nó, nhưng không đảm bảo rằng mã được tạo ra bởi các trình biên dịch khác sẽ hoạt động.
Ngoài ra, Verifiable C không hỗ trợ truyền, trả về hoặc gán cấu trúc. Trong libsecp256k1, các cấu trúc luôn được truyền qua con trỏ, điều này được phép trong Verifiable C, nhưng có một vài trường hợp sử dụng gán cấu trúc. Tóm lại, Blockstream Research đã xác minh chính thức tính đúng đắn của hàm nghịch đảo mô-đun của libsecp256k1, cung cấp thêm bằng chứng rằng việc xác minh mã C là khả thi trong thực tế.
Công việc này cũng nhấn mạnh rằng phần còn lại của các hàm được triển khai trong libsecp256k1 cũng có thể được xác minh, cho phép thư viện đạt được các đảm bảo về tính chính xác phần mềm cao nhất có thể.
Nguồn
<p>Bài viết How Digital Signatures Make Bitcoin Secure! lần đầu tiên xuất hiện trên CoinBuzzFeed.</p>
