[seL4] Re: Formally verified AES C code

Hi Roderick, here (https://github.com/rod-chapman/SPARKNaCl#why-bother) in the "Known weaknesses and TBD items" I can read: - API/wrapper for calling SPARKNaCl from C. Does it mean that currently I can only use this library from a Spark program? Is not this scares me as I only need to encrypt/decrypt in a very simple way so I can try lo learn the basics of Spark to just do the job, but just want to be sure I have understood correctly what I have in my hands. So, no way to import the library in a C program? Thanks! El lun, 19 jul 2021 a las 20:06, Hugo V.C. () escribió:

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