Vitalik dự đoán tương lai không lỗi cho hợp đồng thông minh

Nguồn: CryptoNewsNet Tiêu đề gốc: Vitalik dự đoán tương lai không lỗi cho hợp đồng thông minh Liên kết gốc:

Tổng quan

Các nhà phát triển ưu tiên an ninh có thể mong đợi việc lập trình không lỗi trở thành khả thi vào những năm 2030, theo đồng sáng lập Ethereum Vitalik Buterin.

Sau đợt hard fork gây tranh cãi của Gnosis Chain nhằm khôi phục 9,4 triệu đô la từ vụ hack Balancer, đồng sáng lập Ethereum Vitalik Buterin cho biết niềm tin rằng “lỗi là không thể tránh khỏi, bạn không thể tạo ra mã không lỗi” sẽ không còn đúng vào những năm 2030.

Vitalik Buterin nói gì về lập trình?

Vitalik Buterin đã dự đoán rằng mã không lỗi sẽ trở thành hiện thực vào những năm 2030 thông qua một cuộc trò chuyện trên nền tảng mạng xã hội X.

Cuộc thảo luận bắt đầu khi Gnosis Chain thông báo rằng họ đã thực hiện một hard fork vào ngày 22 tháng 12. Hard fork này đã khôi phục 9,4 triệu đô la bị đánh cắp trong vụ khai thác Balancer tháng 11 năm 2024, đã rút sạch hơn $128 triệu đô la qua nhiều chuỗi khối. Việc khôi phục đòi hỏi phần lớn các validator phải cập nhật phần mềm mới, và những ai không cập nhật sẽ phải đối mặt với các hình phạt.

Điều này gặp phải sự phản đối từ những người ủng hộ blockchain, những người chỉ trích hành động này vì nó đi ngược lại nguyên tắc bất biến. Một người dùng X với biệt danh ‘colluding node’ nói rằng vấn đề thực sự là cách các ứng dụng blockchain được xây dựng. Họ lập luận rằng việc sử dụng hợp đồng thông minh trong các máy ảo có thể lập trình là cách tiếp cận sai.

“Chỉ có 7 hợp đồng đáng để viết, và chúng nên được ghi vào lớp nền và đảm bảo an ninh từ đa dạng khách hàng,” người dùng viết.

Buterin sau đó đã phản hồi bằng cách làm rõ rằng xác minh chính thức không đồng nghĩa với không lỗi có thể chứng minh được. Ông còn đi xa hơn khi đề xuất rằng mã không lỗi có thể chứng minh được thậm chí còn không khả thi.

“Tôi thậm chí còn nghĩ rằng ‘không lỗi có thể chứng minh’ là không thể, vì ‘không lỗi’ có nghĩa là ‘không có khoảng cách giữa ý định và thực thi mã’, và ý định của chúng ta là một đối tượng cực kỳ phức tạp mà chúng ta chỉ có giới hạn truy cập.”

Xác minh chính thức sử dụng các phương pháp toán học để kiểm tra xem các hệ thống quan trọng về an toàn có hoạt động chính xác hay không. Kỹ thuật này đã được sử dụng từ những năm 1960 trong các lĩnh vực như kỹ thuật hàng không vũ trụ.

Khi được sử dụng trong hợp đồng thông minh, xác minh chính thức có thể chứng minh rằng logic kinh doanh của hợp đồng đáp ứng một đặc tả xác định trước; tuy nhiên, mặc dù các hợp đồng Balancer đã được kiểm tra 11 lần, do bốn công ty an ninh riêng biệt thực hiện, vẫn còn một lỗi nghiêm trọng lọt qua.

Liệu tương lai mã không lỗi có khả thi?

Buterin đề xuất rằng giải pháp là nhiều lớp dự phòng để lọc bỏ các khoảng trống giữa ý định và thực thi. Ông chỉ ra hệ thống kiểu như một dạng dự phòng, và xác minh chính thức các tuyên bố cụ thể về mã như một lớp khác.

Xác minh chính thức có thể phát hiện các vấn đề như tràn số nguyên, tràn số, re-entrancy, và tối ưu gas kém có thể bị bỏ qua bởi các kiểm tra viên và kiểm thử. Trong khi đó, kiểm thử truyền thống chỉ có thể kiểm tra sự hiện diện của lỗi chứ không phải sự vắng mặt của chúng.

Buterin lưu ý rằng một số phần mềm sẽ tiếp tục có lỗi vì lợi ích của chức năng quan trọng hơn sự hoàn hảo trong một số trường hợp. Nhưng các nhà phát triển ưu tiên an ninh sẽ có các công cụ để đạt được mã không lỗi thực sự.