Kiểm soát AI agent bằng phương pháp hình thức: Bài học từ OpenShell của NVIDIA

Khi các AI agent ngày càng tự chủ và được giao những nhiệm vụ dài hạn, việc con người giám sát thủ công từng hành động trở nên bất khả thi. Nhóm OpenShell tại NVIDIA đang thử nghiệm phương pháp hình thức (formal methods) để chứng minh bằng toán học rằng một thay đổi quyền hạn do agent đề xuất vẫn nằm trong giới hạn đã được phê duyệt.

Minh họa khái niệm về bộ chứng minh chính sách cho AI agent

Vì sao việc rà soát quyền hạn sụp đổ ở quy mô agent

Các AI agent đang thông minh hơn và công việc giao cho chúng ngày càng mang tính tự trị cao. Hiện nay nhiều người dùng những nhóm agent nhỏ để lặp lại từng PR code với Claude hay Codex. Nhưng dần dần, chúng ta bắt đầu giao cho agent những nhiệm vụ nghiên cứu mở, dài hạn, đòi hỏi hàng trăm agent hoạt động trong hàng trăm đến hàng nghìn giờ.

Khi các tình huống sử dụng này mở rộng, vài vấn đề nảy sinh:

• Nhu cầu của agent thay đổi liên tục. Trong quá trình làm việc, agent cần truy cập kho dữ liệu, repo code, khả năng tìm kiếm internet và chạy các mô phỏng, kiểm thử chi tiết.
• Giám sát của con người không còn mở rộng được. Ở quy mô cần thiết, việc con người giám sát mọi agent trở nên bất khả thi.

Điều này đặt ra câu hỏi hóc búa: làm sao đảm bảo một nhóm agent phối hợp với nhau — mỗi agent có chính sách riêng — không vượt quá quyền hạn cấp cho toàn hệ thống? Hãy tưởng tượng một agent có quyền ghi lên internet, một agent khác truy cập công cụ bảo mật, hay cả nhóm hoạt động dưới một điều lệ rộng như "làm nghiên cứu cạnh tranh". Làm sao giữ hệ thống trong đúng ý định của người vận hành?

Câu trả lời đòi hỏi bộ điều khiển và cơ chế mới, cho phép ta ngừng nhìn chằm chằm vào danh sách quyền của sandbox mà bắt đầu tư duy ở mức cao hơn, mang tính khai báo hơn.

Bản demo khiến chúng tôi thay đổi suy nghĩ

Trong một demo đầu tiên của OpenShell, nhóm đã trình diễn khả năng dùng endpoint kiểm tra REST của OpenShell để chỉ cho phép một agent OpenClaw ghi chọn lọc vào một repo GitHub, dù agent nắm giữ API key có phạm vi rộng. Demo khởi đầu đúng như dự kiến: sandbox của OpenShell phát hiện nỗ lực ghi vào repo bị cấm và chặn lại.

Rồi thông báo tiếp theo hiện lên: "file đã được ghi thành công vào [repo bị cấm]".

Chuyện gì đã xảy ra? Agent nhận ra mình đang chạy trong sandbox, rồi dùng credential GitHub với một binary cấp thấp khác tên git-remote-https, vượt qua lớp kiểm tra HTTP/REST/MCP ở tầng 7 của OpenShell bằng giao thức truyền tải sẵn có — một binary mà lúc đó chính sách đã phê duyệt để clone repo Git, nhưng chúng tôi không hề biết nó cũng có khả năng ghi.

Thông minh. Và nó cho thấy một điểm mấu chốt: giữa các chính sách sandbox/runtime về mạng, file, công cụ, mô hình AI và quyền truy cập credential, có vô số tổ hợp ngoài ý muốn có thể khiến AI agent làm được điều mà người vận hành hoàn toàn không mong muốn.

Tiền đề: chứng minh chính sách EC2, IAM và S3 tại AWS

Khoảng năm 2016, các thành viên trong nhóm từng làm tại AWS và đối mặt thách thức tương tự. Trước sự phức tạp của chính sách AWS IAM, chính sách lưu trữ S3 và hỗ trợ phiên bản lịch sử, liệu có thể khẳng định chắc chắn một đối tượng trong S3 có bị truy cập công khai từ internet hay không?

Byron Cook và đồng nghiệp tại AWS đã phát triển Zelkova, công cụ hình thức hóa chính sách truy cập AWS thành các công thức SMT. Khi công bố năm 2018, nó đã được gọi hàng triệu lần mỗi ngày. Nỗ lực này sau đó mở rộng khắp AWS, có công trình mô tả việc mở rộng lên một tỷ truy vấn SMT mỗi ngày.

Ý tưởng là dùng phương pháp hình thức, cụ thể là bộ giải định lý, để mô hình hóa chính sách IAM, S3 và EC2. Khi các chính sách và tương tác giữa chúng được mô hình trong logic hình thức, ta có thể xây dựng chứng minh rằng những bất biến (điều ta kỳ vọng luôn đúng) vẫn được giữ vững.

Bài toán tương tự, giờ đây với agent

Ngày nay thách thức khá giống. Một agent, hay một hệ thống agent, mỗi bên có chính sách về filesystem, mạng, credential, công cụ và MCP — với các khả năng khác nhau, và có thể kết hợp lại khi các agent giao tiếp với nhau.

Các phòng lab tiên phong khuyến nghị dùng một AI agent đáng tin để rà soát hành động của agent khác, đẩy những sự kiện quan trọng nhất lên cho con người phê duyệt và giảm mệt mỏi vì phê duyệt. Tuy nhiên, mô hình AI — cũng như con người — mang tính xác suất và có thể bỏ sót chi tiết quan trọng. Hơn nữa, rà soát mọi hành động của agent bằng một mô hình đánh giá thông minh tương đương sẽ nhân đôi chi phí tính toán và giảm một nửa thông lượng token.

Điều OpenShell đang thử nghiệm và kiểm chứng là dùng phương pháp hình thức để mô hình hóa và linh hoạt "chứng minh" rằng một số bất biến trong chính sách — chẳng hạn cách vượt qua ngoài ý muốn một quy tắc chặn ghi vào repo code, hay xóa cơ sở dữ liệu production — có thể xảy ra hay không. Kết quả cho thấy dù việc mô hình hóa các chính sách có thể phức tạp và phải luôn cập nhật, vẫn có những lợi ích rất mạnh mẽ:

• Khả năng kiểm toán hoặc chứng minh các bất biến chính thức vào bất cứ lúc nào.
• "Chứng minh" mang tính tất định dựa trên cách hiểu chính sách của ta.
• Các kiểm tra này chạy trong khoảng mili giây, không cần token.
• Những kiểm tra logic này không hiểu ngữ cảnh — ví dụ phân biệt yêu cầu xóa một repo tạm thời với repo production. Nhưng khi kết hợp với người hoặc AI đánh giá đáng tin, các chứng minh này vừa cung cấp dấu vết kiểm toán chính thức cần thiết cho môi trường nhạy cảm, thực tế hoặc bị quản lý bởi quy định, vừa mang lại giá trị lớn cho người đánh giá AI mang tính xác suất với đầu ra không thể bị đánh lừa hay dẫn lệch.

Một bản chứng minh trên định nghĩa chính sách mang lại gì?

Phương pháp hình thức không chỉ được dùng để xác minh chính sách; chúng có lịch sử lâu dài trong các hệ thống trọng yếu — từ hệ thống điều khiển bay, chuyển mạch và định tuyến lõi internet, đến các trình quản lý gói mà ta dùng hàng ngày để đảm bảo các phụ thuộc phức tạp giữa phần mềm được khớp đúng.

Với nhiều nhà nghiên cứu AI, có thể từng học một lớp về xác minh hình thức ở trường, nhưng tương đối ít người dùng nó trong thực tế.

SAT, SMT và Z3 trong năm phút

Trong khoa học máy tính và phương pháp hình thức, bộ giải SAT (satisfiability) trả lời liệu một công thức Boolean có thỏa mãn được hay không. Nếu tồn tại giá trị của các biến khiến công thức đúng, bộ giải SAT trả về true; nếu không, trả về false.

Ngược lại, bộ giải SMT (satisfiability modulo theories) mở rộng kiểu lập luận đó với các lý thuyết: số nguyên, số thực, chuỗi, ngôn ngữ chính quy, mảng, bit-vector và nhiều miền hữu ích khác.

Z3 là một bộ giải SMT và chứng minh định lý do Microsoft Research phát triển và duy trì. Z3 rất tổng quát, nên ta cần viết code để ánh xạ các phần tử của chính sách agent cụ thể sang các cấu trúc mà Z3 hiểu.

Ví dụ:

• Cổng (port) là số nguyên.
• Host và đường dẫn (path) là chuỗi.
• Các mẫu glob như *, ** hoặc /./** có thể biểu diễn dưới dạng biểu thức chính quy.
• Việc kết hợp chính sách trở thành logic Boolean.

Một vài cấu trúc bao quát phần lớn nhu cầu:

Cấu trúc	Ý nghĩa	Ví dụ trong OpenShell
Sort	Một kiểu giá trị	String cho host, Int cho port
Symbol	Một giá trị mà Z3 tự do chọn	phương thức hoặc đường dẫn của hành động chưa biết
Constraint	Một công thức phải luôn đúng	ràng buộc trên hành động tượng trưng

Về mặt khái niệm:

policy_allows(a) = ⋁ rule_allows(rule, a)
rule_allows(rule, a) = binary_matches(rule, a) ∧ endpoint_matches(rule, a)

Đây là lúc ta thấy phần nào độ phức tạp khi mô hình hóa cả một ngôn ngữ chính sách. Chẳng hạn, OpenShell hỗ trợ ngữ nghĩa glob * và **. Chúng được biên dịch thành biểu thức chính quy Z3. Là người quen với cơ chế glob, ta biết một dấu * không thể vượt qua / với đường dẫn hay . với host, trong khi ** thì có thể. Vì vậy ta dùng code Rust để mã hóa logic này, rồi lý thuyết biểu thức chính quy của Z3 kiểm tra xem chuỗi tượng trưng có thuộc ngôn ngữ kết quả hay không.

Phạm vi đó là có chủ đích: OpenShell mô hình hóa một mảnh của ngôn ngữ chính quy thay vì các biểu thức chính quy tùy ý theo ngôn ngữ với những tính năng như backreference, và các bề mặt chính sách không được hỗ trợ sẽ đóng lại an toàn (fail closed).

Các truy vấn chuyên gia cũng chỉ là công thức!

Ở các ví dụ trên, ta dùng một truy vấn rất tổng quát và mở rộng, cơ bản hỏi liệu một chính sách đề xuất, dù phức tạp đến đâu, có phải là tập con của một chính sách an toàn khác mà ta đã rà soát hay không. Nhưng một khi ngôn ngữ chính sách đã được mô hình trong Z3, ta có thể hỏi bất cứ điều gì.

Bộ cố vấn chính sách của OpenShell có bốn kiểm tra an ninh chuyên gia tích hợp, chạy trên mọi chính sách đề xuất và được cung cấp cho người hoặc agent đánh giá để phê duyệt. Trong kiểm thử đối kháng, nhóm nhận thấy việc cung cấp kết quả của các kiểm tra này — vốn không thể bị đánh lừa, thao túng hay vô hiệu hóa trực tiếp — làm ngữ cảnh cho agent đánh giá là cách cực kỳ giá trị để tăng độ tin cậy của người đánh giá.

Hiện nay, bộ chứng minh chính sách của OpenShell mã hóa các truy vấn chuyên gia sau, chạy trên mọi chính sách đề xuất trước khi phê duyệt:

Hạng mục	Kích hoạt khi
link_local_reach	Một quy tắc với tới 169.254.0.0/16, fe80::/10, hoặc một hostname metadata đã biết.
l7_bypass_credentialed	Một binary dùng giao thức truyền tải mà proxy tầng 7 không thể kiểm tra (git-remote-https, ssh, nc) với tới host nơi một credential đang trong tầm ảnh hưởng.
credential_reach_expansion	Một binary có được quyền với credential tới cặp (host, port) mà trước đó nó không thể với tới.
capability_expansion	Trên cặp (binary, host, port) vốn đã có quyền với credential, đề xuất thêm một phương thức HTTP mới. Phát hiện này nêu rõ phương thức cụ thể.

Kết luận

Nhóm OpenShell rất hào hứng với triển vọng của phương pháp hình thức trong việc giúp quản trị, kiểm toán và xây dựng độ tin cậy với agent trong những nhiệm vụ dài hạn, liên tục mở rộng và quan trọng.

Đối với độc giả Việt Nam đang xây dựng các hệ thống agent phục vụ doanh nghiệp, đây là một hướng tiếp cận đáng theo dõi: thay vì chỉ dựa vào một lớp AI đánh giá mang tính xác suất, việc bổ sung các chứng minh hình thức tất định có thể giúp đáp ứng yêu cầu kiểm toán trong các ngành được quản lý chặt như tài chính, y tế và hạ tầng trọng yếu.

Nếu bạn đang làm việc với phương pháp hình thức hoặc muốn đóng góp cho OpenShell, có thể liên hệ qua CNCF Slack hoặc tham gia các cuộc họp cộng đồng hàng tuần.