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
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 -- devel@sel4.systems To unsubscribe send an email to devel-leave@sel4.systems