Thank you Matthew! Sounds good. El sáb., 17 jul. 2021 22:43, Matthew Fernandez escribió:

...

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

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.

Axel

-------- Original Message -------- From: Hugo V.C. [mailto:skydivebcn@gmail.com] Sent: Saturday, July 17, 2021, 10:16 PM To: devel Subject: [seL4] Formally verified AES C code

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?

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

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

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

On 20/07/2021 13:31, Hugo V.C. wrote:

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?

Yeah... it's directly callable from Ada (of which SPARK is a subset) right now. A C binding is reasonably easy, but you need to know Ada well to do it - see Annex B of the Ada RM for the details. That's assuming you're using the _same_ GCC compiler to compile both the C and SPARK components - if that's true, the compiler will do most of the work with sorting out the right parameter passing mechanisms and so on.  - Rod