[seL4] Re: Formally verified AES C code

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