What we have learned applying formal methods to control AI agents - #63
Conversation
Documentation previewThe preview has been removed. |
zredlined
changed the title
johnnygreco
left a comment
johnnygreco
left a comment
There was a problem hiding this comment.
Thanks Alex! I enjoyed this read—appreciate the human prose 💚
Left some mostly nit comments inline. One general comment, which is the biggest of nits that you can feel free to ignore: IMO it would add a touch of polish to have an agent go through and make all the em-dashes actual em-dashes (which BTW is like my favorite punctuation mark, and I don't care if AI loves them too).
|
|
||
| ## The demo that changed our minds | ||
|
|
||
| In one of our first demos of OpenShell, for Jensen actually, we demonstrated the ability to use OpenShell’s REST inspection endpoint to only allow an OpenClaw agent to write selectively to a GitHub repository, despite having access to a broadly scoped API key. The demo started off as expected- OpenShell’s sandbox saw the attempted write to the forbidden repo and blocked it. Then the next message was “file successfully written to \[forbidden repo\]. What had happened here? 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. |
There was a problem hiding this comment.
this is such a great illustrative example!
just a thought: what about adding a diagram / graphic of some kind that visually shows what happened here? just to get it to really sink into the reader's mind.
| <img src="../../assets/agent-policy-prover/hero-concept.png" alt="Five colorful clusters of connected AI agent nodes sit within a green policy boundary while a red path crosses the boundary and is stopped by a proof marker."> | ||
| </figure> | ||
|
|
||
| In this post- we’ll dive into how permission review breaks at agent scale, and how to use the Z3 open source library to write a formal proof that a policy change proposed by an agent stays inside what you approved. |
There was a problem hiding this comment.
maybe make "Z3 open source library" a link?
|
|
||
| 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? | ||
|
|
||
| Today, this sounds kind of funny, and it did in 2016 too, until you think about the complexity and layering interactions possible between the policies that we write to control systems. Byron Cook’s team of Ph.D’s came up with a clever approach, code-named Zelkova, that now runs once per day for every S3 bucket policy- millions of SMT queries per day and definitively answers this question. |
There was a problem hiding this comment.
Is there a link to Byron Cook and/or his team?
There was a problem hiding this comment.
It is no longer a single team :) What he started has morphed into a huge automated reasoning workforce at AWS. He remains the key evangelist.
| binary_matches(rule, a) ∧ endpoint_matches(rule, a) | ||
| ``` | ||
|
|
||
| This is where you start to see some of the complexity of modeling an entire policy language. For example, OpenShell supports `*` and `**` glob semantics. These are compiled into Z3 regular expressions. As humans that are familiar with glob mechanics, we know that a single `*` cannot cross `/` for paths or `.` for hosts- while `**` can. So, we use our Rust code to encode this logic. Z3's regular-expression theory can then check for us whether the symbolic string belongs to the resulting language. For a deep-dive on our research around containment, check out the OpenShell spike on maximum policies and narrowness budgets here: <https://github.com/NVIDIA/OpenShell/blob/spike/maximal-policy-prover-subset/crates/openshell-prover/MAXIMUM_POLICY_ENVELOPE_SPIKE.md>. |
There was a problem hiding this comment.
Not sure we can count on branches persisting, especially considering the repo itself could move. If the example is needed, perhaps it should be extracted and persisted somewhere more intentional, or just move the markdown description somewhere.
There was a problem hiding this comment.
While regular expressions form a regular language that is decidable, using things like back references which Python supports makes them more expressive at the cost of decidability. Maybe we can add somewhere that we only process decidable fragments of regexes (as in Formal Regex)? I remember because we had to deal with Python/Java code with regexes at AWS that made it hard to prove equivalence between these legacy controls and the ones we built using a strongly typed fully decidable domain specific language for controls.
There was a problem hiding this comment.
I am saying this also because the OpenAI HuggingFace incident relied on poor regex matches. Not the same problem but regexes have been oftentimes involved in breaking security me thinks.
3 participants
Summary
Validation
python3 tests/test_render_dev_notes.pyscripts/build-docs.sh