Ingo Blechschmidt

@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

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 :-)

@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)

@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.

@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 :-)

@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.

@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!

@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)

@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.

@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 :-)

@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.