I feel this is going to be the thing which really boosts automated theory proving.
Up until now it's always been a hard sell, people say "Well, I can prove it myself, and that's less work than getting the computer to prove it", and they weren't completely wrong.
However, now we have LLMs which can do lots of interesting work, but really can't be trusted for anything important (like an LLVM optimisation pass, for example). If those LLMs can convince a theorem prover the LLVM optimisation pass is correct, then suddenly their output is much more useful.
One concern here is that proofs don't necessarily prove what we intuitively think they do. So we need to be very careful to understand what we actually proved.
The TLS 1.3 "Selfie attack" is an example of a gap between what we did prove and what we intuitively understood.
The formal proof for TLS 1.3 says Alice talking to Bob gets all the defined benefits of this protocol, and one option is they have a Pre-shared Key (PSK) for that conversation. They both know the same key, in that sense it's symmetric.
But the human intuition is that we're talking about an Alice+Bob key, whereas the proof says this is an Alice->Bob conversation key. If we re-use the same PSK for Bob->Alice conversations too we get the Selfie Attack, the formal proof never said we can expect that to work, it was just our intuition which confused us.
This piece starts out super-duper inside baseball (optimizing DER encoding for, in the main, X.509 certificate handling) in Rust code that is increasingly leveraged by Python's cryptography stack. But it ends up somewhere crazy: with an LLM agent apparently one-shotting an LLVM optimization, then semiformally verifying the change, which is ultimately merged by the LLVM team.
having two very different code paths for measuring the length of the DER buffer and writing the DER sounds very scary. i guess its fine with Rust but the idea would give me the heebee-jeebies for any other language unless they are using a safe buffer implementation. i would find it hard to trust that there is no buffer overflow based on divergent behaviour between the two functions.
The most interesting part of this post is the bit about half way down, where Alex uses Claude to help identify a missing compiler optimization in LLVM... and then uses Claude Code to implement that optimization and gets a PR accepted to LLVM itself! https://github.com/llvm/llvm-project/pull/142869
> There’s only one encoding I choose to acknowledge, which is DER (the Distinguished Encoding Representation, it’s got a monocle and tophat).
I also prefer to use DER, because it is better than BER and CER. DER is actually a subset of BER but BER has some messiness which is avoided by DER; because there are not as any ways to encode data by DER this makes it simpler to handle.
DER is also the format used by X.509 certificates, so this is fortunate; however, I use DER for other stuff too (since I think it is generally better than XML, JSON, CSV, etc).
I wrote a library in C to serialize and deserialize DER.
The post title is misleading and the content reads more like a guerilla advertisement for claude. TL;DR: author works for Anthropic, and used claude to implement an optimization for LLVM.
The author has added a note in the beginning of the post now making it clear that he works for Anthropic, which may explain the fixation on Claude Code!
He’s also well respected in the Python community for maintaining the cryptography package, partially written in Rust. This is just a random blog post, not an ad.
(as in it isn't one standard but a group of standards, like asn.1 without any encoding is split in ~4 standards by itself. Through to be fair all or CER, BER and DER are in the same standard. But PER is another standard, so is XER, OER, JER, GSER, RXER each and others.)
I feel this is going to be the thing which really boosts automated theory proving.
Up until now it's always been a hard sell, people say "Well, I can prove it myself, and that's less work than getting the computer to prove it", and they weren't completely wrong.
However, now we have LLMs which can do lots of interesting work, but really can't be trusted for anything important (like an LLVM optimisation pass, for example). If those LLMs can convince a theorem prover the LLVM optimisation pass is correct, then suddenly their output is much more useful.
One concern here is that proofs don't necessarily prove what we intuitively think they do. So we need to be very careful to understand what we actually proved.
The TLS 1.3 "Selfie attack" is an example of a gap between what we did prove and what we intuitively understood.
The formal proof for TLS 1.3 says Alice talking to Bob gets all the defined benefits of this protocol, and one option is they have a Pre-shared Key (PSK) for that conversation. They both know the same key, in that sense it's symmetric.
But the human intuition is that we're talking about an Alice+Bob key, whereas the proof says this is an Alice->Bob conversation key. If we re-use the same PSK for Bob->Alice conversations too we get the Selfie Attack, the formal proof never said we can expect that to work, it was just our intuition which confused us.
This piece starts out super-duper inside baseball (optimizing DER encoding for, in the main, X.509 certificate handling) in Rust code that is increasingly leveraged by Python's cryptography stack. But it ends up somewhere crazy: with an LLM agent apparently one-shotting an LLVM optimization, then semiformally verifying the change, which is ultimately merged by the LLVM team.
having two very different code paths for measuring the length of the DER buffer and writing the DER sounds very scary. i guess its fine with Rust but the idea would give me the heebee-jeebies for any other language unless they are using a safe buffer implementation. i would find it hard to trust that there is no buffer overflow based on divergent behaviour between the two functions.
The most interesting part of this post is the bit about half way down, where Alex uses Claude to help identify a missing compiler optimization in LLVM... and then uses Claude Code to implement that optimization and gets a PR accepted to LLVM itself! https://github.com/llvm/llvm-project/pull/142869
> There’s only one encoding I choose to acknowledge, which is DER (the Distinguished Encoding Representation, it’s got a monocle and tophat).
I also prefer to use DER, because it is better than BER and CER. DER is actually a subset of BER but BER has some messiness which is avoided by DER; because there are not as any ways to encode data by DER this makes it simpler to handle.
DER is also the format used by X.509 certificates, so this is fortunate; however, I use DER for other stuff too (since I think it is generally better than XML, JSON, CSV, etc).
I wrote a library in C to serialize and deserialize DER.
DER encoding is in fact unique.
The post title is misleading and the content reads more like a guerilla advertisement for claude. TL;DR: author works for Anthropic, and used claude to implement an optimization for LLVM.
The author has added a note in the beginning of the post now making it clear that he works for Anthropic, which may explain the fixation on Claude Code!
He’s also well respected in the Python community for maintaining the cryptography package, partially written in Rust. This is just a random blog post, not an ad.
Maybe. But the fact they work for Anthropic is very relevant and changes my impression of the post quite a lot.
FWIW Having worked a lot with Alex on cryptography he seems almost entirely incapable of doing something that I would normally consider an advert.
Sometimes people have good experiences with tools and like to share them.
So many encoding rules. DER, PER. It's an xkcd cartoon but inside one asn.1 standard!
it's as much one standard as OIDC is ;)
(as in it isn't one standard but a group of standards, like asn.1 without any encoding is split in ~4 standards by itself. Through to be fair all or CER, BER and DER are in the same standard. But PER is another standard, so is XER, OER, JER, GSER, RXER each and others.)