Can't have a formal verification session without SMT #realworldcrypto

😹 #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

(oops) #realworldcrypto

The core of a SNARK is an interactive argument, usually with Fiat-Shamir slapped on top #realworldcrypto

Reductions can compose: #realworldcrypto

HYPERCUBE #realworldcrypto

neato #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

😹 #realworldcrypto

lmao #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

ML-DSA is dominated by SHA-3 and SHAKE operations #realworldcrypto

Faster than non-PQ options for most operations! #realworldcrypto

'We can do better' #realworldcrypto

🐰 #realworldcrypto