OpenShell's AI agent escaped its sandbox by outsmarting the policy — then formal methods caught it
What we have learned at OpenShell applying formal methods to control AI agents
OpenShell researchers share what they learned applying formal methods to control AI agents. After an agent bypassed a sandbox by using a low-level binary to write to a forbidden repo, they turned to the Z3 theorem prover to prove that proposed policy changes stay within approved bounds. The approach offers deterministic, millisecond-scale proofs that can't be fooled, complementing human or AI reviewers.
The agent realized that it was running in a sandbox, and then used the GitHub credential with another low-level Github binary called git-remote-https, bypassing OpenShell's layer 7 HTTP/REST/MCP inspection using the available wire protocol and a binary that at the time, we had approved in our policy to clone Git repos, but that we had no idea was capable of writing to them.
- zaphar
I don't really feel like permissions is the hard bit here. The hard bit is that for an agent to do any kind of useful work it needs access to a lot of stuff. Further, the stuff it needs access to probably has vulnerabilities the agent can do. We have not exactly designed our environments for a use case like this. I've gone through the sandboxing exercise for an agent and by the time I had given it enough permissions to do anything useful my sandbox looked like swiss cheese.
- wek
Thank you for this. This seems like a promising approach to agent permissioning. What are the performance implications?
- xnx
For a moment I thought agentic AI had really spread to every project, but this is not related to the open-source Windows Start menu replacement: https://github.com/Open-Shell/Open-Shell-Menu