Next up, 'Finding Bugs and Features Using Cryptographically-Informed Functional Testing', presented by Fernando Virdia eprint.iacr.org/2024/1122 #realworldcrypto

Finding Bugs and Features Usin...
Finding Bugs and Features Using Cryptographically-Informed Functional Testing

In 2018, Mouha et al. (IEEE Trans. Reliability, 2018) performed a post-mortem investigation of the correctness of reference implementations submitted to the SHA3 competition run by NIST, finding previously unidentified bugs in a significant portion of them, including two of the five finalists. Their innovative approach allowed them to identify the presence of such bugs in a black-box manner, by searching for counterexamples of expected cryptographic properties of the implementations under test. In this work, we extend their approach to key encapsulation mechanisms (KEMs) and digital signature schemes (DSSs). We perform our tests on multiple versions of the LibOQS collection of post-quantum schemes to capture implementations at different points of the recent Post-Quantum Cryptography Standardization Process run by NIST. We identify multiple bugs, ranging from software bugs (segmentation faults, memory overflows) to cryptographic bugs, such as ciphertext malleability in KEMs claiming IND-CCA security. We also observe various features of KEMs and DSSs that do not contradict any security guarantees but could appear counter-intuitive. Finally, we compare this methodology with a traditional fuzzing campaign against LibOQS and SUPERCOP, observing that traditional fuzzing harnesses appear less effective in surfacing software and logical bugs.

IACR Cryptology ePrint Archive
Checking if KEM implementations actually achieve IND-CCA in practice by mutating #realworldcrypto
'There is no obvious negative consequence, but it is also not intuitive.' #realworldcrypto
Cryptographically-informed testing #realworldcrypto
Finds bug classes not found by KATs and fuzzing #realworldcrypto
Next up, 'Formosa Crypto: End-to-end formally verified crypto software', presented by Santiago Arranz-Olmos and Ignacio Cuevas #realworldcrypto
Achieving end-to-end security for crypto software #realworldcrypto
Producing a high-assurance implementation of ML-KEM for use in Signal #realworldcrypto
Assembly-in-the-Head programming #realworldcrypto
Also looked at Signal's Contact Discovery Service #realworldcrypto
Found timing leakages in the previous impl #realworlcrypto
clang transformed the code, breaking the constant-time guarantees the source code had tried to achieve #realworldcrypto
Tying it all together #realworldcrypto
ʕ·͡ᴥ·ʔ #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
C90! 😭 Very portable #realworldcrypto
Front of house, back of house #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
There are still some gaps tho #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
I love this idea (SOUNDNESS.md) #realworldcrypto
Doing the same for ML-DSA! #realworldcrypto
Next up, 'Formally Verifying Circuits for Zero Knowledge Proofs', presented by Alex Ozdemir #realworldcrypto
Can't have a formal verification session without SMT #realworldcrypto
We really hate circuit bugs! #realworldcrypto
Next up, 'Compositional Formal Verification of SNARKs with ArkLib', presented by Quang Dao #realworldcrypto
Multiple zkSNARK verifiers in Ethereum #realworldcrypto
ArkLib: verified SNARKs in Lean #realworldcrypto
The core of a SNARK is an interactive argument, usually with Fiat-Shamir slapped on top #realworldcrypto
Reductions can compose: #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
i think we get a live demo 🤓 #realworldcrypto
Chocolate + coffee + Daniel = hardware attacks #realworldcrypto
The demo computer survived the TSA! #realworldcrypto
A scheme originally intended for disk encryption, not for RAM #realworldcrypto
aTtEsTaTiOn #realworldcrypto
"Please don't crash, please don't crash—" #realworldcrypto
It worked! #realworldcrypto
Attestation is...a bit of a fragile thing in practice #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