Rendered at 10:37:39 GMT+0000 (Coordinated Universal Time) with Cloudflare Workers.
AlotOfReading 9 hours ago [-]
SAW/Cryptol are amazingly easy to use compared to other formal methods tools. It's a shame that C++ is still popular in high assurance spaces, because the tooling for it and the ability to write safe code is so much worse than C these days.
pjmlp 3 hours ago [-]
When did C got safe strings and arrays?
Ideally neither C nor C++ should be used when security matters.
FabHK 6 hours ago [-]
Had totally forgotten that Apple had rolled out post-quantum crypto (ML-KEM and ML-DSA, FIPS 203 and FIPS 204, respectively) already back in 2024. [1]
Slightly off topic, but it's great to see "crypto" to mean cryptography, helping users to keep their data secure, and not as so often these days those silly cryptocurrency crime tokens.
The missing-step bug in early ML-DSA is the perfect case for SAW. rare inputs that pass code review because the line that should be there doesn't look absent, it looks like the next line is correct. tests wouldn't catch it unless someone happened to roll exactly the right inputs.
FiloSottile 3 minutes ago [-]
I would really like to look at the bug and whether we could have caught it with conventional testing, but it doesn't look like Apple actually disclosed it?
throwaway85825 7 hours ago [-]
Verified crypto is important but apple still doesnt take parser security seriously enough. They know it's insecure and offer lockdown mode instead of fixing it.
Ideally neither C nor C++ should be used when security matters.
Slightly off topic, but it's great to see "crypto" to mean cryptography, helping users to keep their data secure, and not as so often these days those silly cryptocurrency crime tokens.
[1] https://security.apple.com/blog/imessage-pq3/