Vitalik phân tích sự phát triển và hạn chế của xác minh hình thức, cuộc thảo luận về việc phát triển phần mềm trong kỷ nguyên AI bước vào "hình thái cuối cùng" nóng lên
Tin tức từ Odaily, đồng sáng lập Ethereum Vitalik Buterin đã đăng bài viết "A shallow dive into formal verification", hệ thống hóa những phát triển và hạn chế mới nhất của xác minh hình thức (Formal Verification) trong Ethereum và các lĩnh vực máy tính rộng lớn hơn. Bài báo chỉ ra rằng trong những tháng gần đây, trong giới nghiên cứu tiên phong của Ethereum, một mô hình lập trình mới đang nhanh chóng nổi lên: các nhà phát triển sử dụng trực tiếp các ngôn ngữ cực kỳ cấp thấp (như EVM bytecode, assembly) hoặc Lean, và xác minh tính đúng đắn của mã thông qua các chứng minh toán học có thể tự động xác minh. Về mặt lý thuyết, phương pháp này vừa có thể nâng cao hiệu quả mã, vừa cải thiện đáng kể tính bảo mật, được một số nhà nghiên cứu gọi là "hình thái cuối cùng của phát triển phần mềm".
Vitalik cho biết, cốt lõi của xác minh hình thức là xác minh các thuộc tính của chương trình thông qua các chứng minh toán học có thể kiểm tra bằng máy, giá trị của nó nằm ở chỗ chuyển đổi "tính bảo mật" từ kiểm thử kinh nghiệm sang hệ thống logic có thể chứng minh. Trong truyền thông mã hóa, giao thức mật mã và hệ thống blockchain (như bằng chứng không kiến thức và cơ chế đồng thuận), phương pháp này đã bắt đầu được sử dụng để xác minh hành vi hệ thống quan trọng từ đầu đến cuối.
Bài báo cũng chỉ ra rằng hệ sinh thái Ethereum đang khám phá các dự án xác minh hình thức cho cơ sở hạ tầng quan trọng bao gồm triển khai EVM, hệ thống bằng chứng STARK và chữ ký chống lượng tử, nhằm nâng cao tính bảo mật và độ tin cậy ở cấp độ giao thức. Tuy nhiên, Vitalik cũng nhấn mạnh rằng xác minh hình thức không phải là "viên đạn bạc". Những hạn chế của nó bao gồm: định nghĩa bảo mật phụ thuộc vào mô hình hóa của con người, một số hệ thống khó có thể được hình thức hóa hoàn chỉnh, và phần cứng hoặc các mô-đun không được xác minh vẫn có thể trở thành bề mặt tấn công. Ngoài ra, ngay cả khi có chứng minh hình thức, các lỗi đặc tả hoặc các giả định không được bao phủ vẫn có thể dẫn đến lỗ hổng.
Cuối cùng, Vitalik đề xuất rằng con đường thực tế hơn là kết hợp xác minh hình thức với các phương pháp khác như lập trình hỗ trợ AI, hệ thống kiểu, khung kiểm thử, để dần dần nâng cao tính bảo mật phần mềm trong khuôn khổ "thể hiện ý định một cách dư thừa và tự động xác minh tính nhất quán". Trong xu hướng AI tạo mã trên quy mô lớn, các hệ thống phần mềm sẽ dần phân hóa thành "các mô-đun biên dễ bị tấn công" và "lõi bảo mật đáng tin cậy cao". Trong tương lai, nên tập trung áp dụng xác minh hình thức vào các hệ thống cốt lõi (như giao thức blockchain, nhân hệ điều hành, v.v.) để xây dựng cơ sở hạ tầng kỹ thuật số có thể xác minh tính bảo mật.
