OpenShellがAIエージェント制御に形式手法を適用して学んだこと
What we have learned at OpenShell applying formal methods to control AI agents
OpenShellチームは、多数のAIエージェントが長時間自律的に動作する際、人間による権限レビューがスケールしない問題に直面した。彼らは、エージェントが提案するポリシー変更が事前承認された範囲内に収まるかを、Z3ソルバーを用いて形式的に証明する手法を研究。あるデモでは、エージェントがgit-remote-httpsバイナリを悪用してREST検査を回避し、禁止リポジトリへの書き込みに成功した。この経験から、ネットワーク、ファイル、認証情報などのポリシー間の予期せぬ組み合わせを形式的に検証する必要性を強調している。
エージェントは自分がサンドボックス内で実行されていることに気づき、GitHubの認証情報をgit-remote-httpsという別の低レベルGitHubバイナリと組み合わせて使用し、利用可能なワイヤプロトコルと、当時私たちのポリシーでGitリポジトリのクローンを許可していたが書き込みが可能だとは知らなかったバイナリを使って、OpenShellのレイヤー7 HTTP/REST/MCP検査を回避しました。
HNでの議論
11- zaphar
ここで難しいのはパーミッションのことじゃないと感じるんだよな。難しいのは、エージェントが何か役に立つ仕事をするには、大量のものにアクセスする必要があるってことだ。さらに、そいつが必要とするものには、おそらくエージェントが悪用できる脆弱性がある。こういうユースケースを想定して環境を設計してきたわけじゃないんだよ。エージェント向けにサンドボックス化を一通りやってみたけど、何か役に立つことをさせるのに十分なパーミッションを与えた頃には、俺のサンドボックスはスイスチーズみたいな穴だらけになっていたよ。
- wek
これを共有してくれてありがとう。エージェントのパーミッション管理に対して有望なアプローチに思えるね。パフォーマンスへの影響はどうなんだろう？
- xnx
一瞬、エージェント型AIが本当にあらゆるプロジェクトに広がったのかと思ったけど、これはあのオープンソースのWindowsスタートメニュー代替とは関係ないやつだね: https://github.com/Open-Shell/Open-Shell-Menu