Deirdre Connolly¹ ²
The server can send Sealed Sender messages on behalf of anyone without detection (but the system is supposed to be secure in the setting that the server is insecure!)
#realworldcrypto
Existing Sealed Sender doesn't authenticate messages 😭
#realworldcrypto
'Boring' stuff matters: open source, documentation!!!, communication with community
#realworldcrypto
Ensure that cryptographic logic is _unified_ in a single native library [Is this possible in practice? Sounds less performant]
#realworldcrypto
Break time!
#realworldcrypto
Next up, the Levchin Prize!
#realworldcrypto
This is The Paper:
ee.stanford.edu/~hellman/pub...
#realworldcrypto
ee.stanford.edu/~hellman/publi...
ee.stanford.edu/~hellman/publi...
@cascremers.bsky.social gracefully accepts
#realworldcrypto
@cascremers.bsky.social gives the Levchin Prize invited talk on Tamarin
#realworldcrypto
Tamarin is a constraint solver impersonating a theorem prover
#realworldcrypto
Undecidable problem— we can't be sure it will ever terminate
#realworldcrypto
Much more precise handling of cryptographic primitives, including those that are motivated by the symbolic modeling of protocols
#realworldcrypto
If Tamarin terminates, there is always either an attack or a proof of security (if it doesn't terminate, oop)
#realworldcrypto
Can find complex attacks that humans will probably never find on their own
#realworldcrypto
Find attacks not by programming in the attacks, but by modeling the protocol, the security notions, the state transitions, and seeing what shakes out
#realworldcrypto
New version of Tamarin out, and there's a new book!
#realworldcrypto
Starting up a Tamarin Foundation!
#realworldcrypto
Don't want to be married to any particular methodology, but do want to learn from the other methodologies
#realworldcrypto
Struggled in the UC framework whether I've correctly modeled the attacker correctly
#realworldcrypto
Q: Insights on investing on web ui, what helps users?
A: Being stubborn; thinking more about making something that people can use; open source projects are fragile
#realworldcrypto
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 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.
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
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