Clarification: this still has dependencies. For example, it requires one of "OpenSSL (versions 1.0.2, 1.1.1 and 3.0.x), LibreSSL, BoringSSL, AWS-LC, and the Apple Common Crypto framework to perform the underlying cryptographic operations"
S2N is great, clean, actively maintained, and even has experimental support for post-quantum key exchange (compatible with BoringSSL and the Zig standard library).
> But formal methods (and TLA+ for distributed computation) don't eliminate side channels.
True, but they eliminate whole classes of attack. I'm normally aghast at people writing new code in plain C, but formally verified plain C counts as a whole other and better paradigm to me.
There have been some attempts at formally verifying lack of timing attacks (to the extent allowed by hardware). This is the one I know the most about: https://dl.acm.org/doi/pdf/10.1145/3314221.3314605 but there are likely others
12 comments
[ 4.7 ms ] story [ 31.0 ms ] threadAWS-LC is the recommended option of the supported choices, there doesn't seem to be a "built-in" type choice.
Other very nice TLS implementations in C/C++:
- Facebook Fizz: https://github.com/facebookincubator/fizz
- PicoTLS: https://github.com/h2o/picotls
https://scholar.google.com/scholar?cites=2686812922904040715...
But formal methods (and TLA+ for distributed computation) don't eliminate side channels.
True, but they eliminate whole classes of attack. I'm normally aghast at people writing new code in plain C, but formally verified plain C counts as a whole other and better paradigm to me.
Why?
E. Prouff and M. Rivain, Masking against Side-Channel Attacks: A Formal Security Proof, EUROCRYPT 2013, LNCS 7881
S. Dziembowski and K. Pietrzak, "Leakage-Resilient Cryptography, 10.1109/FOCS.2008.56.
Time complexity > Constant time: https://en.wikipedia.org/wiki/Time_complexity#Constant_time
"Masking against side-channel attacks: A formal security proof" (2013) https://link.springer.com/chapter/10.1007/978-3-642-38348-9_... https://scholar.google.com/scholar?cites=1479355492097437276...
"Leakage-Resilient Cryptography" (2008) https://ieeexplore.ieee.org/abstract/document/4690963 https://scholar.google.com/scholar?cites=5581902451405085906...