For instance, in mathematics, we have A ⇒ A (every statement implies itself, for instance "if it rains, then it rains"); and analogously, in programming, we have the identity function of type A → A (which reads a value as input and outputs the same value).

This is the tip of an enormous iceberg identifying, in a certain precise sense, proving with programming (and stating mathematical assertions with specifying the desired behavior of a program).

However, programming is a bit more general than proving: Circular proofs are simply of no value, whereas looping programs can still be valuable. For instance, I for sure hope that the main loop of the browser I'm currently using to fill out this textbox does not prematurely stop.

I would object to the first part: Of course there is a nontrivial learning curve, but then I'd argue that non-slop Lean/Agda/Rocq/... formalizations are amazing for understanding proofs. A good formalization presents the outline and the key arguments in nicely structured form, and then, unlike pen-and-paper proofs, also allow you to get the details on every single step, exactly to your desired level of depth.

The proofs in Martín Escardó's TypeTopology Agda repository come immediately to my mind as an example. [An interactive Agda tutorial is here: lets-play-agda.quasicoherent.io]

In contrast, LLM-generated formalizations can currently be extremely messy. They certify truth and can also contain interesting arguments, but substantial work is required to bring them into a shape that contributes to the actual goal of improving our understanding of the mathematical landscape.

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.

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.

It all depends on your threat model.

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.

I agree; or resurrecting FridgeLock: https://www.sec.in.tum.de/i20/publications/fridgelock-preven...

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.

https://www.usenix.org/legacy/event/sec08/tech/full_papers/h...

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.

It was also fun to write, and enabled git-bisecting to isolate the specific kernel refactoring which introduced this bug: https://github.com/NixOS/nixpkgs/pull/532499

https://github.com/QubesOS/qubes-issues/issues/2890

But I would never trust it a second, being proprietary and known for issues. You likely know that, but for the benefit of others:

38C3 - Windows BitLocker: Screwed without a Screwdriver https://media.ccc.de/v/38c3-windows-bitlocker-screwed-withou... https://www.youtube.com/watch?v=5eNtT2p12cM

(You don't mean BitLocker, right?)

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

Up to kernel 6.8, this worked as described; starting with kernel 6.9, it silently didn't.

Comments URL: https://news.ycombinator.com/item?id=48763035

Points: 539

# Comments: 226