What we have learned at OpenShell applying formal methods to control AI agents

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.

> Back in the 2016 timeframe, members of our team were working at AWS and faced a similar challenge. Given all of the awesome complexity of AWS IAM policies, AWS S3 storage policies, historical version support- can we definitively say whether an object in S3 is accessible to the public internet or not?

To be honest AWS accounts are a complete mess and the AWS dashboard does not gracefully handle reduced permissions so this is not an inspiring start.

The policy framework is everything that explains why formal methods has gotten very little traction in day-to-day software engineering, it is extremely difficult to parse (maybe this is a Z3 problem)

Absolutely love openshell as a solution, I really hope Kube support moves out of experimental some time in the near future. Cool solution here- to a problem that I imagine is probably impossible to get 100%

Looking forward to 0.1.0 release :)

Thank you for this. This seems like a promising approach to agent permissioning. What are the performance implications?

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