Questions about scope and further plans for verification and policies

[tlringer]

Hello, my name is Talia and I am a professor of computer science at UIUC (my website is here). One of my students @leejasper851 and I are interested in a potential research project on formally verified AI sandboxing, and one route that might be nice is contributing directly to OpenShell.

I saw that there is SMT-based verification of policies, which is really neat! From my understanding, that verification checks that the policy itself matches the intended behavior. With that in mind, I have a few questions:

1. Is there any formal guarantee that the sandbox actually faithfully enforces the policy (i.e., that the runtime checks are correctly implemented)?
2. If there is not such a guarantee at this time, is there any interest in such a guarantee?
3. How expressive are the policies with respect to information flow? Can they get very granular about what information can flow where, or are they mostly coarse permissions-based policies?
4. If the policies do not yet express granular information flow, is there any interest in making this possible, while preserving guarantees?
5. Is there any consideration for multi-run properties, especially with multiple agents invovled? For example, the need to include some kind of provenance when one agent writes out information that another agent may read in a future run, so that we can mark information as tainted when we want to limit the scope of multi-agent coordination over many runs? If not, is there any interest in this?

We are happy to talk to anyone who is interested in doing any of these things, but first we want a good idea of what has been done and what people are interested in. Thanks!

Talia

[gopal9097]

Hi Talia,

Thanks for the detailed questions! My understanding is that the current SMT verification checks the policy itself, but doesn’t formally verify that the runtime enforces it correctly.

The current policies are mainly permission-based rather than full information-flow control. I think extending this to runtime verification, provenance/taint tracking, and multi-agent/cross-run information flow would be a really interesting direction.

I’d be happy to discuss this further and explore a small prototype.

[tlringer]

This appears to be an AI-generated comment (pangram score of 100%) from an account created just a couple of days ago with no prior contributions to this repository.

[gopal9097]

yeah i got the concern the github account is new but i was interested in it and tried to raise a point you are right about that it is 100% ai generated text but the technical point is mine i only took help to make comment more relevent and simple for your understanding

[AAMARVA]

Welcome Talia! Seeing UIUC’s formal verification team look into NVIDIA OpenShell is fantastic.
Right now, OpenShell separates the verification engine (Policy Prover) from the execution plane (Supervisor/Kernel constraints). Bridging that gap with a formal guarantee that runtime checks perfectly match the intended policy would be huge.
Regarding multi-agent provenance (Question 5)—preventing complex interaction paths where sub-agents collectively bypass global boundaries is a known focus area for the architecture. Bringing rigorous information-flow tracking down to the sandbox level is exactly what this project needs to scale safely.

[tlringer]

This also appears to be an AI-generated comment (pangram score of 100%). Not sure what is going on here.

[AAMARVA]

Lmao, caught in 4K 😂Yeah, I used AI to help phrase it. The questions and points were mine but apparently the AI seasoning was a little too strong 💀I’ll take the L and write like a human next time.

[tlringer]

Haha sorry for being kind of adversarial here, just want to make sure I get some responses from people who are actively contributing to this repository

[CHUNCHUNMARU-d]

HI Talia, did you check the latest openAI sandbox test that went out of control?
https://openai.com/index/hugging-face-incident-and-the-road-ahead/
That is the full report i think is very interesting and worth check if you are interested on ai sandboxing

[tlringer]

Yes that is one of the big inspirations for this line of research inquiry

[briandersn]

Hi @tlringer! Let me try to route this to the relevant folks so it gets the proper attention. Formal verification of sandboxes and other security primitives should be very desirable. I mostly work with formal verification folks on the hardware side of things, but I bet they can point us in the right direction. (I'll also try to mention the potential AI spam problem to the right ppl.)

[zredlined]

Hey @tlringer - I have led a lot of the work with formal verification in Openshell to date. Happy to chat, and apologies for the confusion above with bots. We'll look into that. In the meantime, I'll reach out via the contact on your webpage. Thanks for the heads up @briandersn