Tóm tắt nhanh
- Vitalik Buterin cho rằng xác minh hình thức có hỗ trợ AI có thể giúp giảm lỗ hổng trong Ethereum và các hạ tầng crypto khác.
- Kỹ thuật này sử dụng các bằng chứng toán học để xác minh rằng phần mềm hoạt động đúng như thiết kế.
- Buterin cho rằng AI có thể vừa làm tăng sức mạnh của các cuộc tấn công mạng, vừa cải thiện các công cụ phòng thủ bảo mật.
Đồng sáng lập Ethereum, Vitalik Buterin, cho biết phần mềm được xác minh bằng toán học đang trở nên cần thiết để bảo vệ Ethereum và ngành công nghiệp crypto nói chung khỏi các cuộc tấn công mạng có hỗ trợ AI cũng như các lỗ hổng phần mềm.
Trong một bài blog được đăng vào thứ Hai, Buterin lập luận rằng “xác minh hình thức” có hỗ trợ AI có thể giúp bảo mật mạng blockchain, smart contract và các hệ thống mật mã trước những lỗi phần mềm có thể khiến người dùng chịu tổn thất tài chính không thể đảo ngược.
“Nếu được thực hiện đúng cách, điều này có tiềm năng vừa tạo ra mã nguồn cực kỳ hiệu quả, vừa an toàn hơn rất nhiều so với cách lập trình truyền thống trước đây,” Buterin viết, đồng thời cho biết nhà phát triển Yoichi Hirai gọi đây là “hình thái cuối cùng của phát triển phần mềm.”
Xác minh hình thức là phương pháp kiểm tra bằng toán học nhằm xác định liệu phần mềm có hoạt động chính xác hay không, với nền tảng nghiên cứu bắt nguồn từ những năm 1950 và 1960. Theo Buterin, những tiến bộ gần đây trong AI đang khiến kỹ thuật này trở nên thực tiễn hơn đối với ngành kỹ thuật phần mềm và nghiên cứu bảo mật.
“Nếu bạn xác minh hình thức từ đầu đến cuối, bạn không chỉ chứng minh rằng mô tả lý thuyết của giao thức là an toàn, mà còn chứng minh rằng chính đoạn mã mà người dùng thực sự chạy cũng an toàn trong thực tế,” ông viết. “Từ góc nhìn của người dùng, điều này cải thiện đáng kể tính trustless: để hoàn toàn tin tưởng mã nguồn, bạn không cần phải kiểm tra toàn bộ code, mà chỉ cần xác minh các tuyên bố đã được chứng minh về nó.”
Bài viết của Buterin xuất hiện trong bối cảnh các nhà nghiên cứu và chính phủ cảnh báo rằng các mô hình AI tiên tiến đang nhanh chóng cải thiện khả năng phát hiện và khai thác lỗ hổng phần mềm. Anthropic đã hạn chế quyền truy cập vào mô hình Claude Mythos chuyên về an ninh mạng sau khi các bài kiểm tra cho thấy hệ thống này có thể tự động xác định và khai thác lỗ hổng phần mềm ở mức vượt xa các mô hình AI công khai trước đây.
Mô hình này đã thu hút sự chú ý từ các cơ quan tình báo và an ninh nhờ những khả năng đó. Vào tháng 4, Claude Mythos của Anthropic đã phát hiện 271 lỗ hổng trong Mozilla Firefox trong quá trình thử nghiệm nội bộ, trong khi đầu tháng này, các nhà nghiên cứu bảo mật cho biết phiên bản preview của mô hình đã hỗ trợ phát triển một exploit nhắm vào cơ chế bảo vệ của chip M5 từ Apple. Các nhà nghiên cứu tại Viện An ninh AI của Anh cũng phát hiện rằng GPT-5.5 của OpenAI đã thể hiện khả năng tấn công mạng ở mức độ cao.
“Lỗi trong mã máy tính thực sự đáng sợ,” Vitalik Buterin viết.
Những lỗi chưa được phát hiện có thể gây hậu quả nghiêm trọng đối với các dự án crypto, nơi các lỗ hổng phần mềm có thể bị khai thác để đánh cắp vĩnh viễn tài sản của người dùng với rất ít cơ hội khôi phục.
Vào tháng 4, các hacker thuộc Lazarus Group do Triều Tiên hậu thuẫn đã đánh cắp 292 triệu USD token từ hạ tầng của Kelp DAO sau khi “đầu độc” các RPC nội bộ được sử dụng bởi LayerZero Labs. Tổng cộng, các hacker được cho là có liên hệ với nhà nước Triều Tiên đã đánh cắp hơn 6 tỷ USD crypto cho đến nay.
Buterin cho biết xác minh hình thức cũng có thể cải thiện độ tin cậy của phần mềm do AI tạo ra bằng cách chứng minh rằng mã cấp thấp đã được tối ưu hóa thực sự khớp với phiên bản tham chiếu dễ đọc hơn.
“Một phần rất lớn của giá trị nằm ở việc các bằng chứng này thực sự end-to-end,” Buterin viết. “Thông thường, những lỗi nguy hiểm nhất lại là lỗi tương tác nằm ở ranh giới giữa hai hệ thống con vốn được xem xét riêng biệt.”
Tuy nhiên, dù nhìn thấy tiềm năng của AI trong việc giúp bảo mật mã nguồn cho các mạng crypto, Buterin cũng cảnh báo rằng xác minh hình thức không thể loại bỏ hoàn toàn các rủi ro bảo mật.
“Xác minh hình thức không phải liều thuốc vạn năng. Nhưng nó đặc biệt phù hợp trong những trường hợp mục tiêu đơn giản hơn rất nhiều so với quá trình triển khai,” ông viết. “Điều này đặc biệt đúng với một số công nghệ cực kỳ phức tạp mà chúng ta sẽ cần triển khai trong phiên bản lớn tiếp theo của Ethereum: chữ ký kháng lượng tử, STARKs, thuật toán đồng thuận và ZK-EVM.”
Buterin bác bỏ quan điểm cho rằng các cuộc tấn công mạng ngày càng tinh vi cuối cùng sẽ khiến phần mềm mã nguồn mở hoặc các hệ thống phi tập trung trở nên không thể bảo mật.
“Đó sẽ là một tương lai u ám cho an ninh mạng. Và đặc biệt là một tương lai cực kỳ u ám đối với những người quan tâm đến sự phi tập trung và tự do của internet,” ông nói. “Toàn bộ tinh thần cypherpunk về cơ bản được xây dựng trên ý tưởng rằng trên internet, bên phòng thủ có lợi thế.”
Thay vào đó, Buterin cho rằng các hệ thống trong tương lai nhiều khả năng sẽ phụ thuộc vào một hạ tầng “lõi” có độ bảo mật cực cao, được bảo vệ thông qua xác minh hình thức và các môi trường bảo mật hạn chế.
“Khi nói đến lõi bảo mật, chúng ta không để mã lỗi tiếp tục nhân lên,” ông nói. “Chúng ta hành động quyết liệt để giữ kích thước của lõi bảo mật ở mức nhỏ, và thậm chí còn tiếp tục thu nhỏ nó hơn nữa.”
Bản tin Daily Debrief
Bắt đầu mỗi ngày với những tin tức nổi bật nhất, cùng các bài viết độc quyền, podcast, video và nhiều nội dung khác.
