Library Sandboxing for Verona

However others do end in production like Windows Phone 7 kernel, Drawbridge, P*, .NET generics, F#, FStar, Lean,..

Actually I thought Verona was no longer active.

The problem this is solving is: It's the future, and Verona is no longer a research project but instead a real language that people write production systems in. You are working in a Verona codebase and need to add a dependency on an existing library written in a memory-unsafe language like C or C++. (Perhaps, e.g., this library is the only available parser for some obscure file format, and the format is too complicated for you to feasibly write a new parser from scratch.) You do not trust this library to be free of exploitable memory-safety vulnerabilities, so you need a way to call it that doesn't allow an attacker to take over your computer if they can find such a vulnerability. And you would like this to happen in a reasonably low-engineering-overhead way, rather than having to spin up a new microservice or similar. This is what this feature is trying to offer.

This is indeed something that any memory-safe language, not just Verona, could benefit from. However, a lot of the actual work being done here is on the language-integration side, and so would have to be repeated for every new host language. It's possible that the sandbox-side work could be reused.

The actual sandboxing is done with Linux's security features like seccomp-bpf. (The readme also mentions Capsicum so I guess FreeBSD is also supported?) This is lower-overhead than Firecracker or gVisor. Firecracker and gVisor can defend against some kinds of attacks that seccomp-bpf can't, particularly bugs in the Linux kernel, and if you are deliberately running potentially-hostile code on your server then these may be worth defending against. But it's likely overkill if your goal is just to sandbox a slightly dodgy parsing library.