12 ms·
PolarSSL has been validated with FRAMA-C by a company. Unfortunately you have to pay to see the results, and they use blinding for bignum arithmetic, not consta
by wbl 13y ago
PolarSSL has been validated with FRAMA-C by a company. Unfortunately you have to pay to see the results, and they use blinding for bignum arithmetic, not constant-time. (But they do have a decent curve implementation). http://trust-in-soft.com/news/ http://trust-in-soft.com/news/
To remove side channels and preserve validation, you need to be slightly clever. You validate that a C implementation of one of the functions does the same thing as a function in the validated package, then swap them in the build output. This can be done for miTLS. Your validation of the C part is much more limited in scope than the whole thing.
- wfn 13y ago> To remove side channels and preserve validation, you need to be slightly clever. You validate that a C implementation of one of the functions does the same thing as a function in the validated package, then swap them in the build output. This can be done for miTLS. Aha, this is interesting! Thanks for the link.