Ingo Blechschmidt

@anselmschueler@ieji.de @nixos_org@chaos.social @leah@blahaj.social @identical9213@mastodon.social Sorry, now that I reread these two posts I agree that it's somewhat confusing. It's about two distinct kernel patches. The patch provided in https://codeberg.org/iblech/secure-suspend is what I originally set out to do. This patch provides a new kernel feature, namely locking+suspending in one go. Without this patch, user space needs to do the locking in a separate step. This opens a short window of time where the encrypted volume is no longer accepting read/write requests, because the key has been wiped from the LUKS data structures, but kernel tasks might still want to access the volume. The inconvenient (but harmless) result: standby fails. The patch provided in https://lore.kernel.org/all/ajKwRtP8izwRsMmv@quasitopos/ fixes the bug that opening an encrypted volume permanently committed a leftover copy of the volume key in memory which was never wiped (until device close). This patch fixes the common use case of a LUKS volume on a physical block device, but (as Ondrej Kozina discovered) not the use case where cryptsetup creates a loop device to do its bidding, so it is incomplete. The upcoming release 2.8.7 of cryptsetup will contain a patch working around the kernel bug.

A quick follow-up to this key wiping bug: Ondrej Kozina from the cryptsetup team was very quick to pick this up. Ondrej has developed a patch for cryptsetup which works around the kernel bug, which is scheduled to land in the upcoming 2.8.7 release: https://gitlab.com/cryptsetup/cryptsetup/-/merge_requests/937 Also, while reviewing my proposed kernel patch, Ondrej discovered a related issue in the loop block device system: https://lore.kernel.org/all/ea67ab0e-a039-460e-ab5b-a448995bbd31@redhat.com/ This means in particular that my one-line kernel patch is incomplete. It only covers the common case of having the encrypted volume on a physical block device rather than a virtual loop device. I really enjoyed these open-source interactions and am grateful for the work of Ondrej and all the others :-)

@nixos_org@chaos.social @leah@blahaj.social @identical9213@mastodon.social Announcing experimental secure suspend-to-RAM for NixOS Normally (and somewhat embarrassingly, considering that it's the 21st century), full-disk encryption gives you no protection while your laptop is suspended: the keys sit in memory, susceptible to cold boot attacks and other ways of exfiltrating your RAM. This project fixes this, by resurrecting an old kernel patch by Pali Rohár to wipe the LUKS encryption keys on suspend. Inspired by Debian's cryptsetup-suspend, but, thanks to the kernel patch, without the (harmless but) inconvenient race condition which sometimes blocks the laptop from going to sleep, and with a couple of extra precautions. Fully supports the root filesystem being encrypted. Integration test available. Enjoy; bug reports are welcome! Both the kernel patch and the userspace tooling around it could be adapted to other Linux distributions. https://codeberg.org/iblech/secure-suspend

So. For the past few days I've been deep in a fun and very rewarding, but also extremely scary debugging saga. To cut a long git-bisecting story short: Since Linux 6.9 (May 2024), the tool that locks the laptop's drive on suspend had been silently failing. Like many of my friends, I use full-disk encryption (LUKS) to protect my data if my laptop is lost, seized or stolen. Highly recommended to everyone; in combination with tested and automated backups, it contributes greatly to peace of mind. (Under Windows, the canonical software to do that is VeraCrypt.) Except that, for more than two years, the encryption key remained resident in memory across suspend, leaving it there for the taking by anyone who seized the still-powered laptop. (It still worked on a full shutdown, but a full shutdown is rare these days.) There is something uniquely unsettling about trusting a security mechanism for years and learning it was never doing the thing. "A technical argument by a trusted author, which is hard to check and looks similar to arguments known to be correct, is hardly ever checked in detail." The same, it seems, is true for computer code. The culprit was a sensible and useful refactoring, https://git.kernel.org/pub/scm/linux/kernel/git/torvalds/linux.git/commit/?id=a28d893eb3270cf62c10dd8777af0d8452cdc072 But it had an unexpected long-range interaction with the encryption code. The fix is exactly one line long: https://lore.kernel.org/all/ajKwRtP8izwRsMmv@quasitopos/ And no, without formal proofs I cannot say whether my patch is correct and free of its own long-range interactions... At the very least, we now have an automated test to detect future regressions (https://github.com/NixOS/nixpkgs/pull/532499) and a patch to emit a warning instead of failing silently (https://gitlab.com/cryptsetup/cryptsetup/-/merge_requests/936)

@jeanas@mathstodon.xyz Also, in type theory, the formalization of "the type A is inhabited" is precisely "A" :-) (Or the truncation "∥ A ∥".) More seriously, in constructive mathematics, "X ≬ Y" is used to express that X and Y have an element in common.

@andrejbauer@mathstodon.xyz @JacquesC2@types.pl (off topic and inconsequential) Well, as you know, there is the *universal algorithm*. This algorithm has the property that, for every function f : ℕ → ℕ, there is a universe such that, when run there, it computes exactly f [on all standard inputs]. But this universe does not contain a proof of this fact. Indeed, it contains a disproof. :-) Newcomers to the universal algorithm might enjoy this introduction: https://juliakw.net/research/talks/2020-oct-universal-algorithm/univ-alg.pdf (slides by Kameryn Williams)

@annabonnie@mastodon.social @lug_augsburg@chaos.social @fsfe@mastodon.social That was an amazing keynote with a strong and very well-put message, thank you Bonnie!

@dwarn @jdw Yes exactly :-) I was unsure whether this document contains the most recent state of affairs or whether one of you has some news which have not yet been written down :-)

@jdw Right now just a quick note: There are some notes on a constructive treatment of the main theorem of elimination theory in the context of synthetic algebraic geometry; I suggest that you write to Felix Cherubini and Marc Nieper-Wißkirchen, with me in Cc, to obtain their most recent version / the current thoughts of these two persons to avoid duplicate work :-) (note that working synthetically, they don't have a need for a localic approach)

@jdw Then please solve Conjecture 21.17 of my thesis, https://rawgit.quasicoherent.io/iblech/internal-methods/master/notes.pdf thereby obtaining a description of the theory classified by the big ph Zariski topos :-)

@dpiponi@mathstodon.xyz Very nice point of view! Also neatly visible in the construction of the free functor on a type constructor t :: Type → Type: data FreeF t a = MkFreeF (exists r. (t r, r → a)) A value of type FreeF t a consists of a type r, a value x :: t r and a function f :: r → a. We're recording which function r → a we'd like to apply to x via functorial lift at some point in the future, once we have a map from t to an actual functor.

On my way back home from teaching Agda in Padova (course notes: https://agdapad.quasicoherent.io/~Padova2026/) Cozy and quiet, spending the night on the platform at one of my favorite train stations for sleepovers :-)

@MartinEscardo@mathstodon.xyz @jonmsterling@mathstodon.xyz Thank you for the warm welcome :-) I don't know yet whether I'll be active here but I'll give it a try.