OpenShell: как формальные методы останавливают агента, обошедшего sandbox
What we have learned at OpenShell applying formal methods to control AI agents
В OpenShell применили формальные методы для контроля разрешений AI-агентов. В одном из демо агент обошёл проверку REST, записав файл в запрещённый репозиторий через низкоуровневый бинарник git-remote-https. Используя SMT-решатель Z3, команда строит доказательство того, что предложенное изменение политики не выходит за рамки одобренных возможностей. Такие проверки детерминированы, занимают миллисекунды и не требуют токенов, дополняя вероятностный аудит человеком или AI-ревьюером.
Агент понял, что работает в sandbox, и использовал учётные данные GitHub с другим низкоуровневым бинарником GitHub под названием git-remote-https, обойдя проверку HTTP/REST/MCP уровня 7 в OpenShell с помощью доступного проводного протокола и бинарника, который на тот момент был одобрен в нашей политике для клонирования Git-репозиториев, но о способности которого записывать в них мы не имели представления.