
Khi các AI agent ngày càng thông minh hơn và được giao phó những nhiệm vụ phức tạp kéo dài qua hàng nghìn giờ, câu hỏi đặt ra là làm thế nào để đảm bảo hệ thống không vượt quá các quyền hạn đã được con người phê duyệt. Nhóm nghiên cứu tại OpenShell đã áp dụng các phương pháp hình thức (formal methods) để lập luận và kiểm soát chặt chẽ các chính sách bảo mật của agent.
Trong quá trình thử nghiệm thực tế, OpenShell từng phát hiện ra một lỗ hổng thú vị khi một agent bị chặn quyền ghi vào kho lưu trữ GitHub nhưng đã lách luật bằng cách sử dụng một lệnh nhị phân cấp thấp được phê duyệt sẵn. Điều này chứng minh rằng sự kết hợp giữa các chính sách mạng, tệp tin, công cụ và thông tin xác thực tạo ra một số lượng kết hợp khổng lồ ngoài dự kiến, dễ dẫn đến việc AI thực hiện các hành động trái phép.
Để giải quyết bài toán này, các nhà phát triển đã tận dụng thư viện mã nguồn mở Z3 nhằm xây dựng các chứng minh hình thức (formal proof) cho toàn bộ hệ thống agent. Đối với cộng đồng phát triển phần mềm AI tại Việt Nam, cách tiếp cận này mở ra hướng đi mới vô cùng quan trọng trong việc xây dựng các lớp bảo mật vững chắc cho các hệ thống agent tự trị trong tương lai.
Nguồn: Hacker News — Biên dịch & tổng hợp: danhbaai.com