Hi Rod, this really looks interesting... I'll give it a try, but I will not read the code myself as I really have not the skills to do it. I'm not developer, and also never saw SPARK before. I'm just building a prototype so as long it works and it is reasonably secure it may work for me. Anyway, honestly, I was looking for just a C AES implementation without any more features but your work looks so nice so, as said, I'll give it a try. Let's see if I can cross compile your project as static Linux aarch64 binaries...
Thank you! El lun., 19 jul. 2021 11:08, Roderick Chapman <[email protected]> escribió: > 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 > > > > _______________________________________________ > Devel mailing list -- [email protected] > To unsubscribe send an email to [email protected] > _______________________________________________ Devel mailing list -- [email protected] To unsubscribe send an email to [email protected]
