(P1) Người đồng sáng lập Ethereum Vitalik Buterin cho biết việc xác minh chính thức có sự hỗ trợ của AI có thể loại bỏ phần lớn các lỗ hổng mã nguồn, một tuyên bố được đưa ra ngay khi một giao thức DeFi khác vừa mất 11,6 triệu USD do một vụ khai thác trên cầu nối Ethereum của nó.
(P2) "Nếu bạn xác minh chính thức từ đầu đến cuối, thì bạn đang chứng minh không chỉ một số mô tả của giao thức là an toàn về mặt lý thuyết, mà là đoạn mã cụ thể mà người dùng chạy là an toàn trong thực tế," Buterin đã viết trong một bài đăng blog xuất bản hôm thứ Hai. Ông lập luận rằng phương pháp này có thể cắt giảm hơn 99% hậu quả tiêu cực từ mã nguồn bị hỏng.
(P3) Các nhận xét của Buterin về bảo mật mã nguồn đã trở nên rõ ràng hơn sau một vụ khai thác được báo cáo của cầu nối Ethereum thuộc Verus Protocol. Các công ty bảo mật on-chain Blockaid và PeckShield báo cáo rằng một kẻ tấn công đã sử dụng tin nhắn chuyển chuỗi chéo giả mạo để rút tài sản, sau đó được chuyển đổi thành 5.402 Ether, trị giá hơn 11,4 triệu USD.
(P4) Sự cố này nhấn mạnh các rủi ro tài chính của lỗi phần mềm trong hệ sinh thái tiền mã hóa. Buterin tin rằng xác minh chính thức là điều cần thiết để bảo mật thế hệ cơ sở hạ tầng tiếp theo của Ethereum, đặc biệt là đối với các thành phần phức tạp và quan trọng như chữ ký kháng lượng tử, STARK và ZK-EVM.
Theo Blockaid, sự cố cầu nối Verus là do thiếu xác thực số tiền nguồn, một khiếm khuyết có thể được xác định và khắc phục bằng khoảng 10 dòng mã Solidity. Công ty bảo mật lưu ý cấu trúc của cuộc tấn công giống với các vụ khai thác năm 2022 của Nomad Bridge (190 triệu USD) và Wormhole (325 triệu USD), nơi các hướng dẫn gian lận đã đánh lừa các cầu nối gửi tiền từ nguồn dự trữ của họ.
Trong bài đăng của mình, Buterin đã mô tả một tương lai nơi các công cụ AI giúp các nhà phát triển viết cả mã nguồn hiệu quả cao và các bằng chứng toán học để xác minh tính chính xác của nó. Ông gọi sự kết hợp này là "hình thái cuối cùng của phát triển phần mềm" tiềm năng. Phương pháp này được coi là một biện pháp phòng thủ mạnh mẽ chống lại một tương lai nơi AI tiên tiến cũng có thể được sử dụng để phát hiện và thực hiện các cuộc tấn công mạng ở quy mô chưa từng có.
Mặc dù là một người ủng hộ mạnh mẽ, Buterin cảnh báo rằng xác minh chính thức "không phải là liều thuốc vạn năng", vì nó không thể loại bỏ tất cả các rủi ro bảo mật, chẳng hạn như những rủi ro bắt nguồn từ các giả định ban đầu sai lầm hoặc lỗ hổng phần cứng. Tuy nhiên, ông lập luận rằng nó đặc biệt phù hợp với các hệ thống mật mã phức tạp sẽ củng cố lộ trình tương lai của Ethereum, khiến mã nguồn gần như không có lỗi trở thành một kỳ vọng thực tế.
Bài viết này chỉ mang tính chất thông tin và không cấu thành lời khuyên đầu tư.
