Vitalik's Latest Long Read: How Can Code Become Safer in the Age of AI?

Tiêu đề gốc: A shallow dive into formal verification

Tác giả gốc: Vitalik

Biên dịch gốc: Peggy, BlockBeats

Lời người biên tập: Với sự tiến bộ nhanh chóng của khả năng lập trình AI, an ninh phần mềm đang phải đối mặt với một nghịch lý mới: AI có thể tạo ra mã hiệu quả hơn, nhưng cũng có thể phát hiện lỗ hổng hiệu quả hơn. Đối với ngành công nghiệp tiền mã hóa, vấn đề này đặc biệt quan trọng. Một khi hợp đồng thông minh, bằng chứng ZK, thuật toán đồng thuận và hệ thống tài sản trên chuỗi xuất hiện khiếm khuyết, hậu quả thường không chỉ là lỗi phần mềm thông thường, mà là mất mát tài sản không thể đảo ngược và sự sụp đổ niềm tin.

Vitalik thảo luận trong bài viết này về một con đường khác cho bảo mật mã trong kỷ nguyên AI: xác minh hình thức. Nói một cách đơn giản, nó không phụ thuộc vào việc kiểm toán viên con người xem xét mã từng dòng một, mà là viết các tính chất mà chương trình cần thỏa mãn dưới dạng các mệnh đề toán học, sau đó sử dụng các bằng chứng có thể kiểm tra bằng máy để xác minh các tính chất này có đúng hay không. Trước đây, xác minh hình thức do ngưỡng cao và quy trình phức tạp, luôn nằm trong lĩnh vực nghiên cứu và kỹ thuật tương đối ít người biết đến; nhưng với sự trợ giúp của AI trong việc viết mã và bằng chứng, phương pháp này đang lấy lại ý nghĩa thực tiễn.

Nhận định cốt lõi của bài viết không phải là "xác minh hình thức có thể giải quyết mọi vấn đề an ninh". Ngược lại, Vitalik liên tục nhắc nhở rằng cái gọi là "bảo mật có thể chứng minh" không đồng nghĩa với bảo mật tuyệt đối: bằng chứng có thể bỏ sót các giả định quan trọng, bản thân thông số kỹ thuật có thể được viết sai, và mã chưa được xác minh, ranh giới phần cứng và các cuộc tấn công kênh phụ cũng có thể trở thành nguồn rủi ro mới. Nhưng nó vẫn cung cấp một mô hình bảo mật đáng tin cậy hơn: thể hiện ý định của nhà phát triển theo nhiều cách khác nhau, sau đó để hệ thống tự động kiểm tra xem các cách thể hiện này có tương thích với nhau hay không.

Điều này đặc biệt quan trọng đối với Ethereum. Trong tương lai, Ethereum sẽ ngày càng phụ thuộc vào các thành phần nền tảng phức tạp, bao gồm STARK, ZK-EVM, chữ ký kháng lượng tử, thuật toán đồng thuận và triển khai EVM hiệu suất cao. Việc triển khai các hệ thống này cực kỳ phức tạp, nhưng các mục tiêu bảo mật cốt lõi của chúng thường có thể được hình thức hóa một cách tương đối rõ ràng. Và chính trong những kịch bản như vậy, xác minh hình thức hỗ trợ AI có thể phát huy giá trị lớn nhất: để AI chịu trách nhiệm viết mã hiệu quả và bằng chứng, và để con người chịu trách nhiệm kiểm tra xem mệnh đề cuối cùng được chứng minh có thực sự tương ứng với mục tiêu bảo mật mà họ muốn hay không.

Từ góc nhìn vĩ mô hơn, bài viết này cũng là phản hồi của Vitalik đối với an ninh mạng trong kỷ nguyên AI. Đối mặt với những kẻ tấn công AI mạnh hơn, câu trả lời không phải là từ bỏ mã nguồn mở, từ bỏ hợp đồng thông minh, hoặc phụ thuộc lại vào một số ít tổ chức tập trung, mà là nén các hệ thống quan trọng thành một "lõi bảo mật" nhỏ hơn, dễ xác minh hơn và đáng tin cậy hơn. AI sẽ làm gia tăng đáng kể lượng mã thô sơ, nhưng cũng có thể làm cho mã thực sự quan trọng trở nên an toàn hơn so với trước đây.

Sau đây là nội dung gốc:

Đặc biệt cảm ơn Yoichi Hirai, Justin Drake, Nadim Kobeissi và Alex Hicks đã cung cấp phản hồi và đánh giá cho bài viết này.

Trong vài tháng qua, một mô hình lập trình mới đang nhanh chóng nổi lên trong giới nghiên cứu tiên phong của Ethereum và nhiều ngóc ngách khác trong lĩnh vực máy tính: các nhà phát triển viết mã trực tiếp bằng các ngôn ngữ rất cấp thấp, chẳng hạn như bytecode EVM, hợp ngữ, hoặc viết mã bằng Lean, và xác minh tính đúng đắn của nó bằng cách viết các bằng chứng toán học có thể tự động kiểm tra trong Lean.

Nếu được sử dụng đúng cách, phương pháp này vừa có khả năng tạo ra mã cực kỳ hiệu quả, vừa có thể an toàn hơn nhiều so với các phương pháp phát triển phần mềm trước đây. Yoichi Hirai gọi nó là "hình thái cuối cùng của phát triển phần mềm". Bài viết này sẽ cố gắng giải thích logic cơ bản đằng sau phương pháp này: xác minh hình thức phần mềm có thể làm được gì, và điểm yếu cũng như ranh giới của nó ở đâu - dù là trong bối cảnh Ethereum hay trong lĩnh vực phát triển phần mềm rộng lớn hơn.

Xác minh hình thức là gì?

Xác minh hình thức, đề cập đến việc viết các bằng chứng của các định lý toán học theo cách có thể được máy móc tự động kiểm tra.

Để đưa ra một ví dụ tương đối đơn giản nhưng vẫn thú vị, chúng ta có thể xem xét một định lý cơ bản về dãy số Fibonacci: cứ ba số thì có một số chẵn, hai số còn lại là số lẻ.

Một phương pháp chứng minh đơn giản là sử dụng quy nạp toán học, mỗi lần tiến về phía trước ba số.

Đầu tiên, xem xét trường hợp cơ bản. Đặt F1 = F2 = 1, F3 = 2. Qua quan sát trực tiếp, có thể thấy mệnh đề này - "khi i là bội số của 3, Fi là số chẵn; trong các trường hợp khác, Fi là số lẻ" - đều đúng trước x = 3.

Tiếp theo là bước quy nạp. Giả sử mệnh đề đúng trước 3k+3, nghĩa là chúng ta đã biết tính chẵn lẻ của F3k+1, F3k+2, F3k+3 lần lượt là lẻ, lẻ, chẵn. Sau đó, chúng ta có thể tính tính chẵn lẻ của ba số tiếp theo:

Từ đó, chúng ta đã hoàn thành suy luận từ "mệnh đề đã biết đúng trước 3k+3" đến "xác nhận mệnh đề cũng đúng trước 3k+6". Chỉ cần lặp lại suy luận này, chúng ta có thể tin tưởng rằng quy luật này đúng với mọi số nguyên.

Lập luận này có sức thuyết phục đối với con người. Nhưng điều gì sẽ xảy ra nếu điều bạn muốn chứng minh phức tạp hơn gấp trăm lần và bạn thực sự muốn chắc chắn rằng mình không mắc lỗi? Lúc đó, bạn có thể xây dựng một bằng chứng mà máy tính cũng có thể tin được.

Nó sẽ trông đại khái như thế này:

Đây là cùng một suy luận, nhưng được diễn đạt bằng Lean. Lean là một ngôn ngữ lập trình thường được sử dụng để viết và xác minh các bằng chứng toán học.

Nó trông rất khác so với phiên bản "dành cho con người" mà tôi đưa ra ở trên, và có lý do chính đáng cho điều đó: những gì trực quan đối với máy tính hoàn toàn khác với những gì trực quan đối với con người. Máy tính được đề cập ở đây là "máy tính" theo nghĩa cũ - các chương trình "xác định" được cấu thành từ các câu lệnh if/then, không phải các mô hình ngôn ngữ lớn.

Trong bằng chứng trên, bạn không nhấn mạnh thực tế rằng fib(3k+4) = fib(3k+3) + fib(3k+2); bạn nhấn mạnh rằng fib(3k+3) + fib(3k+2) là số lẻ, và chiến thuật omega có tên khá hoành tráng trong Lean sẽ tự động kết hợp điều này với sự hiểu biết của nó về định nghĩa của fib(3k+4).

Trong các bằng chứng phức tạp hơn, đôi khi bạn phải nêu rõ ở mỗi bước: chính xác là định luật toán học nào cho phép bạn thực hiện bước đó, và những định luật này đôi khi mang những cái tên khá khó hiểu, như Prod.mk.inj. Mặt khác, bạn cũng có thể mở rộng các biểu thức đa thức khổng lồ chỉ trong một bước và chỉ cần viết một dòng biểu thức như omega hoặc ring để hoàn thành lập luận.

Sự không trực quan và phức tạp này chính là lý do quan trọng khiến các bằng chứng có thể kiểm tra bằng máy dù đã tồn tại gần 60 năm, nhưng vẫn chỉ giới hạn trong một lĩnh vực nhỏ. Nhưng đồng thời, nhiều điều gần như không thể trong quá khứ, giờ đây đang nhanh chóng trở nên khả thi nhờ sự tiến bộ vượt bậc của AI.

Xác minh chương trình máy tính

Đến đây, bạn có thể nghĩ: Được rồi, vậy chúng ta có thể để máy tính xác minh các bằng chứng của định lý toán học, để cuối cùng chúng ta có thể xác định, trong số những khám phá mới điên rồ về số nguyên tố, cái nào là thật, cái nào chỉ là lỗi ẩn trong các tài liệu PDF hàng trăm trang. Có lẽ chúng ta thậm chí còn có thể tìm ra liệu bằng chứng của Shinichi Mochizuki về giả thuyết ABC có đúng hay không! Nhưng ngoài việc thỏa mãn trí tò mò, điều này còn có ý nghĩa thực tế gì?

Có thể có nhiều câu trả lời. Và đối với tôi, một câu trả lời rất quan trọng là: xác minh tính đúng đắn của các chương trình máy tính, đặc biệt là những chương trình liên quan đến mật mã hoặc bảo mật. Rốt cuộc, bản thân chương trình máy tính là một đối tượng toán học. Do đó, chứng minh rằng một chương trình máy tính sẽ hoạt động theo một cách nhất định, về bản chất là chứng minh một định lý toán học.

Ví dụ, giả sử bạn muốn chứng minh liệu một phần mềm liên lạc mã hóa như Signal có thực sự an toàn hay không. Trước tiên, bạn có thể viết một cách toán học, "an toàn" trong bối cảnh này có nghĩa là gì. Tóm lại, bạn cần chứng minh rằng: dưới một số giả định mật mã nhất định, chỉ những người có khóa riêng mới có thể biết được bất kỳ thông tin nào về nội dung tin nhắn. Trong thực tế, tất nhiên có nhiều thuộc tính bảo mật thực sự quan trọng.

Và hóa ra, đã có một nhóm đang cố gắng tìm hiểu điều này. Một trong những định lý bảo mật mà họ đưa ra, trông đại khái như thế này:

Dưới đây là bản tóm tắt của Leanstral về ý nghĩa của định lý này:

Định lý passive_secrecy_le_ddh là một sự quy giản chặt chẽ, cho thấy rằng dưới mô hình Oracle ngẫu nhiên (Random Oracle Model), tính bí mật thụ động của X3DH ít nhất cũng khó bị phá vỡ như giả định DDH.

Nói cách khác, nếu kẻ tấn công có thể phá vỡ tính bí mật thụ động của X3DH, thì chúng cũng có thể phá vỡ DDH. Vì DDH thường được giả định là một bài toán khó, nên X3DH cũng có thể được coi là có khả năng chống lại các cuộc tấn công thụ động.

Định lý này chứng minh rằng nếu kẻ tấn công chỉ có thể thụ động quan sát các thông điệp trao đổi khóa của Signal, thì chúng không thể phân biệt khóa phiên cuối cùng được tạo ra với một khóa ngẫu nhiên với xác suất cao hơn một cách đáng kể so với ngẫu nhiên.

Nếu kết hợp với một bằng chứng chứng minh rằng mã hóa AES được triển khai chính xác, thì bạn có thể có một bằng chứng: cơ chế mã hóa của giao thức Signal có khả năng chống lại các cuộc tấn công thụ động.

Các dự án xác minh tương tự c