[seL4] Re: Formally verified AES C code

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) which is a mature project very well tested, then I can encrypt with Leonards implementation wich should be functionally correct. That way I can minimize the first layer exposition to functional bugs (i.e., memory corruption ones) which are the ones that I'm more concerned as are the ones usually I can't easily fight. Crypto bugs are not my biggest concern in my solution as I can easily nest diffent crypto solutions. So in that security onion, I need the more external layer of crypto to be functionally correct more than crypto safe. Let me know your opinions on my approach. El dom., 18 jul. 2021 3:17, Gernot Heiser escribió:

On 18 Jul 2021, at 07:00, Hugo V.C. wrote:

...

This sounds even better... Thanks Alex.

El sáb., 17 jul. 2021 22:57, Axel Heider escribió:

...

Hugo,

last year Leonard Blazevic did his master thesis at Hensoldt Cyber about this, see

https://tumanager.ei.tum.de/service.php?token=lifecycle_sec_tueilnt&mode=pdfdownload&tId=330&language=en

...

...

I've put him in CC.

Just keep in mind that for crypto, while functional correctness is one (very strong) property, it isn’t the whole story. The other important parts are cryptographic safety (which for AES is well understood) and security from side-channel attacks, which depend on implementation choices and is much harder to prove.

Having a functional correctness proof of a well-understood crypto scheme is definitely something extremely desirable, I’m just trying to raise awareness to the limitations to avoid disappointment and reputational damage – just imagine the headlines “‘proved secure’ crypto code hacked”.

Gernot _______________________________________________ Devel mailing list -- devel@sel4.systems To unsubscribe send an email to devel-leave@sel4.systems