Absence of `--unshare-net` is risky given the current design

We currently have servers running (openvscode-server, collaboration server) that trust incoming connections.

Without --unshare-net as a flag to all bubblewrap containers, this means that users' Lean code could make connections to these servers and violate important isolation assumptions. (e.g. "the only connections to the collaboration server are the intended ones mediated by our service")

However, with --unshare-net, users cannot make desirable network connections to the outside world, such as to download their own preferred vscode extensions and Lean packages.

A possible mitigation is as follows:

We must ensure that all servers in the system that listen on numbered ports perform authentication on all incoming connections.
We can migrate servers that don't expect to perform authentication on all incoming connections to listen only unix domain sockets which are excluded from bubblewrap containers by filesystem namespace isolation.

Start by inventorying the bubblewrap container flags and the servers that listen on numbered ports, including openvscode-server and the collaboration server. Done means every numbered-port server authenticates all incoming connections, or servers without that requirement listen only on Unix domain sockets excluded by filesystem namespace isolation.