> 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 (again, for some odd reason).
Yes and no.
No: There are lots of very hard open problems which are judged to be of little value by mathematicians and hence garner little attention.
Yes: If a conjecture resists proof for a long time, this can indicate that we still have a substantial gap in our understanding. We project utility into an eventual closure of this gap, not into the statement of the concrete conjecture at hand. The gain in understanding is what we actually work for. It just turns out that chasing specific results, even if they are mostly dead ends on their own, is useful for orientation.
The (by now solved) problem by Fermat (for all integers a ≥ 1, b ≥ 1, c ≥ 1, n ≥ 3, the equation aⁿ + bⁿ = cⁿ does not hold) and the (still open) Collatz conjecture are perhaps good illustrations of this situation.
> 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 valuable ingredient in defending against evil maid attacks.
But another reason is... convenience. Resuming from RAM is faster than resuming from disk, especially so if your "disk" is actually just a USB flash drive. I know that it might be a bit weird to ask for convenience when the motivation is security. But I argue that there are use cases where the tradeoff is sound.
With hibernation, all your data is safe but the inconvenience might seduce you not to use it.
With suspend to RAM and your distro's version of cryptsetup-suspend (and the kernel patch or alternatively the cryptsetup workaround), only your volume key (and hence the bulk of your data, potentially terabytes worth of sensitive information) is safe, but sensitive data in memory (recent files, recent chat messages, session cookies, ...) is not. But on the other hand it's quick.
Some people use a combination: suspend to RAM for short breaks, where they expect to remain physically able to fully switch off the laptop when something happens; and suspend to disk for longer breaks.
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 thing correctly, and cryptsetup luksSuspend relied on cryptsetup luksOpen doing its thing correctly, and cryptsetup luksOpen relied on the thread keyring being purged from memory on process exit, which is promised in the tread-keyring(7) manpage.
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 put your LUKS headers elsewhere, separated from the disk) and perhaps disk and disk sector usage statistics.
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 the volume key to be safe during suspend anyway.
Debian's solution was ported to several (most?) other distributions and I guess quite a few people maintained private ports.
The thread-keyring(7) manpage promises: "A thread keyring is destroyed when the thread that refers to it terminates." For their key upload (from userspace to kernelspace) mechanism, the cryptsetup project relied on this property; but kernel 6.9 introduced a regression invalidating this property.
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: Cold Boot Attacks on Encryption Keys":
Other options: DMA attacks. Also you never know what the Intel Management Engine hidden in your computer is doing. It's running a version of Minix you don't have any control over, and it has full access to memory.
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 the passphrase if the volume key is still in memory, right?").
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 space, tracks this at the following issue:
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 remains.
A couple of years ago, three security researchers from the TU Munich implemented a prototype for also encrypting (most) parts of the memory just before suspend, to address this limitation; but as far as I know, it was not upstreamed or developed further: https://www.sec.in.tum.de/i20/publications/fridgelock-preven...
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) cryptsetup-suspend addon. This issues a luksSuspend command which is supposed to wipe the key from memory, and on resume asks you to resupply your passphrase.
Up to kernel 6.8, this worked as described; starting with kernel 6.9, it silently didn't.
It is a configuration language with general programming features, but it is decidedly _not_ Turing complete. It seems to sit at a sweet spot between "just JSON, no programming convenience at all" and "full-blown programming language with nontrivial toolchain".
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 till every item has been visited (in contrast to merely most items).
The keyword to look up more details is "coupon collector's problem".
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, the Bundesverfassungsgericht, learned of this case, the court immediately ordered their release and declared the original verdict void: According to the Bundesverfassungsgericht, (in the specific situation at hand) this phrase is more a value judgment and less a factual claim.
Together with a fellow activist, who also served as informal legal counsel, they gave a talk on this case at the 38th Chaos Communication Congress: https://www.youtube.com/watch?v=r5RmTOGucZo
Gwern shared an idea how to exploit the strength of current-generation LLMs, despite their weaknesses, for "create your own adventure"-style fiction. https://gwern.net/cyoa Having people vote on AI-generated potential continuations should yield better results and cut costs at the same time.
From the title I thought this was an implementation of Gwern's idea, but it's not.
Sorry, didn't intend to use so much jargon. By "quantifying over all formulas" I just meant that one has to distinguish between the following two statements:
1. The law of excluded middle holds for a particular formula p.
2. The law of excluded middle holds for _all_ formulas p.
Also note that "formula" just means "formal logical statement", i.e. structured string consisting of v, ==>, and so on.
What do you mean by "perspective of totality"?
Regarding your first edit: There is indeed a metatheorem which says "any classical proof can be turned into a constructive proof". The catch is that this does _not_ apply to all formulas (of course, else the discussion would be moot), but only to formulas of a special kind. Not many formulas are of this kind, but for instance "There exist infinitely many prime numbers" and "A particular Turing machine halts" are (when suitably formulated). If you want to lookup the details, look for "Friedman's Trick".
That the implication (~p ∨ p) ⇒ (¬¬p ⇔ p) holds is because there is a direct proof of this. I didn't show (here or in the slides) that the reverse implication is not intuitionistically valid. A simple way to do this would be to proceed along your lines, that is construct a Heyting algebra in which (¬¬p ⇔ p) holds for a particular element p but in which (~p v p) does not holds for this p. A fancier way would be to look at toposes arising "in nature", not specifically constructed for giving a counterexample.
Thanks for the book recommendation! I'll check it out. I won't have Internet over the weekend but I'd be glad to continue the discussion later.
Yes and no.
No: There are lots of very hard open problems which are judged to be of little value by mathematicians and hence garner little attention.
Yes: If a conjecture resists proof for a long time, this can indicate that we still have a substantial gap in our understanding. We project utility into an eventual closure of this gap, not into the statement of the concrete conjecture at hand. The gain in understanding is what we actually work for. It just turns out that chasing specific results, even if they are mostly dead ends on their own, is useful for orientation.
The (by now solved) problem by Fermat (for all integers a ≥ 1, b ≥ 1, c ≥ 1, n ≥ 3, the equation aⁿ + bⁿ = cⁿ does not hold) and the (still open) Collatz conjecture are perhaps good illustrations of this situation.