Deirdre Connolly¹ ²Next up, 'Formosa Crypto: End-to-end formally verified crypto software', presented by Santiago Arranz-Olmos and Ignacio Cuevas
#realworldcrypto
Producing a high-assurance implementation of ML-KEM for use in Signal
#realworldcrypto
clang transformed the code, breaking the constant-time guarantees the source code had tried to achieve
#realworldcrypto
Q: Do you document the verification boundary of your toolchain with any formalism?
A: Difficult to achieve this; described in english in various papers
#realworldcrypto
Next up, 'mlkem-native: a unified, fast and verified ML-KEM library', presented by Hanno Becker
#realworldcrypto
As we saw constant-time guarantees can be difficult to ensure
#realworldcrypto
Proving all assembly is memory-safe using HOL Light; running proofs continuously in CI
#realworldcrypto
By ensuring type safety, ensure the correct modular reductions in the right places
#realworldcrypto
The models are hand-written, there could be a bug in there, try to address with extensive testing; but is it the 'best' level of abstraction?
#realworldcrypto
Doing the same for ML-DSA!
#realworldcrypto
Next up, 'Formally Verifying Circuits for Zero Knowledge Proofs', presented by Alex Ozdemir
#realworldcrypto
Next up, 'Compositional Formal Verification of SNARKs with ArkLib', presented by Quang Dao
#realworldcrypto
The core of a SNARK is an interactive argument, usually with Fiat-Shamir slapped on top
#realworldcrypto
large models are now pretty good at LEAN, this is helpful to arklib; the AI can prove faster than Quang!
#realworldcrypto
Q: Why are there so many Fiat-Shamir instantiation mistakes out there?
A: We lack to right tooling to auto catch these issues; must be secure in the spec first
#realworldcrypto
Next up, 'TEE.fail: Breaking Trusted Execution Environments via Memory Bus Interposition', presented by Christina Garman and Daniel Genkin
#realworldcrypto
A scheme originally intended for disk encryption, not for RAM
#realworldcrypto
"Please don't crash, please don't crash—"
#realworldcrypto
It worked!
#realworldcrypto
Protections were removed to improve performance at customer demand 😭
#realworldcrypto
Q: You believe these protections only got removed bc of performance?
A: Yes I do, we talked to the engineers, they were so upset and repeatedly saying "I told you so" etc
#realworldcrypto
Next up, 'Migrating a Silicon Root of Trust to Post-Quantum Crypto', presented by Jade Philipoom and Hien Pham
#realworldcrypto
Goal is to PQ secure boot chain
#realworldcrypto
