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 <ger...@unsw.edu.au> escribió: > On 18 Jul 2021, at 07:00, Hugo V.C. <skydive...@gmail.com> wrote: > > > > This sounds even better... Thanks Alex. > > > > El sáb., 17 jul. 2021 22:57, Axel Heider <axelhei...@gmx.de> 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 > _______________________________________________ Devel mailing list -- devel@sel4.systems To unsubscribe send an email to devel-leave@sel4.systems
