On 18/07/2021 07:52, Hugo V.C. wrote:
Ha, ha... yes Gernot, you are absolutely right. Maybe I can just use both: first I can encrypt with HACL (https://github.com/project-everest/hacl-star)
If you want something beyond AES, then there's TweetNaCl, which is a small and portable implementation of the NaCl API. I subsequently re-implemented it all in SPARK, and it has a complete and automatic proof of type-safety, memory-safety and some correctness properties. It is also (claimed to be) free of timing side-channels. If you have a GCC with Ada enabled, then my code is at https://github.com/rod-chapman/SPARKNaCl (If you want to know how TweetNaCl actually works, then read my code, since it it littered with comments and assertions...my code is also much faster than TweetNaCl, especially on 32-bit targets) - Rod