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