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:Khi khả năng lập trình của AI phát triển nhanh chóng, 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, chứng minh ZK, thuật toán đồng thuận và hệ thống tài sản trên chuỗi xuất hiện lỗi, hậu quả thường không chỉ là lỗi phần mềm thông thường, mà là tổn thất tài chính không thể đảo ngược và sự sụp đổ niềm tin.
Điều mà Vitalik thảo luận trong bài viết này chính là một con đường khác cho an ninh mã nguồn trong thời đại AI: xác minh hình thức. Nói một cách đơn giản, thay vì dựa vào kiểm toán viên con người kiểm tra mã từng dòng, nó viết các tính chất mà chương trình phải thỏa mãn thành các mệnh đề toán học, sau đó sử dụng các chứng minh có thể kiểm tra bằng máy để xác minh xem các tính chất này có được đáp ứng hay không. Trước đây, do rào cản cao và quy trình phức tạp, xác minh hình thức luôn nằm trong lĩnh vực nghiên cứu và kỹ thuật tương đối nhỏ; nhưng khi AI có thể hỗ trợ viết mã và chứng minh, phương pháp này đang trở nên có ý nghĩa thực tế trở lại.
Đánh giá 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à "an ninh có thể chứng minh" không bằng an ninh tuyệt đối: chứng minh có thể bỏ sót giả định quan trọng, bản thân đặc tả có thể viết sai, mã không được xác minh, ranh giới phần cứng và tấn công kênh bên 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 ninh đáng tin cậy hơn: biểu đạt ý định của nhà phát triển bằng nhiều cách, sau đó để hệ thống tự động kiểm tra xem các biểu đạt đó có tương thích với nhau không.
Điều này đặc biệt quan trọng với Ethereum. Ethereum tương lai 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ý chố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 mục tiêu an ninh 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 các tình huống như vậy, xác minh hình thức hỗ trợ bởi 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à chứng minh, để 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 an ninh họ muốn hay không.
Từ góc độ vĩ mô hơn, bài viết này cũng là sự phản hồi của Vitalik về an ninh mạng trong thời đại AI. Đối mặt với các tác nhân 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 lại dựa vào một số tổ chức tập trung hóa, mà là nén các hệ thống quan trọng thành một "lõi an ninh" nhỏ hơn, có thể kiểm chứng hơn, đáng tin cậy hơn. AI sẽ làm tăng số lượng mã thô, 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.
Dưới đây là bài viết 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à xem xét 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 góc khác trong lĩnh vực tính toán: các nhà phát triển viết mã trực tiếp bằng các ngôn ngữ cấp thấp, chẳng hạn như bytecode EVM, ngôn ngữ assembly, hoặc sử dụng Lean để viết mã, và xác minh tính chính xác của nó bằng cách viết các chứng minh toán học có thể tự động kiểm tra trong Lean.
Nếu được áp dụng đúng cách, phương pháp này vừa có thể 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ách phát triển phần mềm trước đây. Yoichi Hirai gọi đây 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 của phần mềm thực sự có thể làm được gì, và những hạn chế và ranh giới của nó ở đâu—cho dù trong bối cảnh Ethereum hay trong lĩnh vực phát triển phần mềm rộng hơn.
Xác minh hình thức là gì?
Xác minh hình thức là việc viết chứng minh cho các định lý toán học theo cách có thể được máy 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 một định lý cơ bản về dãy 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, tiến ba số mỗi lần.
Đầu tiên xét trường hợp cơ sở. Đặt F1 = F2 = 1, F3 = 2. 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ẻ"—là đúng trước x = 3.
Tiếp theo là bước quy nạp. Giả sử mệnh đề đúng đến 3k+3, tức 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ừ "biết mệnh đề đú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 lập luận này, chúng ta có thể tin chắc rằng quy luật này đúng với mọi số nguyên.
Lập luận này đối với con người là có sức thuyết phục. Nhưng nếu bạn muốn chứng minh một thứ phức tạp hơn một trăm lần, và bạn thực sự muốn xác nhận mình không mắc sai lầm thì sao? Lúc này, bạn có thể xây dựng một chứng minh mà máy tính cũng có thể tin.
Nó sẽ trông đại khái như thế này:
Đây là cùng một lập luận, nhưng được biểu đạ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 chứng minh toán học.
Nó trông rất khác so với chứng minh "phiên bản con người" tôi đưa ra ở trên, và có lý do chính đáng: những gì trực quan đối với máy tính khác hoàn toàn với những gì trực quan đối với con người. Ở đây, máy tính được nói đến là "máy tính" theo nghĩa cũ—chương trình "xác định" cấu thành từ các câu lệnh if/then, không phải mô hình ngôn ngữ lớn.
Trong chứng minh trên, bạn không nhấn mạnh thực tế 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 mang tên khá hoành tráng omega trong Lean, sẽ tự động kết hợp điều này với hiểu biết của nó về định nghĩa của fib(3k+4).
Trong các chứng minh phức tạp hơn, đôi khi bạn phải chỉ rõ từng bước: chính xác định luật toán học nào cho phép bạn thực hiện bước này, và những định luật này đôi khi còn mang những cái tên khó hiểu, chẳng hạn như Prod.mk.inj. Mặt khác, bạn cũng có thể khai triển một 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 là có thể hoàn thành lập luận.
Sự không trực quan và phiền phức ở đây chính là lý do quan trọng khiến chứng minh có thể kiểm chứng bằng máy mặc dù đã tồn tại gần 60 năm, nhưng vẫn luôn nằm trong 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ờ tiến bộ nhanh chóng của AI.
Xác minh chương trình máy tính
Đến đây, bạn có thể nghĩ: OK, vậy chúng ta có thể để máy tính xác minh chứng minh của các định lý toán học, vậy cuối cùng chúng ta có thể xác định những phát hiện mới điên rồ về số nguyên tố, cái nào là thật, cái nào chỉ là sai sót ẩn trong các bài báo PDF dài hàng trăm trang. Có lẽ chúng ta thậm chí còn có thể tìm ra xem chứng minh của Shinichi Mochizuki về phỏng đoán ABC có chính xác hay không! Nhưng ngoài việc thỏa mãn sự tò mò, việc 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 chính xác của 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 an ninh. 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 đó, việc chứng minh một chương trình máy tính sẽ chạy theo một cách nào đó, 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 phần mềm truyền thông mã hóa như Signal có thực sự an toàn hay không. Đầu tiên, bạn có thể viết rõ ràng bằng toán học, trong ngữ cảnh này, "an toàn" thực sự có nghĩa là gì. Nói tóm lại, bạn cần chứng minh rằng: với giả định mật mã nào đó được thiết lập, chỉ những người có 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. Trong thực tế, tất nhiên có nhiều loại thuộc tính an ninh thực sự quan trọng.
Và sự thật là, đã có một nhóm đang cố gắng tìm hiểu điều này. Một trong các định lý an ninh mà họ đề xuất, trông đại khái như thế này:
Dưới đây là 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 phép quy giản chặt chẽ, cho thấy trong mô hình tiên tri ngẫu nhiên, tính bảo mật thụ động của tin nhắn X3DH ít nhất cũng khó 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ảo mật thụ động của tin nhắn X3DH, thì họ cũng có thể phá vỡ DDH. Vì DDH thường được coi là một vấ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ể quan sát thụ động các tin nhắn trao đổi khóa của Signal, thì họ không thể phân biệt khóa phiên cuối cùng được tạo với một khóa ngẫu nhiên với xác suất vượt quá mức có thể bỏ qua.
Nếu kết hợp với một 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 chứng minh: cơ chế mã hóa của giao thức Signal có thể chống lại kẻ tấn công thụ động.
Các dự án xác minh tương tự cũng đã tồn tại, chúng được sử dụng để chứng minh tính an toàn của TLS và các thành phần mật mã khác trong trình duyệt.
Nếu bạn có thể thực hiện xác minh hình thức từ đầu đến cuối, thì bạn chứng minh không chỉ mô tả giao thức nào đó an toàn về mặt lý thuyết, mà cả đoạn mã cụ thể mà người dùng thực sự chạy trong thực tế cũng an toàn. Từ góc độ người dùng, điều này sẽ nâng cao đáng kể mức độ "không cần tin tưởng": để hoàn toàn tin tưởng vào đoạn mã này, bạn không cần phải kiểm tra toàn bộ codebase từng dòng, chỉ cần kiểm tra các phát biểu đã được chứng minh là đúng.
Tất nhiên, có một số dấu sao rất quan trọng cần lưu ý, đặc biệt là về từ khóa "an toàn" thực sự có nghĩa là gì. Mọi người rất dễ quên chứng minh những tuyên bố thực sự quan trọng; cũng rất dễ gặp phải tình huống: tuyên bố cần được chứng minh, không tồn tại mô tả ngắn gọn hơn chính mã nguồn; cũng rất dễ lén đưa vào chứng minh một số giả định cuối cùng không thành lập. Bạn cũng dễ dàng phán đoán rằng, chỉ một phần của hệ thống thực sự cần chứng minh hình thức, nhưng cuối cùng lại bị một lỗ hổng quan trọng trong các phần khác, thậm chí ở cấp độ phần cứng. Ngay cả bản thân việc triển khai Lean cũng có thể có lỗi. Nhưng trước khi thảo luận về những chi tiết đau đầu này, chúng ta hãy xem xét thêm: nếu xác minh hình thức có thể được hoàn thành một cách lý tưởng và chính xác, nó có thể mang lại một viễn cảnh gần như không tưởng như thế nào.
Xác minh hình thức hướng tới an ninh
Bug trong mã máy tính, vốn đã đáng lo ngại.
Khi bạn đưa tiền mã hóa vào hợp đồng thông minh trên chuỗi bất biến, bug mã nguồn sẽ trở nên đáng sợ hơn. Bởi vì một khi mã bị lỗi, tin tặc Triều Tiên có thể tự động chuyển toàn bộ tiền của bạn đi, và bạn hầu như không có biện pháp truy đòi nào.
Khi tất cả điều này lại được bọc trong chứng minh không kiến thức, bug mã nguồn sẽ trở nên đáng sợ hơn. Bởi vì nếu ai đó thành công tấn công hệ thống chứng minh không kiến thức, họ có thể rút toàn bộ tiền, và chúng ta có thể hoàn toàn không biết vấn đề ở đâu—thậm chí tệ hơn, chúng ta có thể hoàn toàn không biết vấn đề đã xảy ra.
Khi chúng ta có các mô hình AI mạnh mẽ, bug mã nguồn sẽ càng trở nên đáng sợ hơn. Ví dụ như mô hình Claude Mythos, sau hai năm cải tiến, có thể đã có thể tự động hóa việc phát hiện những lỗ hổng này.
Một số người đối mặt với thực tế này, bắt đầu chủ trương từ bỏ ý tưởng cơ bản về hợp đồng thông minh, thậm chí cho rằng không gian mạng không thể trở thành lĩnh vực mà bên phòng thủ có lợi thế phi đối xứng 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 nhiều token hơn kẻ tấn công để phát hiện lỗ hổng.
Và:
Ngành của chúng ta được xây dựng xung quanh mã xác định. Viết mã, kiểm tra, triển khai, và sau đó biết rằng nó chạy đúng—nhưng theo kinh nghiệm của tôi, thỏa thuận này đang thất bại. Trong số những người vận hành hàng đầu của các công ty bản địa AI thực sự, codebase đã bắt đầu trở thành thứ gì đó "bạn tin rằng nó chạy", và xác suất mà niềm tin này tương ứng, không thể được xác định chính xác nữa.
Tệ hơn nữa, một số người cho rằng, giải pháp duy nhất là từ bỏ mã nguồn mở.
Đối với an ninh mạng, đây sẽ là một tương lai ảm đạm. Đặc biệt đối với những người quan tâm đến phi tập trung và tự do internet, đây sẽ là một tương lai cực kỳ ảm đạm. Toàn bộ tinh thần Cypherpunk về bản chất đều xây dựng trên ý tưởng này: trên internet, bên phòng thủ có lợi thế. Xây dựng một "lâu đài" số—dù nó thể hiện dưới dạng mã hóa, chữ ký hay chứng minh—dễ dàng hơn nhiều so với việc phá hủy nó. Nếu chúng ta mất đi điều này, thì an ninh internet chỉ có thể đến từ kinh tế theo quy mô, từ việc truy bắt kẻ tấn công tiềm năng trên toàn cầu, nói rộng hơn, từ một lựa chọn: hoặc thống trị mọi thứ, hoặc đi đến hủy diệt.
Tôi không đồng ý với đánh giá này. Tôi có một tầm nhìn lạc quan hơn nhiều về tương lai của an ninh mạng.
Tôi cho rằng thách thức do khả năng phát hiện lỗ hổng AI mạnh mẽ mang lại thực sự nghiêm trọng, nhưng nó là một thách thức chuyển tiếp. Khi bụi lắng xuống và chúng ta bước vào trạng thái cân bằng mới, chúng ta sẽ đến một trạng thái thuận lợi hơn cho bên phòng thủ so với trước đây.
Mozilla cũng đồng ý với điều này. Trích dẫn lời của họ:
Bạn có thể cần sắp xếp lại thứ tự ưu tiên của tất cả các công việc khác, đầu tư một cách liên tục và tập trung vào nhiệm vụ này. Nhưng có ánh sáng ở cuối đường hầm. Chúng tôi rất tự hào khi thấy nhóm đã đứng lên đối mặt với thách thức này, những 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 ngoặt và bắt đầu nhìn thấy một tương lai tốt hơn, không chỉ là "theo kịp". Bên phòng thủ cuối cùng đã có cơ hội giành chiến thắng quyết định.
......
Số lượng lỗ hổng là có hạn, và chúng ta đang bước vào một thế giới cuối cùng có thể tìm ra tất cả chúng.
Bây giờ, nếu bạn sử dụng Ctrl+F trong bài viết này của Mozilla để tìm kiếm "formal" và "verification", bạn sẽ thấy cả hai từ đều không xuất hiện. 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 minh hình thức, cũng 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 cái gì? Về cơ bản, chính là biểu đồ 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ỗ hổng":
Hệ thống kiểu;
Ngôn ngữ an toàn bộ nhớ;
Cải tiến kiến trúc phần mềm, bao gồm sandbox, cơ chế quyền hạn, và tổng quát hơn là phân biệt rõ ràng giữa "cơ sở tính toán đáng tin cậy" và "mã khác";
Phương pháp kiểm tra tốt hơn;
Tích lũy kiến thức về mô hình mã hóa an toàn và không an toàn;
Ngày càng nhiều thư viện phần mềm được viết sẵn và kiểm toán.
Xác minh hình thứ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 coi như một bộ gia tốc mạnh mẽ: nó đang đẩy nhanh một xu hướng và mô hình vốn đã tiến về phía trước.
Xác minh hình thức không phải là thuốc chữa bách bệnh. Nhưng trong một số tình huống, nó đặc biệt phù hợp: chính là khi mục tiêu đơn giản hơn nhiều so với triển khai cụ thể. Điều này đặc biệt rõ ràng trong một số công nghệ khó nhất cần triển khai trong lần lặp lớn tiếp theo của Ethereum, chẳng hạn như chữ ký chống lượng tử, STARK, thuật toán đồng thuận và ZK-EVM.
STARK là một bộ phần mềm rất phức tạp. Nhưng thuộc tính an ninh cốt lõi mà nó thực hiện lại dễ hiểu và dễ hình thức hóa: nếu bạn thấy một bằng chứng, nó trỏ đến chương trình P, đầu vào x và đầu ra y của băm H, thì hoặc thuật toán băm mà STARK sử dụng bị phá vỡ, hoặc P(x) = y. Do đó, chúng ta có dự án Arklib, nó cố gắng tạo ra một triển khai STARK được xác minh hình thức hoàn chỉnh. Một dự án liên quan khác là VCV-io, nó cung cấp cơ sở hạ tầng tính toán oracle cơ bản, có thể được sử dụng để xác minh hình thức các giao thức mật mã khác nhau, nhiều giao thức trong số đó cũng là thành phần phụ thuộc của STARK.
Tham vọng hơn nữa là evm-asm: đây là một dự án cố gắng xây dựng triển khai EVM hoàn chỉnh và xác minh hình thức cho nó. Ở đây, thuộc tính an ninh không rõ ràng như vậy. Nói một cách đơ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; triển khai sau có thể theo đuổi tính trực quan và khả năng đọc cao nhất có thể, mà không cần xem xét hiệu suất chạy cụ thể.
Tất nhiên, về mặt lý thuyết vẫn có thể xảy ra tình huống: chúng ta có mười triển khai EVM, tất cả đều được chứng minh là tương đương với nhau, nhưng tất cả đều chia sẻ cùng một lỗi chết người, và lỗi này bằng cách nào đó cho phép kẻ tấn công chuyển toàn bộ ETH từ một địa chỉ mà họ không có quyền kiểm soát. Nhưng so với việc ngày nay một triển khai EVM riêng lẻ có lỗi như vậy, xác suất xảy ra tình huống này thấp hơn nhiều. Một thuộc tính an ninh quan trọng khác mà chúng ta chỉ thực sự nhận ra tầm quan trọng sau những kinh nghiệm đau đớn—khả năng chống DoS—tương đối dễ quy định rõ ràng.
Hai hướng quan trọng khác là:
Đồng thuận chịu lỗi Byzantine. Trong hướng này, việc định nghĩa hình thức tất cả các thuộc tính an ninh mong đợi cũng không dễ dàng. Nhưng xét rằng các lỗi liên quan vẫn rất phổ biến, việc thử xác minh hình thức vẫn đáng giá. Do đó, hiện đã có một số công việc đang tiến hành về triển khai đồng thuận Lean và chứng minh của nó.
Ngôn ngữ lập trình hợp đồng thông minh. Ví dụ liên quan bao gồm công việc xác minh 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 mà xác minh hình thức mang lại là: những chứng minh này thực sự từ đầu đến cuối. Nhiều lỗi khó khăn nhất thường là lỗi tương tác, chúng xuất hiện ở ranh giới giữa hai hệ thống con được xem xét riêng biệt. Đối với con người, việc lập luận toàn bộ hệ thống từ đầu đến cuối là quá khó khăn; nhưng hệ thống kiểm tra quy tắc tự động có thể làm được.
Xác minh hình thức hướng tới hiệu quả
Chúng ta hãy xem xét evm-asm. Đó là một triển khai EVM.
Nhưng nó là một triển khai EVM được viết trực tiếp bằng ngôn ngữ assembly RISC-V.
Thực sự theo nghĩa đen là assembly.
Dưới đây là opcode ADD:
Lý do chọn RISC-V là vì các trình chứng minh ZK-EVM hiện đang được xây dựng thường hoạt động bằng cách chứng minh RISC-V và biên dịch máy khách Ethereum sang RISC-V. Do đó, nếu bạn viết trực tiếp một triển khai EVM bằng RISC-V, về lý thuyết nó phải là triển khai nhanh nhất bạn có thể có. RISC-V cũng có thể được mô phỏng chạy rất hiệu quả trên máy tính thông thường, và máy tính xách tay RISC-V cũng đã tồn tại. Tất nhiên, để thực sự từ đầu đến cuối, bạn cũng phải xác minh hình thức cho chính việc triển khai RISC-V, hoặc biểu diễn số học của trình chứng minh. Nhưng đừng lo—loại công việc này cũng đã tồn tại.
Viết mã trực tiếp bằng assembly là việc chúng ta thường làm năm mươi năm trước. Kể từ đó, chúng ta dần chuyển sang viết mã bằng ngôn ngữ cấp cao. Ngôn ngữ cấp cao hy sinh một số hiệu quả, nhưng đổi lại, nó giúp viết mã nhanh hơn nhiều, quan trọng hơn, cũng giúp hiểu mã của người khác nhanh hơn nhiều—và đây là điều kiện cần thiết cho an ninh.
Với sự kết hợp của xác minh hình thức và AI, chúng ta có cơ hội "trở về tương lai". Cụ thể, để AI viết mã assembly, sau đó viết chứng minh hình thức, xác minh rằng mã assembly này có các thuộc tính chúng ta muốn. Ít nhất, mục tiêu thuộc tính này có thể chỉ là: nó hoàn toàn tương đương với một triển khai được tối ưu hóa cho khả năng đọc, được viết bằng một ngôn ngữ cấp cao thân thiện với con người.
Bằng cách này, không còn cần một đối tượng mã cân bằng giữa khả năng đọc và hiệu quả. Chúng ta sẽ có hai đối tượng tách biệt: một là triển khai assembly, chỉ được tối ưu hóa cho hiệu quả và điều chỉnh theo nhu cầu môi trường thực thi cụ thể; cái kia là tuyên bố an ninh, hoặc triển khai ngôn ngữ cấp cao, chỉ được tối ưu hóa cho khả năng đọc. Sau đó, chúng ta sử dụng một chứng minh toán học để chứng minh tính tương đương giữa hai bên. Người dùng có thể tự động xác minh chứng minh này một lần; sau đó, họ chỉ cần chạy phiên bản nhanh.
Điều này rất mạnh mẽ. Yoichi Hirai gọi đây là "hình thái cuối cùng của phát triển phần mềm", không phải không có lý do.
Xác minh hình thức không phải là thuốc chữa bách bệnh
Trong mật mã và khoa học máy tính, có một truyền thống gần cổ xưa như chính các phương pháp hình thức: chỉ trích các phương pháp hình thức, hoặc nói rộng hơn, chỉ trích sự phụ thuộc vào "chứng minh". Có rất nhiều trường hợp thực tiễn trong tài liệu liên quan. Hãy bắt đầu với những chứng minh viết tay đơn giản hơn trong giai đoạn đầu của mật mã. Menezes và Koblitz vào năm 2004 đã chỉ trích chúng như sau:
Năm 1979, Rabin đề xuất một hàm mã hóa, theo một nghĩa nào đó là "có thể chứng minh" an toàn, tức là nó có thuộc tính an ninh quy giản.
Tuyên bố an ninh quy giản là: bất kỳ ai có thể tìm ra tin nhắn m từ bản mã y, cũng phải có khả năng phân tích n.
Ngay sau khi Rabin đề xuất sơ đồ mã hóa của mình, Rivest chỉ ra rằng, mỉa mai thay, chính đặc điểm mang lại cho nó tính an ninh bổ sung, khi đối mặt với một loại kẻ tấn công khác, cũng sẽ dẫn đến sự sụp đổ hoàn toàn của hệ thống. Loại kẻ tấn công này được gọi là kẻ tấn công "lựa chọn bản mã". Cụ thể, giả sử kẻ tấn công có thể dụ dỗ Alice giải mã một bản mã do chính kẻ tấn công chọn. Sau đó, kẻ tấn công có thể phân tích n theo cùng quy trình mà Sam đã sử dụng trong đoạn trước.
Menezes và Koblitz sau đó đưa ra thêm một số ví dụ. Chúng cùng thể hiện một mô hình: việc thiết kế giao thức mật mã xoay quanh "dễ chứng minh hơn", thường làm cho giao thức trở nên kém "tự nhiên" hơn và dễ bị sụp đổ trong các tình huống mà nhà thiết kế hoàn toàn không xem xét.
Bây giờ, chúng ta hãy quay lại với chứng minh có thể kiểm chứng bằng máy và mã. Dưới đây là một ví dụ từ một bài báo năm 2011, tác giả đã tìm thấy lỗi trong trình biên dịch C đã được xác minh hình thức:
Vấn đề thứ hai chúng tôi phát hiện trong CompCert, thể hiện ở hai lỗi. Hai lỗi này tạo ra mã tương tự như sau: stwu r1, -44432(r1)
Ở đây đang phân bổ một khung ngăn xếp PowerPC lớn. Vấn đề là trường dịch chuyển 16 bit bị tràn. Ngữ nghĩa PPC của CompCert không quy định ràng buộc về chiều rộng giá trị ngay lập tức này, vì nó giả định rằng bộ hợp ngữ sẽ bắt được các giá trị vượt quá phạm vi.
Hãy xem một bài báo năm 2022:
Trong CompCert-KVX, commit e2618b31 đã sửa một lỗi: lệnh "nand" sẽ được in thành "and"; và "nand" chỉ được chọn trong chế độ ~(a & b) hiếm gặp. Lỗi này được phát hiện thông qua việc biên dịch các chương trình được tạo ngẫu nhiên.
Đến nay, năm 2026, Nadim Kobeissi khi mô tả các lỗ hổng trong phần mềm được xác minh hình thức tại Cryspen đã viết:
Vào tháng 11 năm 2025, Filippo Valsorda báo cáo độc lập rằng libcrux-ml-dsa v0.0.3 với cùng đầu vào xác định, 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. Lỗi này nằm trong wrapper hàm dựng _vxarq_u64, wrapper này thực hiện thao tác XAR được sử dụng trong phép hoán vị Keccak-f của SHA-3. Đường dẫn fallback truyền tham số sai cho thao tác dịch chuyển, dẫn đến việc tóm tắt SHA-3 bị hỏng trên các nền tảng ARM64 không hỗ trợ phần cứng SHA-3. Đây là một thất bại loại I: hàm dựng này được đánh dấu là đã xác minh, trong khi toàn bộ backend NEON không hoàn thành chứng minh tính an toàn hoặc tính chính xác tại thời gian chạy.
Và:
Libcrux-psq crate triển khai một giao thức khóa được chia sẻ trước hậu lượng tử. 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ì tiếp tục truyền lỗi. Một bản mã dị dạng có thể làm sập tiến trình.
Bốn vấn đề trên có thể được phân loại thành hai loại:
Loại thứ nhất, chỉ một phần mã được xác minh, vì xác minh phần còn lại quá khó; và kết quả chứng minh rằng, mã không được xác minh dễ bị lỗi hơn so với tác giả tưởng tượng, và những lỗi này thường quan trọng hơn.
Loại thứ hai, tác giả quên quy định rõ một thuộc tính quan trọng, và thuộc tính này vốn cần được chứng minh.
Bài viết của Nadim phân loại các chế độ thất bại của xác minh hình thức; ông 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à: bản đặc tả hình thức tự nó sai, hoặc chứng minh chứa tuyên bố sai, nhưng được hệ thống xây dựng chấp nhận im lặng.
Cuối cùng, chúng ta cũng có thể xem xét các thất bại xác minh hình thức xảy ra tại ranh giới giữa phần mềm và phần cứng. Một vấn đề phổ biến ở đây là hệ thống xác minh có thể chống lại các cuộc tấn công kênh bên. Ngay cả khi bạn bảo vệ tin nhắn bằng cách mã hóa hoàn toàn an toàn về mặt lý thuyết, nhưng nếu ai đó cách vài mét có thể bắt được biến động điện và trích xuất khóa riêng tư của bạn sau vài trăm nghìn lần mã hóa, thì bạn vẫn không an toàn.
"Phân tích công suất khác biệt" là một ví dụ về kỹ thuật như vậy đã được hiểu rõ ngày nay.
Phân tích công suất khác biệt là một cuộc tấn công kênh bên phổ biến. Nguồn:Wikipedia
Trước đây cũng đã có người thử chứng minh hệ thống có thể chống lại loại kẻ tấn công này. Tuy nhiên, bất kỳ chứng minh như vậy đều cần một số mô hình toán học về kẻ tấn công, sau đó bạn mới có thể chứng minh tính an toàn trong mô hình đó. Đôi khi, người ta sử dụng "mô hình d-probing": tức là giả định số lượng vị trí trong mạch mà kẻ tấn công có thể thăm dò có một giới hạn đã biết. Nhưng vấn đề là, một số hình thức rò rỉ không thể bị mô hình này bắt được.
Một vấn đề phổ biến được quan sát trong bài báo này, là rò rỉ chuyển tiếp: nếu tín hiệu bạn quan sát không 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ị này, thì nhiều khi bạn có thể khôi phục thông tin cần thiết từ hai giá trị—giá trị cũ và giá trị mới—thay vì chỉ dựa vào một giá trị. Bài báo cũng phân loại các hình thức rò rỉ khác.
Trong nhiều thập kỷ, những lời chỉ trích về xác minh hình thức này, ngược lại cũng giúp xác minh hình thức trở nên tốt hơn. So với trước đây, chúng ta hiện đã giỏi hơn trong việc cảnh giác với loại vấn đề này. Nhưng ngay cả đến ngày nay, nó vẫn chưa hoàn hảo.
Nếu nhìn từ góc độ rộng hơn, thực sự có một sợi chỉ chung: xác minh hình thức rất mạnh mẽ. Nhưng cho dù tiếp thị thị trường đóng gói nó như thế nào để mang lại "tính chính xác có thể chứng minh", cái gọi là "tính chính xác có thể chứng minh" về cơ bản không thể chứng minh phần mềm, hoặc phần cứng, là "chính xác" theo nghĩa thực sự.
Đối với hầu hết mọi người, "chính xác" đại khái có nghĩa là: thứ này hoạt động phù hợp với sự hiểu biết của người dùng về ý định của nhà phát triển.
Và "an toàn" đại khái có nghĩa là: thứ này hoạt động không đi chệch khỏi kỳ vọng của người dùng theo cách gây hại cho lợi ích của họ.
Trong cả hai trường hợp, tính chính xác và an toàn cuối cùng đều quy về một sự 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 bản thân cũng là đối tượng toán học—rốt cuộc, bộ não con người cũng là một phần của vũ trụ, và vũ trụ tuân theo các định luật vật lý; chỉ cần bạn có đủ sức mạnh tính toán, về lý thuyết có thể mô phỏng chúng. Nhưng chúng là những đối tượng toán học cực kỳ phức tạp, cả máy tính và chính chúng ta đều không thể thực sự hiểu, 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 chúng ta vẫn có một số hiểu biết về ý định và kỳ vọng của mình, chỉ vì mỗi người đều có nhiều năm kinh nghiệm quan sát suy nghĩ của bản thân và suy luận suy nghĩ của người khác.
Và cũng vì chúng ta không thể nhét trực tiếp ý định nguyên bản của con người vào máy tính, xác minh hình thức không có cách nào chứng minh sự so sánh giữa một hệ thống và ý định của con người. Do đó, "tính chính xác có thể chứng minh" và "tính an toàn có thể chứng minh" thực tế không chứng minh "tính chính xác" và "tính an toàn" mà con người hiểu—trước khi chúng ta có thể mô phỏng bộ não con người, không có phương pháp nào thực sự có thể làm được điều này.
Vậy, điểm hữu ích thực sự của xác minh hình thức là gì?
Tôi có xu hướng coi bộ kiểm thử, hệ thống kiểu và xác minh hình thức là các dạng triển khai khác nhau của cùng một phương pháp an ninh ngôn ngữ lập trình cơ bản—đây có lẽ cũng là phương pháp duy nhất thực sự có ý nghĩa. Điểm chung của chúng là: sử dụng nhiều cách khác nhau để mô tả dư thừa ý định của chúng ta, sau đó tự động kiểm tra xem các mô tả khác nhau này có tương thích với nhau không.
Ví dụ, hãy xem đoạn mã Python dưới đây:
Ở đây, bạn diễn đạt ý định của mình bằng ba cách khác nhau:
Thứ nhất, diễn đạt trực tiếp: thông qua triển khai mã công thức Fibonacci.
Thứ hai, diễn đạt gián tiếp: thông qua hệ thống kiểu để chỉ ra đầu vào, đầu ra và các bước trung gian trong quá trình đệ quy đều là số nguyên.
Thứ ba, sử dụng phương pháp "bộ trường hợp": chính là các trường hợp kiểm thử.
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 kiểu có thể xác minh các kiểu có tương thích không: cộng hai số nguyên là một thao tác hợp lệ và sẽ cho ra một số nguyên khác. Hệ thống kiểu 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 nhận được kết quả có đơn vị là m/s, thay vì m/s2, thì bạn biết mình đã tính sai ở đâu. Và các định nghĩa kiểu "bộ trường hợp", trường hợp kiểm thử là một trong số đó, thường phù hợp với cách con người xử lý khái niệm hơn so với định nghĩa trực tiếp, rõ ràng.
Bạn có thể diễn đạt ý định của mình bằng càng nhiều cách khác nhau càng tốt; lý tưởng nhất, các cách này nên đủ khác biệt để buộc bạn xử lý cùng một vấn đề bằng các cách suy nghĩ khác nhau. Bằng cách này, nếu tất cả các cách diễn đạt cuối cùng đều tương thích với nhau, thì xác suất bạn thực sự diễn đạt được nội dung mình muốn cũng cao hơn.
Cốt lõi của lập trình an toàn là diễn đạt ý định của bạn bằng nhiều cách khác nhau, sau đó tự động xác minh các diễn đạt này có tương thích với nhau không.
Xác minh hình thức có thể đẩy phương pháp này tiến xa hơn. Với xác minh hình thức, bạn gần như có thể mô tả ý định của mình bằng nhiều cách dư thừa tùy ý; chỉ khi các mô tả này tương thích với nhau, chương trình mới vượt qua xác minh.
Bạn có thể đồng thời viết một triển khai được tối ưu hóa và một triển khai kém hiệu quả nhưng dễ đọc đối với con người, sau đó xác minh hai bên có nhất quán không. Bạn cũng có thể mời mười người bạn liệt kê riêng các thuộc tính toán học mà họ cho rằng chương trình này nên thỏa mãn, sau đó kiểm tra xem chương trình có đáp ứng tất cả không; nếu không vượt qua, hãy xác định thêm xem chương trình sai hay chính thuộc tính toán học đó có vấn đề. Và AI có thể làm cho tất cả các công việc trên trở nên cực kỳ hiệu quả.
Vậy tôi nên bắt đầu như thế nào?
Thực tế mà nói, bạn có lẽ sẽ không tự viết chứng minh. Lý do cơ bản khiến các phương pháp hình thức chưa bao giờ thực sự phổ biến là: hầu hết mọi người khó hiểu làm thế nào để viết những chứng minh chết tiệt này.
Bạn có thể cho tôi biết đoạn mã dưới đây có nghĩa là gì không?
(Nếu bạn muốn biết, nó là một trong nhiều bổ đề phụ trong một chứng minh. Chứng minh này nhằm vào một tuyên bố an ninh cụ thể cho một biến thể nào đó của chữ ký SPHINCS: tức là, trừ khi xảy ra va chạm băm, việc tạo chữ ký cho một tin nhắn, so với chữ ký của bất kỳ tin nhắn nào khác, ít nhất cần sử dụng một giá trị ở vị trí cao hơn trên một chuỗi băm. Do đó, thông tin nó cần không thể tính toán được từ một chữ ký khác.)
Bạn không cần viết mã và chứng minh bằng tay, mà hãy để AI viết chương trình cho bạn—có thể viết trực tiếp bằng Lean; nếu bạn muốn tốc độ, cũng có thể viết bằng assembly—và trong quá trình này chứng minh các thuộc tính bạn muốn.
Một lợi ích của nhiệm vụ này là, về bản chất nó tự xác minh, vì vậy bạn không cần phải liên tục giám sát nó. Bạn hoàn toàn có thể để AI tự chạy liên tục trong vài giờ. Tình huống tệ nhất, chỉ là nó quay vòng tại chỗ, không đạt được tiến triển; hoặc như Leanstral của tôi đã từng làm một lần, để giảm bớt công việc cho mình, trực tiếp thay thế tuyên bố mà nó được yêu cầu chứng minh.
Cuối cùng, bạn cần kiểm tra: mệnh đề mà nó chứng minh, có thực sự là thứ bạn muốn chứng minh hay không.
Trong biến thể chữ ký SPHINCS này, tuyên bố cuối cùng như sau:
Điều này thực sự đã gần mép "có thể đọc":
Nếu một số được tạo bởi một bản tóm tắt băm (dig1), không bằng số được tạo bởi một bản tóm tắt băm khác (dig2), thì điều sau đây không đúng:
Đối với tất cả các số, mỗi chữ số của dig1 đều 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 đều nhỏ hơn hoặc bằng chữ số tương ứng của dig1.
Ở đây so sánh là "số mở rộng" (wotsFullDigits) được tạo ra bằng cách thêm tổng kiểm tra. Nghĩa là, không thể tránh khỏi, ở một số vị trí, số mở rộng của dig1 sẽ cao hơn; ở những vị trí khác, số mở rộng của dig2 sẽ cao hơn.
Về việc sử dụng mô hình ngôn ngữ lớn để viết chứng minh, tôi thấy Claude đã đủ tốt, DeepSeek 4 Pro cũng đủ khả năng. Leanstral là một lựa chọn thay thế đầy hứa hẹn: đó là một mô hình quy mô nhỏ hơn, trọng số mã nguồn mở, được tinh chỉnh đặc biệt cho việc viết Lean. Nó có 119 tỷ tham số, nhưng chỉ kích hoạt 6 tỷ tham số mỗi token, do đó có thể chạy cục bộ, mặc dù tốc độ sẽ chậm—trên máy tính xách tay của tôi, khoảng 15 token mỗi giây.
Theo các bài kiểm tra chuẩn, Leanstral thể hiện vượt trội so với nhiều mô hình tổng quát có quy mô lớn hơn:
Theo trải nghiệm cá nhân hiện tại của tôi, nó yếu hơn một chút so với DeepSeek 4 Pro, nhưng vẫn hiệu quả.
Xác minh hình thức sẽ 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 tổ chức mạnh mẽ, thì chúng ta cần có khả năng chuyển sang tin tưởng vào mã—bao gồm cả việc tin tưởng mã khi đối mặt với đối thủ AI mạnh. Xác minh hình thức hỗ trợ bởi AI, chính có thể cho phép chúng ta tiến một bước quan trọng theo hướng này.
Giống như blockchain và ZK-SNARK, AI và xác minh hình thức cũng là những công nghệ bổ sung cao độ.
Blockchain mang lại khả năng xác minh mở và khả năng chống kiểm duyệt với cái giá là quyền riêng tư và khả năng mở rộng; còn ZK-SNARK lại mang quyền riêng tư và khả năng mở rộng trở lại—thực tế, thậm chí còn mạnh hơn trước đây.
AI cho phép bạn viết mã trên quy mô lớn, nhưng với cái giá là độ chính xác giảm; còn xác minh hình thức lại mang độ chính xác trở lại—thực tế, cũng mạnh hơn trước đây.
Theo mặc định, AI sẽ tạo ra một lượng lớn mã rất thô, số lượng lỗi cũng sẽ tăng lên. Thực sự, trong một số tình huống, việc để lỗi tăng thậm chí là sự đánh đổi đúng đắn: nếu ảnh hưởng của những lỗi này nhẹ, thì ngay cả phần mềm có lỗi cũng tốt hơn là không có loại phần mềm nà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 phân hóa thành các "thành phần biên không an toàn" xung quanh "lõi an ninh".
Các thành phần biên không an toàn này sẽ chạy trong sandbox và chỉ được cấp quyền tối thiểu cần thiết để hoàn thành nhiệm vụ của chúng. Lõi an ninh chịu trách nhiệm quản lý mọi thứ. Nếu lõi an ninh sụp đổ, mọi thứ sẽ sụp đổ—dữ liệu cá nhân, tiền của bạn và nhiều thứ khác sẽ bị ảnh hưởng. Nhưng nếu một thành phần biên không an toàn gặp sự cố, lõi an ninh vẫn có thể bảo vệ bạn.
Khi liên quan đến lõi an ninh, chúng ta sẽ không để mã lỗi lan rộng không kiểm soát. Chúng ta sẽ tích cực kiểm soát quy mô của lõi an ninh, giữ cho nó đủ nhỏ, thậm chí thu nhỏ thêm. Ngược lại, chúng ta sẽ đầu tư toàn bộ năng lực bổ sung mà AI mang lại vào việc nâng cao tính an ninh của chính lõi an ninh, để nó có thể gánh vác gánh nặng tin cậy cực cao trong xã hội số hóa cao.
Nhân 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 lõi khác. Lý tưởng nhất, ít nhất trong tất cả các tính toán không đòi hỏi hiệu suất cao, phần cứng bạn sử dụng cũng sẽ trở thành lõi an ninh thứ ba. Một số hệ thống liên quan đến Internet vạn vật, sẽ là lõi thứ tư.
Ít nhất trong các lõi an ninh này, câu nói cũ—lỗi là không thể tránh khỏi, bạn chỉ có thể cố gắng phát hiện chúng trước kẻ tấn công—sẽ không còn đúng. Nó sẽ được thay thế bằng một thế giới đầy hứa hẹn hơn: nơi chúng ta có thể đạt được sự an toàn thực sự.
Tất nhiên, nếu bạn sẵn sàng giao tài sản và dữ liệu của mình cho những phần mềm được viết kém, thậm chí có thể vô tình đưa tất cả chúng vào hố đen, thì bạn vẫn sẽ có tự do đó.
Liên kết bài viết gốc
