IngoBlechschmid

7 ms·

1.
by IngoBlechschmid 8d ago
I agree! Martín Escardó never tires to say that he uses the Agda proof assistant in exactly this sense, as a kind of interactive blackboard for taking notes and structuring his thoughts. The vast TypeTopology repository is the result of yea
2.
by IngoBlechschmid 25d ago
The Curry-Howard correspondence. 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
3.
by IngoBlechschmid 2mo ago
> 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: Of course there is a nontrivial learning curve, but the
4.
by IngoBlechschmid 2mo ago
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 addition to quality reasons). The proof assistant Agda was ev
5.
by IngoBlechschmid 2mo ago
> 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: Th
6.
by IngoBlechschmid 3mo ago
It's kinda both, right? In any case, good clarification, thank you.
7.
by IngoBlechschmid 3mo ago
> 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.
8.
by IngoBlechschmid 3mo ago
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 cryptse
9.
by IngoBlechschmid 3mo ago
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
10.
by IngoBlechschmid 3mo ago
> 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...
11.
by IngoBlechschmid 3mo ago
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.
12.
by IngoBlechschmid 3mo ago
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": https:&#x
13.
by IngoBlechschmid 3mo ago
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
14.
by IngoBlechschmid 3mo ago
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 refactoring which introduced this bug: https://githu
15.
by IngoBlechschmid 3mo ago
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: http
16.
by IngoBlechschmid 3mo ago
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, but for the benefit of others: 38C3 - Windows BitLocker: Scr
17.
by IngoBlechschmid 3mo ago
Oh, which one is it? (You don't mean BitLocker, right?)
18.
by IngoBlechschmid 3mo ago
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 t
19.
by IngoBlechschmid 3mo ago
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 whic
20.
Since Linux 6.9, LUKS suspend stopped wiping disk-encryption keys from memory(mathstodon.xyz)
539 points by IngoBlechschmid 3mo ago|226 comments
21.
by IngoBlechschmid 10mo ago
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. It seems to sit at a sweet spot between &quo
22.
by IngoBlechschmid 10mo ago
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
23.
by IngoBlechschmid 11mo ago
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
24.
by IngoBlechschmid 1y ago
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 question: What the parent poster referred to
25.
by IngoBlechschmid 1y ago
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.
26.
by IngoBlechschmid 1y ago
The paper was originally released in April 2023, it just got version-bumped a couple months ago :-)
27.
by IngoBlechschmid 1y 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 again. There is no paradox: Externally, there is an enumerati
28.
by IngoBlechschmid 1y ago
This set of slides, originally devised for the Chaos Communication Congress, might be helpful: https://www.speicherleck.de/iblech/stuff/ac-38c3.pdf - Precise statement of the axiom - Overview of its consequences -
29.
by IngoBlechschmid 1y ago
I like Vim's digraphs, which go in a similar direction. For instance, Ctrl-K = > gives ⇒, Ctrl-K a * gives α. An overview of available digraphs is available at :digraphs. Otherwise I like the Agda input method of Emacs, where \to gi
30.
by IngoBlechschmid 1y ago
I'm currently creating an interactive tutorial on Agda, with lots of embedded exercises (running purely in the browser/on a server, no installation required), perhaps it is useful to some: https://lets-play-agda.quasico

More ›