Viewing profile — IngoBlechschmid

> Of course Lean proofs are rarely a good way to understand proofs, but hopefully they can be used to generate more human understandable arguments. I would object to the first part…

Strongly depends on the subbubble of mathematics. In some parts of type theory / formal proofs for instance, there is a rather strong rejection of LLMs (for moral reasons in additi…

> If I defined some pointless construction and it turned out to be very difficult to prove, it would absolutely and automatically over time be considered a "high utility" problem (…

It's kinda both, right? In any case, good clarification, thank you.

> Can I ask one question? Why not use hibernation at that point? The sibling post by cyphar gives a good reason; while UEFI Secure Boot has its own share of issues, it can be a val…

No, it is indeed a kernel bug in the code path responsible for luksOpen. Debian (and the distributions which ported cryptsetup-suspend) relied on cryptsetup luksSuspend doing its t…

Yes, you are right: LUKS encryption protests your data at rest. An attacker which steals your disk can only gain little, like the information that you have used LUKS (unless you pu…

> So hibernating is really the only proper way to protect against cold boot. I agree; or resurrecting FridgeLock: https://www.sec.in.tum.de/i20/publications/fridgelock-preven...

Sorry, aimed for a technically precise title and didn't want to bait clicks. Yes, this does not affect people on stock configurations for the plain reason that they wouldn't expect…

Several options. One is you restart and boot from a live system where you are root, and then dump all memory. This is described in the paper with the witty title "Lest We Remember:…

Exactly. Cryptsetup wouldn't know about the extra copy of the volume key in kernel memory. Which is why, dramatically, it appeared secure ("surely I wouldn't be asked to resupply t…

Right! Which is why integration tests for these kinds of features are all the more important. It was also fun to write, and enabled git-bisecting to isolate the specific kernel ref…

Qubes OS, the Linux distribution aspiring to offer a reasonably secure operating system, pioneering a "every app runs in a virtual machine" approach in the Linux laptop/desktop spa…

Okay, yes, sure. It definitely is the most-used encryption software for Windows. But I would never trust it a second, being proprietary and known for issues. You likely know that, …

Oh, which one is it? (You don't mean BitLocker, right?)

Suspend to (encrypted) swap might be a good middle ground between you and grandparent. Suspend to memory will (at best) protect your LUKS volume key, but other sensitive data remai…

Yes, if you simply suspend your laptop on most stock Linux distributions, then everything including the master key is still kept in memory. But Debian pioneered the (optional) cryp…

An interesting example is the Dhall language: https://dhall-lang.org/ It is a configuration language with general programming features, but it is decidedly _not_ Turing complete. I…

Just a tiny addition: Yes, N log N is the average time, but the distribution is heavily long-tailed, the variance is quite high, so in many instances it might take quite some time …

A good friend of mine was recently sentenced to prison for publicly using this kind of phrase during a protest for climate justice. When Germany's equivalent of the Supreme Court, …

Somebody asked in a now-deleted comment: 'Right, and what does it mean in the context of "A monad is just a monoid in the category of endofunctors"?' Here is an answer to this ques…

Gwern has an interesting take on this: https://gwern.net/cyoa By pivoting to "choose your own adventure"-style games, multiple issues (quality, costs) might be resolved.

The paper was originally released in April 2023, it just got version-bumped a couple months ago :-)

Indeed, what you write is true from an external point of view; just note that within this flavor of constructive mathematics, the set of functions from N to Bool is uncountable aga…