[seL4] Re: Formally verified AES C code

On Jul 17, 2021, at 13:16, Hugo V.C. wrote:

Hi all,

I don't want to use SSL/openssl in a project I'm working. Thus, I want to just use my own encryption at the app layer. As performance is not a problem (just very small data packets over a socket) I would like to have the most simple implementation possible of AES, preferably, formally verified. Is anyone aware of any public AES encrytion implementation in C that has been formally or semi-formally verified?

HACL contains an AES-GCM implementation that can be compiled down to C: https://github.com/project-everest/hacl-star