From b9e09bc6c289a4fb5cdcf71d5cb46e0bf4cc9484 Mon Sep 17 00:00:00 2001 From: Ralf Jung Date: Thu, 21 Mar 2024 19:53:05 +0100 Subject: [PATCH 1/7] update website --- research/index.html | 11 +++++++---- 1 file changed, 7 insertions(+), 4 deletions(-) diff --git a/research/index.html b/research/index.html index d335f56..bd7b174 100644 --- a/research/index.html +++ b/research/index.html @@ -17,10 +17,13 @@ Please explain why you are interested in a PhD in this field and what your prior Note that doing a PhD at ETH Zürich generally requires a Master's degree, but there is a direct doctorate program that you can enter with a Bachelor's degree (application deadline December 15th).

-->

My two main lines of work are about Rust and Iris.
-On the Rust side, I am working (also in collaboration with the Rust language team) towards a solid formal foundation for the language, including in particular the unsafe parts. -One key result here is our type safety proof, which also describes a methodology for establishing type safety of well-encapsulated unsafe code. -My goal is to make unsafe Rust just as safe as safe Rust by means of formal verification.
-On the Iris side, besides continuing development of its logical foundations, I am interested in applying Iris to new problem domains; recently I started working on modular verification of fault-tolerant distributed system components.
+On the Rust side, me and my group are working (also in collaboration with the Rust language team) towards a solid formal foundation for the language, including in particular the unsafe parts. +As part of this we are developing Miri, a practical tool for detecting Undefined Behavior bugs in unsafe Rust code, which has become a part of the standard toolbox of unsafe code authors. +Meanwhile, MiniRust is our work-in-progress proposal for a precise specification of unsafe Rust, that I hope to integrate into an official Rust specification eventually. +My long-term goal is to make unsafe Rust just as safe as safe Rust by means of formal verification based on rigorous foundations for all key components of the language.
+On the Iris side, I am continuing development of its logical foundations. +We are making Iris fit for specifying and verifying programming languages at scale using a more modular approach. +The long-term goal is for Iris to be able to handle the full scale of complexities that arise when doing foundational verification of real languages.
For some more information, check out my research blog, my CV, and my research statement.

In my free time, I like to run internet services myself and work on free software. -- 2.30.2 From 5a209269bef4653c72996235995eb0742a886f1a Mon Sep 17 00:00:00 2001 From: Ralf Jung Date: Sun, 14 Apr 2024 13:09:18 +0200 Subject: [PATCH 2/7] projects: sort alphabetically --- personal/_config.yml | 8 ++++---- personal/projects/index.md | 10 +++++----- 2 files changed, 9 insertions(+), 9 deletions(-) diff --git a/personal/_config.yml b/personal/_config.yml index d63d639..f2c5c2a 100644 --- a/personal/_config.yml +++ b/personal/_config.yml @@ -12,13 +12,13 @@ readmes: src_base: "/home/r/src" out_base: "projects" projects: - - name: "lilass" - name: "dyn-nsupdate" - - name: "zonemaker" - - name: "schsh" + - name: "git-mirror" + - name: "lilass" - name: "rust-101" src: "rust/rust-101" - - name: "git-mirror" + - name: "schsh" + - name: "zonemaker" defaults: - scope: diff --git a/personal/projects/index.md b/personal/projects/index.md index c5d3f4a..988c471 100644 --- a/personal/projects/index.md +++ b/personal/projects/index.md @@ -7,17 +7,17 @@ To solve some issue I was having, or to facilitate my daily computer usage. The tools were usually not written with general re-usability in mind. But maybe you are having just the same problem as I did, in which case I hope they can be helpful. +* [dyn-nsupdate](dyn-nsupdate/): A tool to dynamically and securely update DNS zones via CGI. + This provides self-hosted DynDNS services. +* [git-mirror](git-mirror/): This can keep multiple git repositories of the same project in sync automatically. * [LiLaSS](lilass/): A simple xrandr-based application to configure laptop screens on Linux. If you are using a Laptop, frequently work both with and without an external screen, and you are not happy with the configuration options your desktop provides, this may be for you. -* [dyn-nsupdate](dyn-nsupdate/): A tool to dynamically and securely update DNS zones via CGI. - This provides self-hosted DynDNS services. -* [zonemaker](zonemaker/): A small script to generate DNS zone files from Python. +* [Rust-101](rust-101/): A small tutorial for the [Rust language](https://www.rust-lang.org). * [schsh](schsh/): A collection of scripts and configuration files which can be used to grant someone secure (SSH-based) access to a machine, without giving them a shell or read access to the entire file system. -* [Rust-101](rust-101/): A small tutorial for the [Rust language](https://www.rust-lang.org). -* [git-mirror](git-mirror/): This can keep multiple git repositories of the same project in sync automatically. +* [zonemaker](zonemaker/): A small script to generate DNS zone files from Python. For some more of my projects, check out the [public git repositories](https://www.ralfj.de/git/) hosted on my server and my [GitHub profile](https://github.com/RalfJung/). -- 2.30.2 From 43307ef533738f9b108a6daa91541692f396a725 Mon Sep 17 00:00:00 2001 From: Ralf Jung Date: Sun, 14 Apr 2024 16:53:11 +0200 Subject: [PATCH 3/7] add bubblebox and blog about it --- personal/_config.yml | 1 + personal/_posts/2024-04-14-bubblebox.md | 68 +++++++++++++++++++++++++ personal/projects/index.md | 13 ++--- 3 files changed, 76 insertions(+), 6 deletions(-) create mode 100644 personal/_posts/2024-04-14-bubblebox.md diff --git a/personal/_config.yml b/personal/_config.yml index f2c5c2a..959b104 100644 --- a/personal/_config.yml +++ b/personal/_config.yml @@ -12,6 +12,7 @@ readmes: src_base: "/home/r/src" out_base: "projects" projects: + - name: "bubblebox" - name: "dyn-nsupdate" - name: "git-mirror" - name: "lilass" diff --git a/personal/_posts/2024-04-14-bubblebox.md b/personal/_posts/2024-04-14-bubblebox.md new file mode 100644 index 0000000..85dc684 --- /dev/null +++ b/personal/_posts/2024-04-14-bubblebox.md @@ -0,0 +1,68 @@ +--- +title: "Sandboxing All The Things with Flatpak and BubbleBox" +categories: sysadmin +--- + +A few years ago, I have [blogged]({% post_url 2019-03-09-firejail %}) about my approach to sandboxing less-trusted applications that I have to or want to run on my main machine. +The approach has changed since then, so it is time for an update. + + + +Over time I grew increasingly frustrated with Firejail: configurations would frequently break on updates, +and debugging Firejail profiles is extremely hard. When considering all the included files, we are talking +about many hundred lines of configuration with a subtle interplay of allowlists and blocklists. +Even when I knew which folder I wanted to give access to, it was often non-trivial to ensure that +this access would actually be possible. + +Now I am instead using a combination of two different approaches: Flatpak and BubbleBox. + +## Flatpak + +The easiest sandbox to maintain is the sandbox maintained by someone else. +So when a Flatpak exists for software I want to or have to use, such as Signal or Zoom, that is generally my preferred approach. + +Unfortunately, Flatpaks can come with extremely liberal default profiles that make the sandbox mostly pointless. +The following global overrides help ensure that this does not happen: +``` +[Context] +sockets=!gpg-agent;!pcsc;!ssh-auth;!system-bus;!session-bus +filesystems=~/.XCompose:ro;xdg-config/fontconfig:ro;!~/.gnupg;!~/.ssh;!xdg-documents;!home;!host + +[Session Bus Policy] +org.freedesktop.Flatpak=none +org.freedesktop.secrets=none +``` + +## BubbleBox + +However, not all software exists as Flatpak. +Also, sometimes I want software to run basically on my host system (i.e., to use the regular `/usr`), just without access to literally *everything* in my home directory. +Examples of this are Factorio and VSCodium. +The latter doesn't work in Flatpak as I want to use it with LaTeX, and realistically this means it needs to run the LaTeX on my host. +The official recommendation is to effectively disable the Flatpak sandbox, but that entirely defeats the point, so I went looking for alternatives. + +[bubblewrap] provides a very convenient solution: it can start an application in its own private filesystem namespace with full control over which part of the host file system is accessible from inside the sandbox. +I wrote a small wrapper around bubblewrap to make this configuration a bit more convenient to write and manage; +this project is called [BubbleBox]. +This week-end I finally got around to adding support for [xdg-dbus-proxy] so that sandboxed applications can now access particular D-Bus functions without having access to the entire bus (which is in general not safe to expose to a sandboxed application). +That means it's finally time to blog about this project, so here we go -- if you are interested, check out [BubbleBox]; +the project page explains how you can use it to set up your own sandboxing. +One day I should probably rewrite this in Rust... + +I should also note that this is not the only bubblewrap-based sandboxing solution. +[bubblejail] is fairly similar but provides a configuration GUI and a good set of default provides; +it was a very useful resource when figuring out the right bubblewrap flags to make complex GUI applications work properly. +(Incidentally, "bubblejail" is also how I called my own script originally, but then I realized that the name is already taken.) +Joachim Breitner also recently [blogged](https://www.joachim-breitner.de/blog/812-Convenient_sandboxed_development_environment) about his own bubblewrap-based sandboxing script. +There are many ways to do this, and it was fun to figure out my own solution. + +Using bubblewrap and xdg-dbus-proxy for this was an absolute joy. +Both of these components came out of the Flatpak project, but the authors realized that they could be independently useful, +so in best Unix tradition they turned them into tools that provide all the required mechanism without hard-coding any sort of policy. +Despite doing highly non-trivial tasks, they are both pretty easy to use and compose and very well-documented. +Thanks a lot to everyone involved! + +[bubblewrap]: https://github.com/containers/bubblewrap +[BubbleBox]: {{ site.baseurl }}/projects/bubblebox +[xdg-dbus-proxy]: https://github.com/flatpak/xdg-dbus-proxy +[bubblejail]: https://github.com/igo95862/bubblejail diff --git a/personal/projects/index.md b/personal/projects/index.md index 988c471..f872845 100644 --- a/personal/projects/index.md +++ b/personal/projects/index.md @@ -7,17 +7,18 @@ To solve some issue I was having, or to facilitate my daily computer usage. The tools were usually not written with general re-usability in mind. But maybe you are having just the same problem as I did, in which case I hope they can be helpful. -* [dyn-nsupdate](dyn-nsupdate/): A tool to dynamically and securely update DNS zones via CGI. +* [BubbleBox](bubblebox): A simple script to sandbox Linux applications. +* [dyn-nsupdate](dyn-nsupdate): A tool to dynamically and securely update DNS zones via CGI. This provides self-hosted DynDNS services. -* [git-mirror](git-mirror/): This can keep multiple git repositories of the same project in sync automatically. -* [LiLaSS](lilass/): A simple xrandr-based application to configure laptop screens on Linux. If you are using a +* [git-mirror](git-mirror): This can keep multiple git repositories of the same project in sync automatically. +* [LiLaSS](lilass): A simple xrandr-based application to configure laptop screens on Linux. If you are using a Laptop, frequently work both with and without an external screen, and you are not happy with the configuration options your desktop provides, this may be for you. -* [Rust-101](rust-101/): A small tutorial for the [Rust language](https://www.rust-lang.org). -* [schsh](schsh/): A collection of scripts and configuration files which can be used to grant +* [Rust-101](rust-101): A small tutorial for the [Rust language](https://www.rust-lang.org). +* [schsh](schsh): A collection of scripts and configuration files which can be used to grant someone secure (SSH-based) access to a machine, without giving them a shell or read access to the entire file system. -* [zonemaker](zonemaker/): A small script to generate DNS zone files from Python. +* [zonemaker](zonemaker): A small script to generate DNS zone files from Python. For some more of my projects, check out the [public git repositories](https://www.ralfj.de/git/) hosted on my server and my [GitHub profile](https://github.com/RalfJung/). -- 2.30.2 From e6148fff016bf85c5e4b559a4d69f2deaac0e7ed Mon Sep 17 00:00:00 2001 From: Ralf Jung Date: Sun, 14 Apr 2024 17:01:25 +0200 Subject: [PATCH 4/7] mention cargo-script --- personal/_posts/2024-04-14-bubblebox.md | 7 ++++--- 1 file changed, 4 insertions(+), 3 deletions(-) diff --git a/personal/_posts/2024-04-14-bubblebox.md b/personal/_posts/2024-04-14-bubblebox.md index 85dc684..cc8aa88 100644 --- a/personal/_posts/2024-04-14-bubblebox.md +++ b/personal/_posts/2024-04-14-bubblebox.md @@ -38,7 +38,7 @@ org.freedesktop.secrets=none However, not all software exists as Flatpak. Also, sometimes I want software to run basically on my host system (i.e., to use the regular `/usr`), just without access to literally *everything* in my home directory. Examples of this are Factorio and VSCodium. -The latter doesn't work in Flatpak as I want to use it with LaTeX, and realistically this means it needs to run the LaTeX on my host. +The latter doesn't work in Flatpak as I want to use it with LaTeX, and realistically this means it needs to run the LaTeX installed via `apt`. The official recommendation is to effectively disable the Flatpak sandbox, but that entirely defeats the point, so I went looking for alternatives. [bubblewrap] provides a very convenient solution: it can start an application in its own private filesystem namespace with full control over which part of the host file system is accessible from inside the sandbox. @@ -46,8 +46,9 @@ I wrote a small wrapper around bubblewrap to make this configuration a bit more this project is called [BubbleBox]. This week-end I finally got around to adding support for [xdg-dbus-proxy] so that sandboxed applications can now access particular D-Bus functions without having access to the entire bus (which is in general not safe to expose to a sandboxed application). That means it's finally time to blog about this project, so here we go -- if you are interested, check out [BubbleBox]; -the project page explains how you can use it to set up your own sandboxing. -One day I should probably rewrite this in Rust... +the project page explains how you can use it to set up your own sandboxing.[^1] + +[^1]: One day I should probably rewrite this in Rust... maybe this will be my test project for when [cargo-script](https://rust-lang.github.io/rfcs/3424-cargo-script.html) becomes available. I should also note that this is not the only bubblewrap-based sandboxing solution. [bubblejail] is fairly similar but provides a configuration GUI and a good set of default provides; -- 2.30.2 From fabd70c35d0fa85dc1efc714678f67618bd269ba Mon Sep 17 00:00:00 2001 From: Ralf Jung Date: Mon, 15 Apr 2024 14:42:38 +0200 Subject: [PATCH 5/7] link to flatseal --- personal/_posts/2024-04-14-bubblebox.md | 4 ++++ 1 file changed, 4 insertions(+) diff --git a/personal/_posts/2024-04-14-bubblebox.md b/personal/_posts/2024-04-14-bubblebox.md index cc8aa88..6a90b06 100644 --- a/personal/_posts/2024-04-14-bubblebox.md +++ b/personal/_posts/2024-04-14-bubblebox.md @@ -33,6 +33,10 @@ org.freedesktop.Flatpak=none org.freedesktop.secrets=none ``` +[Flatseal] is an amazing application that helps to check which permissions applications get, and change them if necessary. + +[Flatseal]: https://flathub.org/apps/com.github.tchx84.Flatseal + ## BubbleBox However, not all software exists as Flatpak. -- 2.30.2 From b3391a7aa88717959dddfef6178de815b09ffa90 Mon Sep 17 00:00:00 2001 From: Ralf Jung Date: Mon, 15 Apr 2024 14:43:15 +0200 Subject: [PATCH 6/7] wording --- personal/_posts/2024-04-14-bubblebox.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/personal/_posts/2024-04-14-bubblebox.md b/personal/_posts/2024-04-14-bubblebox.md index 6a90b06..cd8f050 100644 --- a/personal/_posts/2024-04-14-bubblebox.md +++ b/personal/_posts/2024-04-14-bubblebox.md @@ -33,7 +33,7 @@ org.freedesktop.Flatpak=none org.freedesktop.secrets=none ``` -[Flatseal] is an amazing application that helps to check which permissions applications get, and change them if necessary. +I also use [Flatseal], an amazing application that helps to check which permissions applications get, and change them if necessary. [Flatseal]: https://flathub.org/apps/com.github.tchx84.Flatseal -- 2.30.2 From 75454324a78c1fb97500bee0e53adfc613f0fbb3 Mon Sep 17 00:00:00 2001 From: Ralf Jung Date: Mon, 15 Apr 2024 16:18:26 +0200 Subject: [PATCH 7/7] link to sloonz's script --- personal/_posts/2024-04-14-bubblebox.md | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) diff --git a/personal/_posts/2024-04-14-bubblebox.md b/personal/_posts/2024-04-14-bubblebox.md index cd8f050..56a23a6 100644 --- a/personal/_posts/2024-04-14-bubblebox.md +++ b/personal/_posts/2024-04-14-bubblebox.md @@ -59,7 +59,9 @@ I should also note that this is not the only bubblewrap-based sandboxing solutio it was a very useful resource when figuring out the right bubblewrap flags to make complex GUI applications work properly. (Incidentally, "bubblejail" is also how I called my own script originally, but then I realized that the name is already taken.) Joachim Breitner also recently [blogged](https://www.joachim-breitner.de/blog/812-Convenient_sandboxed_development_environment) about his own bubblewrap-based sandboxing script. -There are many ways to do this, and it was fun to figure out my own solution. +sloonz has a similar [script](https://gist.github.com/sloonz/4b7f5f575a96b6fe338534dbc2480a5d) as well, with a nice yaml-based configuration format and [great explanations](https://sloonz.github.io/posts/sandboxing-1/) for what all the flags exactly do. +Had their script existed when I started what eventually became BubbleBox, I would have used it as a starting point. +But it was also fun to figure out my own solution. Using bubblewrap and xdg-dbus-proxy for this was an absolute joy. Both of these components came out of the Flatpak project, but the authors realized that they could be independently useful, -- 2.30.2