document what is needed for this to be a statically verified sandbox

[JanZerebecki]

Would adding a section to the Readme about this be welcome?

Together with static analysis, I think cap-std can be used to reduce the necessary code review to know that something does not escape the capabilities handed to it. So one would only need to review the API that one uses from a crate.

For this one would need some tool(s) one could run on a crate (and recursively its dependencies) to verify that it does not use any of the following:

• cap-directories
• Dir::open_ambient_dir
• the replaced functions/modules/crates (typical clippy job, but probably no ready made lint yet, can clippy guarantee this or is something else needed?)
• unsafe (there is #![deny(unsafe_code)] https://doc.rust-lang.org/reference/attributes/diagnostics.html , I think there are ready made tools, need to find a good recommendation)
• build script https://doc.rust-lang.org/cargo/reference/build-scripts.html (no idea if there is a ready to use tool to check, but easy to code)
• check known unsoundness like Implied bounds on nested references + variance = soundness hole rust-lang/rust#25860 are not used, I think miri https://github.com/rust-lang/miri is supposed to catch it, but need to double check

Any suggestions for relevant tools?

While there is research in that direction, for now none of this is to the level of formally proven, but the constructed to be correct level known from Rust.

[sunfishcode]

As discussed here, cap-std is currently promoted for untrusted-input situations and not untrusted-code situations. I myself don't have a comprehensive list of what would be needed to handle untrusted code, but here's what I do know offhand:

A clippy configuration for scanning for some calls to functions that employ ambient authority is here. It doesn't include cap-directories though, or most third-party crates.

Rust has several open soundness bugs. I wouldn't assume that miri can catch all of them. Some of them are even miscompilations, which miri likely can't catch. I myself am not aware of anyone having studied rustc from the perspective of using it for untrusted-code sandboxing.

[ssokolow]

Given that, as far as I'm aware, LLVM is not unique in being unwilling to take responsibility for ensuring the emergent complexity of their optimization passes is free of exploitable flaws, and that Sun Microsystems tried unsuccessfully for years to squash sandboxing flaws in the Java applet runtime, I think the only real solution for this sort of thing is something specifically designed for it, like WebAssembly. (Either embedded or WASI)