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.
We currently have servers running (openvscode-server, collaboration server) that trust incoming connections.
Without
--unshare-netas 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.