Vitalik Buterin, đồng sáng lập Ethereum, đã công bố một bài luận chi tiết lập luận rằng việc xác minh chính thức có sự hỗ trợ của trí tuệ nhân tạo có thể thay đổi căn bản cách xây dựng phần mềm an toàn, bác bỏ sự bi quan ngày càng tăng trong cộng đồng an ninh mạng về việc liệu các hệ thống không cần tin cậy có thể chống chọi được các cuộc tấn công ngày càng mạnh mẽ do trí tuệ nhân tạo điều khiển hay không.
“Nhiều người cho rằng với việc tìm lỗi bằng trí tuệ nhân tạo, việc viết mã an toàn sẽ trở nên bất khả thi,” Buterin viết. “Tôi có quan điểm lạc quan hơn nhiều, và việc xác minh chính thức bằng trí tuệ nhân tạo là một phần quan trọng của lý do đó.”
Xác minh hình thức thực chất là gì?
Kiểm chứng hình thức là việc viết các chứng minh toán học về mã nguồn mà máy tính có thể tự động kiểm tra. Thay vì thử nghiệm phần mềm và hy vọng không có lỗi xảy ra, các nhà phát triển viết các chứng minh đảm bảo về mặt toán học rằng một đoạn mã hoạt động chính xác như dự định trong mọi điều kiện.
Công nghệ này đã tồn tại hàng thập kỷ nhưng vẫn chỉ được sử dụng rộng rãi vì việc tự viết các chứng minh bằng tay vô cùng khó khăn và tốn thời gian. Luận điểm của Buterin là trí tuệ nhân tạo (AI) sẽ thay đổi đáng kể điều này. AI có thể viết cả mã lập trình và chứng minh, trong khi con người chỉ đơn giản là xác minh xem các tuyên bố được chứng minh có khớp với những gì họ thực sự muốn phần mềm thực hiện hay không.
Ông mô tả sự kết hợp này là điều mà nhà nghiên cứu Yoichi Hirai gọi là “hình thức cuối cùng của phát triển phần mềm”.
Tại sao điều này lại quan trọng đối với Ethereum
Buterin đã chỉ ra một số lĩnh vực mà việc xác minh chính thức đang được áp dụng trong hệ sinh thái phát triển của Ethereum. Chúng bao gồm chữ ký chống lượng tử, hệ thống bằng chứng STARK, thuật toán đồng thuận và ZK-EVM, tất cả đều là những lĩnh vực mà các thuộc tính bảo mật rất dễ xác định mặc dù mã nguồn cơ bản cực kỳ phức tạp.
Các dự án như Arklib đang hướng tới việc triển khai STARK được kiểm chứng chính thức hoàn toàn. Dự án evm-asm đang xây dựng toàn bộ EVM được viết trực tiếp bằng ngôn ngữ assembly RISC-V, được kiểm chứng toán học dựa trên một triển khai tham chiếu dễ đọc đối với con người. Các giao thức đồng thuận chịu lỗi Byzantine cũng đang được đặc tả và kiểm chứng chính thức trong Lean.
Điểm mấu chốt là đối với các hệ thống này, khoảng cách giữa những gì mã lệnh thực hiện và những gì nó được cho là phải làm có thể được thu hẹp bằng độ chắc chắn toán học hơn là bằng thử nghiệm xác suất.
Những giới hạn mà ông ấy thừa nhận
Buterin đã cẩn thận không phóng đại vấn đề. Việc xác minh hình thức có những phương thức thất bại thực sự. Bằng chứng có thể chỉ được viết về một phần của hệ thống trong khi các lỗi nghiêm trọng lại ẩn giấu trong các phần chưa được xác minh. Các nhà phát triển có thể quên chỉ định các thuộc tính quan trọng. Bản thân đặc tả hình thức cũng có thể sai. Các lỗ hổng phần cứng như tấn công kênh phụ có thể vượt qua cả phần mềm đúng về mặt toán học.
“Tính đúng đắn có thể chứng minh được không có nghĩa là phần mềm đúng theo cách mà hầu hết mọi người hiểu về tính đúng đắn,” ông viết. Điều mà việc xác minh hình thức thực sự làm là cho phép các nhà phát triển thể hiện ý định của họ theo nhiều cách khác nhau và dư thừa, đồng thời tự động kiểm tra xem tất cả các cách thể hiện đó có tương thích với nhau hay không.
Tầm nhìn rộng lớn hơn
Buterin đã mô tả một tương lai lạc quan, nơi phần mềm được chia thành hai lớp. Lớp biên không an toàn xử lý các chức năng có mức độ rủi ro thấp hơn, chạy trong môi trường biệt lập (sandbox) và hoạt động với quyền hạn tối thiểu. Lõi an toàn xử lý mọi thứ quan trọng, bao gồm cả Ethereum, nhân hệ điều hành và cơ sở hạ tầng IoT nhạy cảm.
Lõi bảo mật được giữ ở kích thước nhỏ một cách có chủ ý và được kiểm chứng hình thức nghiêm ngặt. Trí tuệ nhân tạo (AI) mang lại sức mạnh tính toán để giúp việc kiểm chứng trở nên khả thi trên quy mô lớn. Kết quả không phải là phần mềm không có lỗi, mà là phần mềm mà các thành phần quan trọng nhất có thể được tin tưởng với độ chính xác toán học chứ không phải chỉ dựa vào hy vọng.
“Cuối cùng thì những người bảo vệ cũng có cơ hội giành chiến thắng một cách dứt khoát,” ông kết luận, dẫn chứng kinh nghiệm của chính Mozilla trong việc tăng cường bảo mật mã nguồn chống lại các công cụ tấn công hỗ trợ bởi trí tuệ nhân tạo.
