Trail of Bits dùng AI tự động hóa kiểm thử bảo mật cho Miden zkVM

Các công ty bảo mật đã đăng tải vô số bài viết trên blog mô tả cách họ hướng các tác nhân (agent) của mình vào một cơ sở mã (codebase) và tìm ra hàng chục lỗi (chúng tôi cũng là một trong số đó). Tuy nhiên, các bài viết này thường tập trung vào việc đánh giá mã bằng tác nhân, vốn chỉ là một khía cạnh trong cách chúng tôi sử dụng AI để đánh giá bảo mật. Chúng tôi muốn đưa ra một góc nhìn khác: ngay cả trước khi quá trình đánh giá mã bắt đầu, các tác nhân hiện đã cho phép chúng tôi xây dựng các công cụ tùy chỉnh và các mô hình hình thức (formal models) giúp cải thiện chất lượng cũng như chiều sâu cho các đánh giá của mình.

Gần đây, chúng tôi đã đánh giá Miden VM, một máy ảo zero-knowledge mới với ngôn ngữ hợp ngữ (assembly) tùy chỉnh riêng và hầu như không có công cụ hỗ trợ cho nhà phát triển. Để chuẩn bị, chúng tôi đã dành sáu tháng để các tác nhân của mình xây dựng từ đầu một máy chủ LSP, một trình dịch ngược (decompiler), một công cụ phân tích tĩnh và một mô hình Lean của bộ thực thi máy ảo. Những công cụ này đã tìm ra các vấn đề bảo mật thực sự, chẳng hạn như một đầu vào do người chứng minh (prover) cung cấp mà không được xác thực, cho phép một người chứng minh độc hại giả mạo chữ ký Falcon và đánh cắp tiền từ các chủ tài khoản Miden. Ngoài ra, công việc với Lean đã tạo ra 95 chứng minh tính đúng đắn được máy kiểm tra, bao phủ một phần lớn thư viện cốt lõi của Miden.

Kiểm toán Miden zkVM

Vào cuối năm 2025, đội ngũ Miden đã tìm đến chúng tôi để nhờ đánh giá các phần trong máy ảo zero-knowledge của họ trước khi ra mắt. Một phần của cuộc đánh giá được giới hạn trong thư viện cốt lõi của Miden, nơi chứa một tập hợp nhỏ các nguyên hàm mật mã được viết bằng ngôn ngữ hợp ngữ tùy chỉnh có tên là Miden assembly (MASM). Điều này khiến chúng tôi thực sự hào hứng vì nó hoàn toàn phù hợp với chuyên môn của chúng tôi: một dự án đảm bảo cao cấp viết mã mật mã phức tạp bằng ngôn ngữ hợp ngữ tùy chỉnh cấp thấp mà chúng tôi chưa từng thấy trước đây. Đồng thời, nó cũng đặt ra một số thách thức độc đáo.

Đầu tiên, Miden VM triển khai kiến trúc máy ngăn xếp (stack-machine). Điều này có nghĩa là mỗi lệnh sẽ thao tác trên các giá trị được đọc từ ngăn xếp, và kết quả của lệnh đó sau đó được ghi ngược lại vào đỉnh ngăn xếp. Mặc dù về mặt khái niệm là đơn giản, nhưng điều này khiến mã viết bằng MASM trở nên khó đánh giá, vì các đầu vào và đầu ra của lệnh được đọc từ ngăn xếp và luôn ở dạng ẩn. Ngoài ra, vì Miden VM là một kiến trúc hoàn toàn mới, nên hầu như không có công cụ hỗ trợ nhà phát triển nào như hỗ trợ IDE, máy chủ Language Server Protocol (LSP) và các trình kiểm tra lỗi (linter).

Chúng tôi biết mình có sáu tháng để chuẩn bị cho việc đánh giá vì quá trình triển khai chưa hoàn thiện các tính năng, vì vậy chúng tôi tự hỏi: "Chúng ta có thể dành thời gian và token vào việc gì để đảm bảo cuộc đánh giá sẽ loại bỏ được nhiều lỗi nhất có thể trong cơ sở mã?"

Xây dựng tất cả các công cụ!

Vì MASM thiếu các công cụ hỗ trợ nhà phát triển, chúng tôi bắt đầu bằng việc tự hỏi mình muốn có những loại công cụ nào khi dự án bắt đầu. Chúng tôi thường sử dụng VS Code để đánh giá mã, và việc tô sáng cú pháp (syntax highlighting) cũng như điều hướng mã là rất cần thiết để đảm bảo khả năng đọc và theo dõi luồng dữ liệu trong toàn bộ cơ sở mã. Chúng tôi cần một máy chủ LSP và một tiện ích mở rộng VS Code tương ứng cho việc này, và chỉ trong vài ngày, chúng tôi đã để Claude xây dựng một nguyên mẫu hoạt động cung cấp hầu hết các chức năng chúng tôi muốn: các tính năng như tô sáng cú pháp, đi đến định nghĩa (goto definition), tìm tham chiếu mã và hiển thị docstring của thủ tục khi di chuột qua. Với các tính năng cơ bản này, chúng tôi cũng quyết định thêm các tính năng đặc thù của ngôn ngữ như hiển thị tài liệu hướng dẫn lệnh nội dòng và hiệu ứng ngăn xếp (stack effects) cho từng lệnh riêng lẻ.

Sau khi xây dựng xong máy chủ LSP, chúng tôi bắt đầu nghĩ về các cách khác để cung cấp thông tin ngữ nghĩa cấp cao nhằm hỗ trợ việc đánh giá thủ công và đánh giá dựa trên tác nhân. Chúng tôi nghĩ sẽ rất thú vị nếu có thể cung cấp khả năng dịch ngược trung thực cho các thủ tục MASM ngay trong giao diện người dùng của VS Code, giúp người đánh giá nhanh chóng hiểu được luồng điều khiển và luồng dữ liệu cấp cao của các thủ tục mà họ đang xem xét. Đối với MASM, đây là một vấn đề khó hơn vẻ ngoài của nó. Việc nâng cấp (lifting) và dịch ngược máy ngăn xếp là một vấn đề đã được nghiên cứu kỹ lưỡng, nhưng việc dịch ngược MASM viết tay vẫn rất khó khăn vì nhiều lý do.

Hầu hết các thủ tục trong thư viện cốt lõi không có chữ ký (signature) được khai báo, nghĩa là số lượng đầu vào và đầu ra phải được suy luận từ ngữ cảnh.

Các thủ tục MASM không tuân theo một quy ước gọi (calling convention) được xác định rõ ràng, và hiệu ứng ngăn xếp ròng của các lệnh gọi như vậy thường không thể xác định được một cách tĩnh. Điều này có nghĩa là mọi lỗi phân tích đều lan truyền lên chuỗi gọi.

Các vòng lặp while không cần phải trung hòa ngăn xếp (stack neutral), nghĩa là điều kiện vòng lặp while có thể chiếm một vị trí ngăn xếp khác nhau trong mỗi lần lặp. Điều này cũng khiến việc ánh xạ đầu vào của lệnh tới các vị trí ngăn xếp cho các lệnh tiếp theo trở nên bất khả thi.

Các nhánh khác nhau trong các câu lệnh điều kiện có thể có hiệu ứng ngăn xếp khác nhau, điều này cũng gây khó khăn tương tự cho việc theo dõi ngăn xếp và suy luận chữ ký.

Điều này có nghĩa là chúng tôi không thể kỳ vọng dịch ngược được tất cả các thủ tục MASM nếu muốn kết quả dịch ngược phải chính xác. Do đó, chúng tôi tập trung vào việc dịch ngược chính xác một tập con được xác định rõ của MASM. Trong quá trình phát triển trình dịch ngược, chúng tôi luân phiên sử dụng Claude để lập kế hoạch và phát triển, còn Codex để đánh giá mã. Bất cứ khi nào triển khai xong một tính năng mới, chúng tôi yêu cầu các tác nhân dịch ngược một tập hợp các thủ tục ngẫu nhiên từ thư viện cốt lõi và so sánh kết quả với MASM gốc để tìm lỗi hồi quy (regression). Bất kỳ vấn đề nào được tìm thấy đều được thêm vào dưới dạng các bài kiểm tra hồi quy để mô hình sửa chữa.

Trình dịch ngược đại diện cho nỗ lực lớn nhất trong việc phát triển công cụ cho dự án này, với hơn 100 commit do AI tạo ra trong nhiều tháng. Lợi ích chính của công việc này hóa ra lại nằm ở các khung phân tích nội bộ và biểu diễn trung gian của trình dịch ngược, thứ mà chúng tôi có thể tái sử dụng cho phân tích tĩnh, thay vì toàn bộ quy trình dịch ngược.

Với trình dịch ngược đã sẵn sàng, chúng tôi có quyền truy cập vào biểu diễn trung gian của từng thủ tục, với các đầu vào và đầu ra của lệnh được điền dưới dạng các biểu thức. Điều này cho phép chúng tôi áp dụng tất cả các cơ chế phân tích tĩnh tiêu chuẩn (như phân tích luồng dữ liệu) vào vấn đề tìm lỗi trong mã MASM. Chúng tôi đã sử dụng nó để xây dựng một số lượt phân tích trên biểu diễn trung gian, trả lời các câu hỏi như:

Các giá trị tư vấn (advice values) do người chứng minh cung cấp như số dư và nghịch đảo mô-đun có được xác thực đúng cách không?

Các ràng buộc kiểu (ví dụ: đầu vào là số nguyên 32-bit hay boolean) có được thực thi không?

Các biến cục bộ có được khởi tạo trên tất cả các đường dẫn thực thi không?

Một cách để khám phá các vấn đề này là thông qua diễn giải trừu tượng (abstract interpretation). Ý tưởng đằng sau kỹ thuật này rất đơn giản. Thay vì chạy chương trình với các con số thực, quá trình phân tích sẽ theo dõi các kiểu giá trị có thể nằm trên ngăn xếp tại mỗi bước, chẳng hạn như "số nguyên 32-bit" hoặc "không xác định". Nó đi qua mã nhiều lần cho đến khi không tìm thấy thông tin mới nào. Vì nó luôn theo dõi mọi giá trị có thể (với một chút dư thừa), nó không bao giờ bỏ sót một trường hợp thực tế nào. Vì vậy, nếu một kiểm tra vượt qua quá trình phân tích, nó được đảm bảo sẽ đúng trong mọi lần chạy thực tế của chương trình.

Chúng tôi đã sử dụng Claude và Codex để xây dựng một công cụ diễn giải trừu tượng tổng quát, sau đó triển khai một số lượt phân tích cụ thể trên đó, yêu cầu các tác nhân chuyển đổi giữa phát triển và đánh giá mã như đã mô tả ở trên. Chúng tôi cũng quyết định để các tác nhân thiết kế và xây dựng giao diện dòng lệnh cho cả trình dịch ngược và một trình kiểm tra lỗi MASM mới để cung cấp các công cụ này cho các quy trình đánh giá mã dựa trên tác nhân.

Tìm ra tất cả các lỗi!

Trong quá trình đánh giá thực tế, các phân tích này đã xác định được hơn 400 vị trí duy nhất mà việc xác thực kiểu có thể được cải thiện (tất cả đều có thể truy cập từ API công khai của thư viện) cũng như một phát hiện có mức độ nghiêm trọng cao.

Vấn đề nghiêm trọng này xuất phát từ một giá trị tư vấn bị ràng buộc lỏng lẻo trong thủ tục mod_12289, thủ tục này thực hiện phép tính modulo 12289 trên một giá trị 64-bit, với thương số và số dư được cung cấp dưới dạng các giá trị tư vấn bởi người chứng minh. Thương số được kiểm tra để đảm bảo đó là giá trị 64-bit hợp lệ (được biểu diễn dưới dạng hai phần 32-bit), nhưng số dư không bao giờ được xác thực trước khi được chuyển đến lệnh 32-bit u32overflowing_sub. Bằng cách thay đổi cẩn thận thương số và số dư để đảm bảo chúng vẫn thỏa mãn các ràng buộc do phép trừ áp đặt, chúng tôi phát hiện ra rằng có thể khiến mod_12289 trả về một giá trị không phải là số dư chính xác. Một người chứng minh độc hại có thể khai thác điều này để giả mạo chữ ký Falcon và rút sạch bất kỳ tài khoản Miden nào được kiểm soát bởi cặp khóa Falcon.

Nhưng nếu không có lỗi thì sao?

Tất cả công việc này có nghĩa là chúng tôi đã có một bộ công cụ toàn diện để hỗ trợ cả việc đánh giá mã thủ công và dựa trên tác nhân khi bước vào kiểm toán. Tuy nhiên, chúng tôi đã có nhiều thời gian để suy nghĩ về các cách khác nhằm hỗ trợ quy trình đánh giá thủ công, và chúng tôi có nhiều ý tưởng hơn mà mình muốn thử nghiệm. Ví dụ, nếu các thủ tục trong thư viện cốt lõi được triển khai chính xác và không chứa lỗi, liệu có thể chứng minh điều này bằng cách sử dụng một trợ lý chứng minh (proof assistant) như Lean không?

Hóa ra Miden VM rất phù hợp với việc mô hình hóa hình thức, vì tập lệnh nhỏ và hầu hết các lệnh đều không có tác dụng phụ. Để mô hình hóa hình thức MASM, chúng tôi bắt đầu bằng việc triển khai một bộ thực thi Miden VM tối giản trong Lean, và yêu cầu Claude xây dựng một trình dịch tự động từ các thủ tục MASM sang Lean. Trong quá trình đánh giá, chúng tôi có nhiều tác nhân làm việc song song để chứng minh tính đúng đắn của càng nhiều thủ tục càng tốt trên toàn bộ thư viện. Vì nhân Lean có thể xác thực rằng các chứng minh được tạo ra là đúng, chúng tôi chỉ cần kiểm toán thủ công các tuyên bố định lý để đảm bảo rằng mỗi định lý chứng minh đúng thuộc tính tính đúng đắn cho thủ tục tương ứng. Để đảm bảo các định lý dễ đánh giá, chúng tôi đã giới thiệu các kiểu Lean cho các phần tử trường (field elements) và các kiểu số nguyên được triển khai trong thư viện cốt lõi. Điều này có nghĩa là ở cấp độ cao, hầu hết các thuộc tính tính đúng đắn có thể được biểu diễn dưới dạng:

Nếu ngăn xếp được cho bởi [x1, x2, x3,..., xn,...] và chúng ta thực thi thủ tục P, thì P kết thúc và ngăn xếp được cho bởi [P(x1, x2, x3,..., xn),...].

Các nỗ lực mô hình hóa hình thức dựa trên tác nhân của chúng tôi đã mang lại 95 chứng minh tính đúng đắn bao phủ tất cả các thành phần số học nhị phân của thư viện cốt lõi. Công việc này cũng xác định được hai lỗi tinh vi mà bộ kiểm thử đơn vị (unit test) hiện tại không phát hiện ra. Lỗi đầu tiên là một trường hợp biên trong phép xoay phải 64-bit rotr, hoạt động không chính xác trên các đầu vào lớn hơn số nguyên tố Goldilocks nếu độ dịch chuyển xoay là bội số của 32. Lỗi thứ hai là một vấn đề trong phép nhân 256-bit wrapping_mul, vốn đã loại bỏ các giá trị thuộc sở hữu của người gọi khỏi ngăn xếp trước khi trả về.

Tại sao chúng tôi không thể làm điều này hai năm trước

Các công cụ chúng tôi phát triển trước khi thực hiện dự án này, cùng với các thư viện Lean và các chứng minh được tạo ra trong quá trình đánh giá, đều là các dự án phụ mà chúng tôi không thể dành thời gian hoặc nguồn lực cho chúng chỉ một hoặc hai năm trước. Các dự án như thế này thường mang tính khám phá cao, và kết quả cuối cùng cũng như lợi ích tiềm năng có thể khó dự đoán. Trong thực tế, điều này có nghĩa là rất khó để thuyết phục khách hàng về chúng trước. Tuy nhiên, trong năm qua, các tác nhân đã trở nên đủ tốt để thực hiện các dự án không thiết yếu như thế này với sự giám sát nhẹ nhàng, điều này đã thay đổi hoàn toàn khía cạnh kinh tế của việc dự án nào đáng để theo đuổi. Ngày nay, một dự án phụ thất bại chỉ tốn chi phí token.

Với Miden, lợi ích của tất cả công việc chuẩn bị này là rất rõ ràng. Máy chủ LSP và công cụ phân tích tĩnh đã cải thiện phạm vi đánh giá thủ công của chúng tôi, củng cố các đánh giá dựa trên tác nhân và xác định các vấn đề bảo mật thực sự trong cơ sở mã, những vấn đề có thể dẫn đến mất hàng triệu đô la. Các chứng minh tính đúng đắn Lean do AI tạo ra cũng cải thiện sự đảm bảo trên một thành phần lớn và cơ bản của thư viện, cho phép đội ngũ tiếp tục xây dựng trên đó với sự tự tin. Đội ngũ đã áp dụng công cụ phân tích tĩnh được phát triển cho cuộc đánh giá, nghĩa là dự án phụ của chúng tôi giờ đây cũng sẽ giúp bảo mật các bản cập nhật trong tương lai cho thư viện cốt lõi Miden.

Về mặt cá nhân, đây là một trong những dự án thú vị nhất mà tôi từng làm việc trong những năm ở Trail of Bits. Nếu bạn thấy loại công việc này thú vị, hoặc nếu bạn đang xây dựng thứ gì đó tương tự, hãy liên hệ với chúng tôi. Chúng tôi rất muốn nghe về điều đó!

Đây là các đầu vào được tính toán trước, được cung cấp thông qua một ngăn xếp tư vấn riêng biệt bởi người chứng minh, và cần được xác thực cẩn thận. ↩︎

Hầu hết các phát hiện này là do thực tế là gần như tất cả các thủ tục trong thư viện cốt lõi đều là một phần của API công khai, nghĩa là các nhà phát triển bên thứ ba có thể gọi chúng mà không cần xác thực đúng cách. ↩︎