原文標題：Một cái nhìn sơ lược về xác minh hình thức

Người viết bài gốc: Vitalik

Dịch thuật: Peggy, BlockBeats

Chú thích biên tập viên: Trong bối cảnh khả năng lập trình AI đang phát triển nhanh chóng, an ninh phần mềm đang đối diện với một nghịch lý mới: AI có thể tạo mã nguồn 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 điện tử, vấn đề này đặc biệt quan trọng. 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 mắc phải lỗi, hậu quả thường không phải là mã lỗi phần mềm thông thường, mà là mất tiền không thể đảo ngược và suy thoái niềm tin.

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

Quyết đị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 tất cả vấn đề an ninh". Ngược lại, Vitalik luôn nhấn mạnh, việc "an toàn có thể chứng minh" không có nghĩa là tuyệt đối an toàn: bằng chứng có thể bỏ sót giả định quan trọng, phần mô tả có thể viết sai, mã chưa được xác minh, ranh giới phần cứng và 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 an toàn đáng tin cậy hơn: biểu diễn ý định của nhà phát triển bằng nhiều cách, rồi để hệ thống tự động kiểm tra xem những biểu diễ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. Tương lai của Ethereum sẽ ngày càng phụ thuộc vào các thành phần hạ tầng phức tạp, bao gồm STARK, ZK-EVM, chữ ký chống lượng tử, thuật toán đồng thuận và triển khai EVM hiệu suất cao. Triển khai của các hệ thống này cực kỳ phức tạp, nhưng mục tiêu an toàn cốt lõi thường có thể được định rõ tương đối. Chính trong các tình huống như vậy, việc xác minh hình thức với sự hỗ trợ của AI có thể phát huy giá trị lớn nhất: để AI viết mã nguồn hiệu quả và bằng chứng, để con người kiểm tra xem những bài toán đã được chứng minh cuối cùng có thực sự tương ứng với mục tiêu an toàn mà họ mong muốn hay không.

Trong cái nhìn bao quát hơn, bài viết này cũng là một phản ứng của Vitalik đối với an ninh mạng trong thời đại AI. Đối mặt với các kẻ tấn công AI mạnh mẽ 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ục hồi lại sự phụ thuộc vào một vài cơ quan tập trung, mà là nén các hệ thống quan trọng thành "lõi an toàn" nhỏ hơn, có thể xác minh được, đáng tin cậy hơn. AI có thể khiến cho mã lỗi trở nên phổ biến hơn, 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 quá khứ.

Dưới đây là văn bản gốc:

Đặc biệt cảm ơn Yoichi Hirai, Justin Drake, Nadim Kobeissi và Alex Hicks đã đưa ra phản hồi và xem xét văn bản 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 cộng đồng nghiên cứu phát triển Ethereum và nhiều góc khác của lĩnh vực tính toán: nhà phát triển trực tiếp viết mã bằng ngôn ngữ cực kỳ cấp thấp như bytecode EVM, ngôn ngữ hợp ngữ, hoặc viết mã bằng Lean và sau đó chứng minh toán học có thể tự động kiểm tra tính đúng đắn của mã của họ thông qua việc viết chứng minh chặt chẽ trong Lean.

Nếu được áp dụng đúng cách, phương pháp này có khả năng tạo ra mã cực kỳ hiệu quả và an toàn hơn nhiều so với cách phát triển phần mềm trước đây. Yoichi Hirai gọi đó là "hình thức 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 gì, điểm yếu và giới hạn của nó - cho dù trong ngữ cảnh Ethereum hay trong lĩnh vực phát triển phần mềm rộng lớn hơn.

Formal Verification là gì?

Xác minh hình thức, tức việc viết chứng minh toán học một cách có thể được máy tính tự động kiểm tra.

Để cho 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: mỗi ba số có một số chẵn và hai số còn lại là số lẻ.

Một cách đơn giản để chứng minh là sử dụng phương pháp quy nạp, mỗi lần di chuyển ba số lên.

Đầu tiên, xem xét trường hợp cơ sở. Giả sử F1 = F2 = 1, F3 = 2. Bằng cách quan sát trực tiếp, có thể thấy rằng 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ẻ" - đúng cho tất cả x <3.

Tiếp theo là bước quy nạp. Giả sử rằng mệnh đề này đúng cho 3k + 3 trước đó, 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à số lẻ, số lẻ, số chẵn. Do đó, chúng ta có thể tính tính chẵn lẻ của ba số tiếp theo:

Qua đó, chúng ta hoàn thành việc chứng minh từ "mệnh đề đã biết ở 3k + 3 trước đó đúng" sang "xác nhận mệnh đề cũng đúng ở 3k + 6". Chỉ cần lặp đi lặp lại quá trình suy luận này, chúng ta có thể tin chắc rằng quy luật này đúng cho tất cả số nguyên.

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

Nó sẽ gần như như thế này:

Đó là cùng một quy luận, nhưng được biểu diễn bằng Lean. Lean là một loại 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 khác hẳn so với bản "dành cho con người" ở trên, điều này hoàn toàn có lý do: điều mà máy tính hiểu một cách trực quan, và điều mà con người hiểu một cách trực quan hoàn toàn khác nhau. Ở đây, khi nói đến máy tính, là theo nghĩa cũ của "máy tính" - một chương trình "xác định" được tạo bởi các câu lệnh if/then, không phải mô hình ngôn ngữ lớn.

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

Trong các bằng chứng phức tạp hơn, đôi khi bạn cần phải rõ ràng từng bước: đó là quy luật toán học nào cho phép bạn tiến đến bước đó, và những quy luật này đôi khi đi kèm với những tên rất khó hiểu, như Prod.mk.inj. Nhưng ở một khía cạnh khác, bạn cũng có thể mở rộng một biểu thức đa thức lớn và chỉ cần viết một dòng như omega hoặc ring, bạn đã có thể hoàn thành bằng chứng.

Sự không trực quan và phiền toái ở đây chính là lý do quan trọng về tại sao bằng chứng máy tính có thể xác minh đã tồn tại gần 60 năm, nhưng vẫn chỉ duy trì ở trình độ nhỏ. Nhưng đồng thời, nhiều điều mà trước đây gần như là không thể, bây giờ đang trở thành khả thi vì sự tiến bộ nhanh chóng của trí tuệ nhân tạo.

Xác minh Chương trình Máy tính

Ở đây, bạn có thể nghĩ: Vậy, vậy là chúng ta có thể cho máy tính xác minh bằng chứng toán học, để cuối cùng chúng ta có thể xác định xem những phát hiện mới điên rồ về số nguyên tố đó, thực sự là đúng hay chỉ là lỗi ẩn trong bài báo khoảng cách 100 trang PDF. Có lẽ chúng ta thậm chí còn có thể làm rõ xem bằng chứng của Ảo Tuyết về Giả thuyết ABC có chính xác không! Nhưng ngoài việc chỉ thoả mãn sự hiếu kỳ, việc này có ý nghĩa gì trong thực tế?

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 chính xác của các chương trình máy tính, đặc biệt là các chương trình liên quan đến mật mã hoặc bảo mật. Cuối cùng, chính 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ẽ chạy theo một cách cụ thể, 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 xem liệu phần mềm truyền thông mã hóa như Signal có thực sự an toàn hay không. Bạn có thể bắt đầu bằng cách viết một cách toán học rõ ràng, trong bối cảnh này, từ "an toàn" thực sự có nghĩa là gì. Nói một cách ngắn gọn, bạn muốn chứng minh rằng: Dưới giả thiết một số giả thuyết mật mã cụ thể, chỉ có người sở hữu khóa riêng tư mới có thể biết bất kỳ thông tin nào về nội dung tin nhắn. Trên thực tế, có nhiều thuộc tính an toàn thực sự quan trọng.

Và thực tế đã chứng minh rằng đã có một nhóm đang cố gắng làm sáng tỏ vấn đề này. Một trong những định lý an toàn mà họ đưa ra có vẻ như sau:

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

Định lý passive_secrecy_le_ddh là một rút gọn chặt chẽ, chỉ ra rằng dưới mô hình truyền thông ngẫu nhiên (Random Oracle Model), tính bảo mật tin nhắn chủ động của X3DH ít nhất cũng khó bẻ được như giả thiết DDH.

Nói cách khác, nếu kẻ tấn công có thể xâm nhập vào tính bảo mật tin nhắn chủ động của X3DH, họ cũng có thể xâm nhập vào DDH. Vì giả thiết DDH thường được cho là một vấn đề khó khăn, nên X3DH cũng có thể được coi là có khả năng chống lại cuộc tấn công chủ động.

Định lý này chứng minh rằng nếu kẻ tấn công chỉ có thể quan sát pas-sive Signal của thông điệp trao đổi khóa, họ sẽ không thể phân biệt khóa phiên cuối cùng được tạo ra khỏi một khóa ngẫu nhiên với một lợi thế vượt trội vượt qua thông số có thể bỏ qua.

Nếu kết hợp với một bằng chứng khẳng định rằng mã hóa AES được triển khai đúng cách, thì bạn có thể nhận được một bằng chứng: Cơ chế mã hóa của giao thức Signal có thể chống lại kẻ tấn công chủ động.

Một số dự án xác minh tương tự cũng đã tồn tại, chúng được sử dụng để chứng minh sự triển khai mã an toàn của TLS và các thành phần mật mã trong trình duyệt khác.

Nếu bạn có thể thực hiện xác minh hình thành đến hình thành, thì điều bạn chứng minh không chỉ là một giao thức cụ thể được mô tả trên lý thuyết là an toàn, mà còn mã nguồn cụ thể mà người dùng thực sự chạy cũng an toàn trong thực tế. Từ góc nhìn của người dùng, điều này sẽ nâng cao đáng kể mức độ "không cần tin cậy": Để tin tưởng hoàn toàn vào mã nguồn đó, bạn không cần phải kiểm tra từng dòng mã trong toàn bộ thư viện mã nguồn, chỉ cần kiểm tra những tuyên bố đã được chứng minh đúng.

Tất nhiên, có một số dấu sao cực kỳ quan trọng cần được giữ lại ở đây, đặc biệt là về từ khoá "an toàn" có nghĩa gì chính xác. Mọi người thường dễ quên điều quan trọng thực sự cần được chứng minh; cũng dễ gặp trường hợp: điều cần chứng minh không tồn tại một cách mô tả súc tích hơn mã nguồn bản thân; cũng dễ dàng giới thiệu một số giả thiết không chính xác cuối cùng vào trong việc chứng minh. Bạn cũng có thể dễ dàng kết luận rằng chỉ một phần của hệ thống thực sự cần phải được chứng minh hình thức, nhưng cuối cùng được tìm thấy một lỗ hổng quan trọng ở một phần khác, thậm chí ở mức phần cứng, bị lỗ hổng chính. Ngay cả việc triển khai Lean chính mình cũng có thể chứa lỗi. Nhưng trước khi thảo luận về những chi tiết đau đầu này, hãy cùng nhìn xem: Nếu xác minh hình thức có thể được thực hiện một cách lý tưởng và chính xác, nó có thể mang lại tầm nhìn gần như Utopia như thế nào.

Đảm bảo An toàn qua Xác minh Hình thức

Lỗi trong mã máy tính đã khiến chúng ta lo lắng.

Khi bạn đặt tiền điện tử vào một hợp đồng thông minh không thể thay đổi, lỗi trong mã sẽ trở nên đáng sợ hơn. Vì nếu có lỗi trên mã, các hacker có thể tự động chuyển toàn bộ tiền của bạn mà bạn gần như không có cách nào để đòi lại.

Khi tất cả điều này được bao bọc trong bằng chứng không cần biết, lỗi trong mã sẽ trở nên đáng sợ hơn. Vì nếu có ai đó tấn công thành công hệ thống bằng chứng không cần biết, họ có thể rút hết tiền và chúng ta có thể hoàn toàn không biết vấn đề ở đâu—hoặc hơn nữa, chúng ta có thể không nhận ra rằng vấn đề đã xảy ra.

Khi chúng ta có một mô hình AI mạnh mẽ, lỗi trong mã sẽ trở nên đáng sợ hơn. Ví dụ, một mô hình như Claude Mythos, sau hai năm cải tiến, có thể tự động phát hiện các lỗ hổng này.

Một số người đối mặt với sự thực này bắt đầu đề xuất từ bỏ ý tưởng cơ bản về hợp đồng thông minh, thậm chí nghĩ rằng không gian mạng không thể trở thành lĩnh vực có lợi thế không đối xứng của bên phòng thủ so với bên tấn công.

Dưới đây là một số trích dẫn:

Để củng cố một hệ thống, bạn cần chi tiêu token vào việc phát hiện lỗ hổng nhiều hơn so với attacker chi tiêu vào việc lợi dụng lỗ hổng.

Và còn:

Ngành công nghiệp của chúng ta được xây dựng xung quanh mã xác định. Viết mã, kiểm thử, triển khai, sau đó biết rằng nó sẽ hoạt động bình thường—nhưng theo kinh nghiệm của tôi, hợp đồng này đang bắt đầu thất bại. Trong số những công ty hoạt động đỉnh cao thực sự AI, kho lưu trữ mã đã bắt đầu biến thành một cái gì đó mà bạn « tin rằng nó sẽ hoạt động », và khả năng tương ứng với sự tin tưởng đó không thể được mô tả chính xác.

Càng tồi tệ hơn, một số người cho rằng, duy nhất giải pháp là từ bỏ mã nguồn mở.

Đối với an ninh mạng, điều này sẽ là một tương lai u ám. Đặc biệt đối với những người quan tâm đến mạng lưới phi trung tâm và tự do trên Internet, điều này sẽ là một tương lai cực kỳ u ám. Toàn bộ tinh thần hacker mật mã, về bản chất xây dựng trên một ý tưởng như vậy: trong Internet, bên phòng thủ có lợi thế. Xây dựng một « thành trì » kỹ thuật số—cho dù nó thể hiện qua mã hóa, chữ ký hay chứng minh—sẽ dễ hơn phá hủy nó rất nhiều. Nếu chúng ta mất điều này, thì an ninh Internet sẽ chỉ đến từ quy mô kinh tế, từ việc truy vết tấn công viên tiềm năng trên toàn thế giới, hoặc hẹp hơn, từ một dạng hai lựa chọn: hoặc kiểm soát tất cả, hoặc tiến vào sự phá hủy.

Tôi không đồng ý với sự đánh giá này. Đối với tương lai an ninh mạng, tôi có một tầm nhìn lạc quan hơn nhiều.

Tôi tin rằng thách thức do khả năng phát hiện lỗi AI mạnh mẽ mang lại thật sự nghiêm trọng, nhưng đó chỉ là một thách thức chuyển tiếp. Khi bụi giảm, chúng ta bước vào một trạng thái cân bằng mới, chúng ta sẽ đạt được một trạng thái thuận lợi hơn cho phía phòng thủ so với quá khứ.

Mozilla cũng đồng ý với quan điểm này. Trích dẫn từ họ:

Bạn có thể cần phải sắp xếp lại ưu tiên của tất cả các công việc khác để đầu tư vào nhiệm vụ này một cách liên tục và tập trung. Nhưng cuối hầm đèn là có ánh sáng. Chúng tôi rất tự hào khi thấy nhóm làm thế nào để đối mặt với thách thức này, và người khác cũng sẽ làm được. Công việc của chúng tôi vẫn chưa hoàn thành, nhưng chúng tôi đã vượt qua điểm khó khăn và bắt đầu nhìn thấy một tương lai tốt hơn, không chỉ là "theo kịp" mà còn hơn thế. Phía phòng thủ cuối cùng đã có cơ hội chiến thắng quyết định.

…

Số lượng khuyết điểm là có hạn, và chúng tôi đang bước vào một thế giới cuối cùng có thể phát hiện tất cả chúng.

Bây giờ, nếu bạn tìm kiếm các từ "formal" và "verification" bằng Ctrl + F trong bài viết của Mozilla này, bạn sẽ không thấy bất kỳ từ khóa nào. Tương lai tích cực của an ninh mạng không phụ thuộc chặt chẽ vào xác nhận hình thức, cũng như không phụ thuộc vào bất kỳ công nghệ đơn lẻ nào khác.

Vậy nó phụ thuộc vào điều gì? Về cơ bản, đó là bức tranh dưới đây:

Trong vài thập kỷ qua, nhiều công nghệ đã thúc đẩy xu hướng "giảm số lượng lỗi":

Hệ thống loại;

Ngôn ngữ an toàn bộ nhớ;

Cải tiến kiến trúc phần mềm, bao gồm hộp cát, cơ chế quyền và sự phân biệt rõ ràng hơn giữa "cơ sở tính toán đáng tin cậy" và "mã khác";

Các phương pháp kiểm thử tốt hơn;

Hiểu biết về các mô hình mã lỗi và không an toàn;

Thư viện phần mềm viết trước và được kiểm tra trước.

Xác nhận hình thức được hỗ trợ bởi AI không nên được coi là một mô hình hoàn toàn mới, mà nên được xem xét là một công cụ tăng tốc mạnh mẽ: nó đang tăng tốc cho một xu hướng và mô hình đã tiến triển từ trước.

Xác nhận hình thức không phải là phương thuốc thần kỳ. Nhưng ở một số tình huống, điều này đặc biệt hiệu quả: nghĩa là khi mục tiêu so với việc triển khai cụ thể đơn giản hơn rất nhiều. Điều này rất rõ ràng trong một số công nghệ phức tạp như chữ ký chống lượng tử, STARK, thuật toán đồng thuận và ZK-EVM cần triển khai trong cập nhật lớn kế tiếp của Ethereum.

STARK là một bộ phần mềm rất phức tạp. Tuy nhiên, các thuộc tính bảo mật cốt lõi mà nó thực hiện lại rất dễ hiểu và dễ hình thức hóa: Nếu bạn nhìn thấy một bằng chứng chỉ đến chương trình P, đầu vào x và băm H của đầu ra y, thì hoặc là thuật toán băm mà STARK sử dụng đã bị đột phá, hoặc là P(x) = y. Do đó, chúng tôi có Dự án Arklib, nơi cố gắng tạo ra một bản triển khai STARK đã được hình thức hóa kiểm chứng đầy đủ. Một dự án liên quan khác là VCV-io, cung cấp cơ sở hạ tầng tính toán siêu việt cơ bản, có thể được sử dụng để kiểm chứng hình thức cho các giao thức mật mã khác nhau, trong đó nhiều giao thức chính là thành phần phụ thuộc của STARK.

Ambitious hơn nữa là evm-asm: Đây là một dự án cố gắng xây dựng một triển khai EVM đầy đủ và kiểm chứng hình thức cho nó. Ở đây, các thuộc tính bảo mật không rõ ràng như vậy. Để đơn giản, mục tiêu của nó là chứng minh rằng triển khai này tương đương với một triển khai EVM khác được viết bằng Lean; trong khi triển khai này có thể theo đuổi sự trực quan và dễ đọc nhất mà không cần quan tâm đến hiệu suất chạy cụ thể.

Tất nhiên, lý thuyết vẫn có thể xảy ra một trường hợp như vậy: Chúng ta có mười triển khai EVM, chúng được chứng minh tương đương với nhau, nhưng tất cả đều chia sẻ một lỗi chết người chung, và lỗi này ở dạng nào đó để kẻ tấn công có thể chuyển đi tất cả ETH từ một địa chỉ không có quyền điều khiển. Nhưng so với trường hợp một triển khai EVM hiện nay có lỗi như vậy, khả năng xảy ra trường hợp này thấp hơn nhiều. Một thuộc tính bảo mật khác mà chúng ta thực sự nhận ra tầm quan trọng sau một kinh nghiệm đau đớn là khả năng chống lại DoS, và điều này có thể được định rõ một cách tương đối dễ dàng.

Hai hướng quan trọng khác là:

Một số sự nhượng bộ Byzantine Fault Tolerance. Trong hướng này, việc định nghĩa hình thức cho tất cả các thuộc tính bảo mật được kỳ vọng không dễ dàng như một. Nhưng vì các bug liên quan đã luôn rất phổ biến, việc thử nghiệm hình thức vẫn đáng giá. Vì vậy, hiện đã có một số công việc đang diễn ra về triển khai chứng minh Lean và Byzantine Fault Tolerance.

Ngôn ngữ lập trình hợp đồng thông minh. Các ví dụ liên quan bao gồm các công việc kiểm chứng hình thức trong Vyper và Verity.

Trong tất cả các trường hợp này, một giá trị gia tăng lớn từ hình thức hóa kiểm chứng đến từ: Các bằng chứng này thực sự là kết quả của việc từ đầu đến cuối. Rất nhiều bug khó nhất thường là bug tương tác, chúng xuất hiện ở ranh giới của hai hệ thống con được xem xét riêng biệt. Đối với con người, suy luận từ đầu đến cuối của toàn bộ hệ thống quá khó khăn; nhưng hệ thống kiểm tra quy tắc tự động có thể thực hiện được.

Kiểm chứng hình thức hóa định hướng hiệu quả

Chúng ta hãy xem lại evm-asm. Đó là một triển khai EVM.

Nhưng đó là một bản hiện thực của EVM được viết bằng ngôn ngữ hợp ngữ RISC-V trực tiếp.

Thực sự là hợp ngữ đen trắng.

Đây là Mã vận hành ADD:

Lý do chọn RISC-V là vì bộ chứng minh ZK-EVM đang được xây dựng hiện nay thường được chứng minh bằng RISC-V, và dịch vụ khách hàng Ethereum thường được biên dịch thành RISC-V để làm việc. Do đó, nếu bạn viết một bản hiện thực EVM trực tiếp bằng RISC-V, lí thuyết là đó sẽ là bản hiện thực nhanh nhất mà bạn có thể có được. RISC-V cũng có thể được mô phỏng chạy hiệu quả trên máy tính thông thường, và đã có cả máy tính xách tay RISC-V. Tất nhiên, nếu bạn muốn thực sự đi từ đầu đến cuối, bạn cũng phải thực hiện xác minh hình thức cho chính bản hiện thực RISC-V, hoặc biểu diễn số học của bộ chứng minh. Nhưng đừng lo lắng—loại công việc này cũng đã tồn tại.

Việc viết mã trực tiếp bằng hợp ngữ là điều chúng ta thường làm cách đây năm mươi năm. Kể từ đó, chúng ta dần chuyển sang viết mã bằng ngôn ngữ cao cấp. Ngôn ngữ cao cấp sẽ hy sinh một số hiệu suất nhưng để đổi lại, nó đã tăng tốc độ viết mã rất nhiều, và điều quan trọng hơn, đã dễ hiểu mã của người khác nhanh chóng hơn—điều này là điều bắt buộc với mục đích bảo mật.

Với sự kết hợp giữa xác minh hình thức và trí tuệ nhân tạo, chúng ta có cơ hội "quay trở lại tương lai". Cụ thể, là để cho trí tuệ nhân tạo viết hợp ngữ, sau đó viết một bản chứng minh hình thức, xác minh rằng hợp ngữ đó có các thuộc tính mà chúng ta muốn. Ít nhất, thuộc tính mục tiêu này có thể chỉ đơn giản là: nó hoàn toàn tương đương với một bản hiện thực được viết bằng một ngôn ngữ cấp cao được tối ưu hóa cho tính đọc hiểu.

Khi đó, bạn sẽ không còn cần phải cân bằng giữa tính đọc hiểu và hiệu suất trong một đối tượng mã duy nhất. Chúng ta sẽ có hai đối tượng cách biệt nhau: một là bản hiện thực hợp ngữ, mà chỉ được tối ưu hóa cho hiệu suất, và điều chỉnh theo yêu cầu của môi trường thực thi cụ thể; và hai là yêu cầu an ninh, hoặc bản hiện thực ngôn ngữ cao cấp, mà chỉ được tối ưu hóa cho tính đọc hiểu. Sau đó, chúng ta lại sử dụng một bản chứng minh toán học để chứng minh sự tương đương giữa hai đối tượng. Người dùng có thể xác minh chứng minh này tự động một lần; sau đó, họ chỉ cần chạy phiên bản nhanh chóng đó.

Điều này rất mạnh mẽ. Yoichi Hirai đã gọi đó là "hình thức cuối cùng của phát triển phần mềm", và không phải là không có lý do.

Xác minh hình thức không phải là thần dược

Trong mật mã học và khoa học máy tính, có một truyền thống gần như cổ điển và cổ xưa như chính phương pháp hình thức: chỉ trích phương pháp hình thức, hoặc nói rộng ra hơn, chỉ trích sự phụ thuộc vào "chứng minh". Có rất nhiều ví dụ thực tiễn trong văn kiện liên quan. Hãy bắt đầu từ những bằng chứng viết tay đơn giản hơn ở giai đoạn đầu của mật mã học. Menezes và Koblitz đã từng chỉ trích những cái đó vào năm 2004:

Năm 1979, Rabin đề xuất một hàm mã hóa được coi là an toàn 「có thể chứng minh」 theo một cách nào đó, có nghĩa là nó có tính bảo mật dựa trên việc rút gọn.

Khẳng định bảo mật dựa trên việc rút gọn đó là: bất kỳ ai có thể tìm ra tin nhắn m từ văn bản mã hóa y cũng phải có khả năng phân tích n.

Ngay sau khi Rabin đưa ra thuật toán mã hóa của mình, Rivest chỉ ra rằng, một cách trớ trêu, chính đặc điểm mang lại sự bảo mật bổ sung cho nó cũng sẽ khiến hệ thống sụp đổ hoàn toàn trước một loại tấn công khác. Loại tấn công này được gọi là tấn công 「chọn văn bản mã hóa」. Cụ thể, giả sử kẻ tấn công có thể dẫn dụ Alice giải mã một phần văn bản mã hóa do chính kẻ tấn công chọn lựa. Khi đó, kẻ tấn công có thể sử dụng quy trình tương tự như Sam đã sử dụng trong đoạn trước để phân tách n.

Sau đó, Menezes và Koblitz đã đưa ra một số ví dụ khác. Chúng cùng nhau tạo ra một mẫu: thiết kế giao thức mật mã dựa trên 「dễ chứng minh hơn」 thường khiến giao thức trở nên không còn 「tự nhiên」 nữa, và dễ dàng gặp sự sụp đổ trong các tình huống mà người thiết kế hoàn toàn không cân nhắc đến.

Bây giờ, chúng ta quay lại với bằng chứng trên máy và mã nguồn. Dưới đây là ví dụ từ một bài báo vào năm 2011, tác giả phát hiện một lỗi trong trình biên dịch C đã được kiểm chứng hình thức:

Chúng tôi đã phát hiện ra vấn đề thứ hai trong CompCert, phản ánh qua hai lỗi. Hai lỗi này sẽ tạo ra đoạn mã như sau: stwu r1, -44432(r1)

Ở đây, một khung ngăn xếp PowerPC rất lớn đang được phân bổ. Vấn đề xảy ra khi trường dịch chuyển 16 bit đã tràn. Hình thức PPC của CompCert không xác định ràng buộc trên giá trị của số ngay tức ấy, bởi vì nó giả định trình biên dịch sẽ bắt giữ giá trị vượt quá phạm vi.

Xem xét một bài báo khác vào năm 2022:

Trong CompCert-KVX, commit e2618b31 đã sửa một lỗi: lệnh 「nand」 sẽ bị in ra là 「and」; và 「nand」 chỉ được chọn trong trường hợp hiếm hoi ~(a & b). Lỗi này được phát hiện thông qua việc biên dịch chương trình ngẫu nhiên.

Đến năm nay, cụ thể là năm 2026, Nadim Kobeissi khi mô tả lỗ hổng trong phần mềm kiểm chứng hình thức Cryspen viết rằng:

Vào tháng 11 năm 2025, Filippo Valsorda báo cáo độc lập rằng, libcrux-ml-dsa phiên bản 0.0.3 sẽ tạo ra khóa công khai và chữ ký khác nhau trên các nền tảng khác nhau khi có cùng đầu vào xác định. Lỗi này nằm trong bao gói hàm xây dựng _vxarq_u64, bao gồm thao tác XAR được sử dụng trong thay thế Keccak-f của SHA-3. Đường dự phòng đưa tham số sai vào thao tác dịch chuyển, làm hỏng băm SHA-3 trên nền tảng ARM64 không hỗ trợ phần cứng SHA-3, Đây là một lỗi loại I: hàm xây dựng nội bộ được đánh dấu đã kiểm chứng, trong khi toàn bộ sau lưng NEON không hoàn thành chứng chỉ an toàn hoặc tính đúng đắn tại thời điểm chạy.

还有：

libcrux-psq crate đã triển khai một giao thức sau lượng tử trước chia sẻ khóa. Trong phương thức decrypt_out, đường dẫn giải mã AES-GCM 128 sẽ gọi .unwrap() trên kết quả giải mã thay vì chuyển tiếp lỗi. Một văn bản mã hóa bất thường có thể làm cho tiến trình bị treo.

Bốn vấn đề trên có thể được phân loại thành hai loại:

Loại thứ nhất là chỉ có một phần mã đã được xác minh vì quá khó xác minh phần còn lại; và kết quả chứng minh rằng mã chưa được xác minh có bug dễ bị phát hiện hơn so với tác giả tưởng tượng và những bug này thường quan trọng hơn.

Loại thứ hai là tác giả quên chỉ định rõ một thuộc tính quan trọng nào đó mà thuộc tính này nguyên được giải thích.

Article của Nadim phân loại các mô hình thất bại của việc xác minh hình thức; anh ấy cũng liệt kê các loại thất bại khác. Ví dụ, một loại chính khác là: quy định hình thức chính nó là sai hoặc chứa các tuyên bố sai, nhưng hệ thống đã chấp nhận một cách im lặng.

Cuối cùng, chúng ta cũng có thể xem xét về việc xác minh hình thức thất bại xảy ra ở ranh giới phần cứng và phần mềm. Một vấn đề phổ biến ở đây là xem hệ thống xác minh có thể chống lại cuộc tấn công kênh phụ. Ngay cả khi bạn bảo vệ tin nhắn bằng một phương pháp mã hóa lý lẽ an toàn hoàn toàn, nhưng nếu một người ở xa vài mét có thể bắt được các biến động điện và rút ra khóa riêng của bạn sau hàng trăm nghìn lần mã hóa, thì bạn vẫn không an toàn.

"Phân tích năng lượng khác biệt" (differential power analysis) chính là một ví dụ trong loại hình công nghệ này mà ngày nay đã được hiểu rõ.

Phân tích năng lượng khác biệt là một hình thức tấn công kênh phụ phổ biến. Nguồn: Wikipedia

Trước đây đã có người cố gắng chứng minh rằng hệ thống có thể chống lại loại tấn công này. Tuy nhiên, bất kỳ chứng minh nào cũng cần một loại mô hình toán học về kẻ tấn công, và sau đó bạn mới có thể chứng minh tính bảo mật trong mô hình đó. Đôi khi, mọi người sử dụng "mô hình d-probing": nghĩa là giả định rằng có một giới hạn trên số điểm mà kẻ tấn công có thể quét trong mạch. Nhưng vấn đề là, một số dạng rò rỉ không thể bị mô hình này bắt.

Một vấn đề phổ biến được quan sát trong bài viết này là rò rỉ chuyển đổi (transitional leakage): nếu tín hiệu bạn quan sát không phải phụ thuộc vào giá trị cụ thể tại một vị trí mà phụ thuộc vào sự thay đổi của giá trị đó, thì nhiều lúc, bạn có thể khôi phục thông tin mong muốn từ hai giá trị - giá trị cũ và giá trị mới - không chỉ dựa vào một giá trị. Bài viết cũng phân loại các dạng rò rỉ khác.

Suốt hàng thập kỷ, những chỉ trích về xác minh hình thức này đã giúp cải thiện xác minh hình thức. So với quá khứ, chúng ta đã trở nên tinh ý hơn đối với các vấn đề như vậy. Tuy nhiên, ngay cả đến ngày nay, nó vẫn chưa hoàn hảo.

Nếu nhìn xa hơn, thực ra có một chung mạch nha tại đây: xác minh hình thức rất mạnh mẽ. Nhưng bất kể thị trường đánh giá nó như thế nào với việc đem lại "sự chính xác có thể chứng minh", thì sự "chính xác có thể chứng minh" đó ở bản chất không thể chứng minh được phần mềm, hoặc phần cứng, ở mức độ "chính xác" thực sự.

Với phần lớn mọi người, "chính xác" đại khái có nghĩa là: hành vi của thứ đó phù hợp với sự hiểu biết mà người dùng có về ý đồ của nhà phát triển.

Và "an toàn" đại khái có nghĩa là: hành vi của thứ đó sẽ không điều chỉnh ra khỏi kỳ vọng của người dùng một cách có hại đến lợi ích của họ.

Trong cả hai trường hợp, tính chính xác và tính an toàn cuối cùng đều quay về một loại so sánh: một bên là một đối tượng toán học, bên kia là ý định hoặc kỳ vọng của con người. Nói một cách nghiêm ngặt, ý định và kỳ vọng của con người chính là các đối tượng toán học - cuối cùng, não người cũng là một phần của vũ trụ, và vũ trụ tuân theo luật lý học; nếu bạn có sức mạnh tính toán đủ lớn, lý thuyết thì bạn có thể mô phỏng chúng. Nhưng chúng là những đối tượng toán học rất phức tạp, không có máy tính hoặc chính chúng ta, thậm chí không thể hiểu rõ, và thậm chí không thể đọc được. Vì mục đích thực tế, chúng ta có thể coi chúng như hộp đen. Lý do mà ta vẫn có thể hiểu về ý định và kỳ vọng của mình một cách nào đó, chỉ đơn giản vì mỗi người đều có nhiều năm kinh nghiệm quan sát ý tưởng của chính mình và suy luận về ý tưởng của người khác.

Và chính bởi vì chúng ta không thể đưa ý định ban đầu của con người vào máy tính trực tiếp, xác minh hình thức không thể chứng minh được sự so sánh giữa một hệ thống và ý định của con người. Do đó, "sự chính xác có thể chứng minh" và "sự an toàn có thể chứng minh" thực tế không chứng minh được "chính xác" và "an toàn" mà con người hiểu - cho đến khi chúng ta có thể mô phỏng não người. Trước khi đó, không có cách nào thực sự làm được điều này.

Vậy, điểm mạnh thực sự của xác minh hình thức là gì?

Tôi thiên về việc xem bộ thử nghiệm, hệ thống kiểu và xác minh hình thức như là các hình thức khác nhau của một phương pháp an toàn lập trình cơ bản - điều này có lẽ cũng là cách duy nhất có lý thuyết. Điểm chung của chúng nằm ở việc: họ mô tả ý định của chúng ta theo cách khác nhau, sau đó tự động kiểm tra xem những mô tả khác nhau đó có tương thích với nhau hay không.

Ví dụ, hãy xem đoạn mã Python dưới đây:

Ở đây, bạn đã sử dụng ba cách khác nhau để diễn đạt ý định của mình:

Thứ nhất, diễn đạt trực tiếp: thông qua mã lập trình triển khai công thức Fibonacci.

Thứ hai, Thể hiện gián tiếp: Bằng cách sử dụng hệ thống loại hình, thể hiện rằng cả đầu vào, đầu ra và các bước trung gian trong quá trình đệ quy là số nguyên.

Thứ ba, Sử dụng phương pháp "Bộ Kiểm Tra": Đây cũng chính là bộ kiểm tra.

Khi chạy tệp này, hệ thống sẽ sử dụng các ví dụ này để kiểm tra xem công thức có đúng không. Bộ kiểm tra loại hình sau đó có thể xác minh tính tương thích giữa các loại hình: Thực hiện phép cộng hai số nguyên là một phép toán hợp lệ và sẽ cho ra một số nguyên khác. Hệ thống loại hình cũng thường hữu ích trong tính toán vật lý: Nếu bạn đang tính gia tốc, nhưng kết quả bạn nhận được có đơn vị là m/s thay vì m/s², thì bạn biết mình đã tính sai ở đâu. Và định nghĩa "bộ kiểm tra" dạng này, bộ kiểm tra là một loại của nó, thường cũng phản ánh cách tiếp cận của con người với khái niệm hơn là định nghĩa trực tiếp, rõ ràng.

Bạn có thể sử dụng càng nhiều cách để thể hiện ý định của mình càng tốt; lý tưởng nhất, những cách này nên khác biệt đủ lớn, buộc bạn phải sử dụng các cách suy nghĩ khác nhau để giải quyết cùng một vấn đề. Với cách này, nếu tất cả các cách thể hiện cuối cùng đều tương thích với nhau, thì khả năng bạn thật sự thể hiện đúng nội dung bạn muốn thể hiện cũng cao hơn.

Điểm cốt lõi của việc lập trình an toàn chính là thể hiện ý định của bạn theo nhiều cách khác nhau, sau đó tự động xác minh xem những thể hiện này có tương thích với nhau hay không.

Chứng minh hóa hình thức có thể đẩy mạnh phương pháp này thêm nữa. Thông qua chứng minh hóa hình thức, bạn gần như có thể sử dụng bất kỳ cách thể hiện nào để mô tả ý định của mình; chỉ khi những mô tả này tương thích với nhau, chương trình mới vượt qua được việc xác minh.

Bạn có thể viết cùng một lúc một cài đặt được tối ưu hóa và một cài đặt hiệu suất thấp nhưng dễ đọc cho con người, sau đó xác minh xem cả hai có nhất quán không. Bạn cũng có thể yêu cầu mười người bạn mỗi người viết ra những thuộc tính toán học mà họ nghĩ rằng chương trình này nên đáp ứng, sau đó kiểm tra xem chương trình có đáp ứng tất cả chưa; nếu không, thì tiến hành xem xét kỹ càng xem là do chương trình có vấn đề hay do tính chất toán học đó có vấn đề. Và Trí tuệ Nhân tạo có thể giúp cải thiện tất cả công việc trên một cách hiệu quả tột độ.

Vậy tôi nên bắt đầu như thế nào?

Trong thực tế, bạn hầu như không thể tự mình viết bản chứng minh. Lý do nguyên cơ của phương pháp hình thức vẫn chưa phổ cập thật sự đến người này hoàn toàn nằm ở: Đa số mọi người khó hiểu đến mức nào nên viết những bản chứng minh đáng mắt như thế nào.

Bạn có thể nói cho tôi biết đoạn mã dưới đây có ý nghĩa gì không?

(Nếu bạn muốn biết, nó là một trong nhiều bổ đề con trong một bản chứng minh nào đó. Bản chứng minh đó nhằm vào một tuyên bố an toàn cụ thể của một biến thể chữ ký SPHINCS: Nghĩa là, trừ khi xảy ra va chạm băm, thì so với bất kỳ chữ ký nào khác của một tin nhắn khác, việc tạo ra một chữ ký cho một tin nhắn nào đó phải sử dụng một giá trị vị trí cao hơn trên một chuỗi băm cụ thể. Do đó, thông tin cần thiết cho việc này không thể được tính toán từ một chữ ký khác.)

Bạn không cần phải viết mã và chứng minh, mà hãy để trí tuệ nhân tạo giúp bạn viết chương trình — bạn có thể viết trực tiếp bằng Lean; nếu bạn muốn tốc độ, bạn cũng có thể viết bằng ngôn ngữ hợp ngữ — và trong quá trình đó chứng minh các thuộc tính mà bạn muốn.

Một lợi ích của nhiệm vụ này là nó về cơ bản là tự xác minh, vì vậy bạn không cần phải luôn nhìn vào nó. Bạn hoàn toàn có thể để trí tuệ nhân tạo hoạt động liên tục trong vài giờ. Trường hợp tồi nhất, nhưng không nhiều hơn, là nó quay vòng tại chỗ, không thể tiến triển; hoặc như một lần Leanstral của tôi đã từng làm, để làm cho công việc của mình dễ dàng hơn, đơn giản thay thế câu tuyên bố mà nó được yêu cầu chứng minh.

Điều bạn cuối cùng cần kiểm tra là: câu tuyên bố mà nó chứng minh, liệu thực sự có phải là điều bạn muốn chứng minh không.

Trong biến thể chữ ký SPHINCS này, tuyên bố cuối cùng như sau:

Thực tế, điều này đã gần như đạt tới ranh giới có thể "đọc được":

Nếu một con số được tạo ra từ băm (dig1) không bằng với một con số được tạo ra từ băm khác (dig2), thì nhận định sau không đúng:

Đối với tất cả các số, mỗi chữ số của dig1 nhỏ hơn hoặc bằng chữ số tương ứng của dig2;

Đối với tất cả các số, mỗi chữ số của dig2 nhỏ hơn hoặc bằng chữ số tương ứng của dig1.

Ở đây, chúng ta so sánh "con số mở rộng" (wotsFullDigits) được tạo ra thông qua việc thêm checksum. Nghĩa là, không thể tránh khỏi, ở một số vị trí, con số mở rộng của dig1 sẽ cao hơn; và ở một số vị trí khác, con số mở rộng của dig2 sẽ cao hơn.

Trong việc viết chứng minh bằng mô hình ngôn ngữ lớn, tôi thấy rằng Claude đã đủ tốt, DeepSeek 4 Pro cũng đủ để thực hiện. Leanstral là một lựa chọn tiềm năng: đó là một mô hình dự chỉ cỡ nhỏ, trọng số mã nguồn mở, được điều chỉnh đặc biệt để viết mỹ thuật Lean. Nó có 1190 tỷ tham số, nhưng mỗi mã thông báo chỉ kích hoạt 60 tỷ tham số, vì vậy nó có thể chạy cục bộ, mặc dù tốc độ sẽ chậm hơn — trên laptop của tôi, khoảng 15 token mỗi giây.

Theo các bài kiểm tra chuẩn, Leanstral đã vượt qua nhiều mô hình chung lớn hơn nhiều:

Theo trải nghiệm cá nhân của tôi hiện tại, nó hơi yếu hơn DeepSeek 4 Pro, nhưng vẫn hiệu quả.

Xác minh hình thức không giải quyết tất cả vấn đề của chúng ta. Nhưng nếu chúng ta muốn xây dựng một mô hình an ninh Internet thay vì để mọi người tin tưởng vào một số tổ chức mạnh mẽ, chúng ta cần có khả năng tin tưởng vào mã nguồn — kể cả khi đối mặt với một đối thủ AI mạnh mẽ. Xác minh hình thức với sự hỗ trợ của AI có thể là bước tiến quan trọng hướng tới mục tiêu này.

Tương tự như blockchain và ZK-SNARKs, AI và xác minh hình thức cũng là những công nghệ hoàn complementarity.

Blockchain mang đến tính bảo vệ quyền riêng tư và khả năng mở rộng với một mức giá; đồng thời, ZK-SNARKs đưa quyền riêng tư và khả năng mở rộng trở lại — thực tế, thậm chí mạnh mẽ hơn so với trước đây.

AI giúp bạn có thể viết mã nguồn quy mô lớn, nhưng với một mức giá là sự giảm độ chính xác; và xác minh hình thức đưa độ chính xác trở lại — thực tế, còn mạnh mẽ hơn cả trước đây.

Mặc định, AI sẽ tạo ra một lượng lớn mã nguồn rất tệ; số lượng lỗi cũng sẽ tăng lên. Thực tế, ở một số tình huống, việc tăng số lỗi may mắn là sự cân nhắc đúng đắn: nếu tác động của những lỗi này nhẹ nhàng, thì phần mềm có lỗi cũng còn hơn là không có phần mềm như vậy. Nhưng ở đây, an ninh mạng vẫn có một tương lai lạc quan: phần mềm sẽ tiếp tục tiến triển thành các thành phần "lõi an ninh" xoành quanh "các thành phần mép không an toàn".

Các thành phần mép không an toàn này sẽ chạy trong một hộp cát và chỉ được cấp quyền nhỏ nhất cần thiết để hoàn thành nhiệm vụ của chúng. "Lõi an ninh" sau đó sẽ chịu trách nhiệm quản lý tất cả. Nếu "lõi an ninh" gặp sự cố, mọi thứ sẽ gặp vấn đề — dữ liệu cá nhân của bạn, tiền của bạn, và nhiều hơn thế nữa sẽ bị ảnh hưởng. Nhưng nếu một "cạnh bị thâm nhập" nào đó gặp vấn đề, "lõi an ninh" vẫn có thể bảo vệ bạn.

Khi đề cập đến "lõi an ninh", chúng tôi sẽ không để mã có lỗi lầm lan một cách liên tục. Chúng tôi sẽ tích cực kiểm soát quy mô của "lõi an ninh", giữ cho nó đủ nhỏ và thậm chí coi đó là mục tiêu thu hẹp hơn nữa. Ngược lại, chúng tôi sẽ đầu tư hoàn toàn vào việc cải thiện tổng thể của "lõi an ninh" bằng tất cả khả năng bổ sung mà AI mang lại, để nó có thể chịu trách nhiệm cho gánh nặng tin cậy cực kỳ cao trong xã hội số cao cấp.

Nhân viên hạt nhân của hệ điều hành của bạn, hoặc ít nhất một phần của nó, sẽ là một trong những "lõi an ninh" như vậy. Ethereum sẽ là một cái khác. Trong điều kiện lý tưởng, ít nhất trong tất cả các tính toán không phải hiệu suất cao, phần cứng bạn sử dụng cũng sẽ trở thành một "lõi an ninh" thứ ba. Một số hệ thống liên quan đến Internet of Things sẽ là lõi an ninh thứ tư.

Ít nhất trong những lõi an ninh này, câu nói cũ "lỗi không thể tránh được, bạn chỉ có thể cố gắng tìm ra chúng trước kẻ tấn công" sẽ không còn đúng nữa. Nó sẽ được thay thế bằng một thế giới có hy vọng hơn: nơi chúng ta có thể đạt được sự an toàn thực sự.

Dĩ nhiên, nếu bạn muốn giao phó tài sản và dữ liệu của mình cho những phần mềm viết rất tệ, thậm chí có thể vô tình đẩy chúng vào hố đen hoàn toàn, thì bạn vẫn sẽ có tự do đó.

[Liên kết đến bài gốc]

Chào mừng bạn tham gia cộng đồng chính thức của BlockBeats:

Nhóm Telegram đăng ký: https://t.me/theblockbeats

Nhóm Telegram thảo luận: https://t.me/BlockBeats_App

Tài khoản Twitter chính thức: https://twitter.com/BlockBeatsAsia