Side-Channel Analysis of Lean4

Stream: lean4

[Stone Olguin]

Hi, all!
So I've been working towards my Master's thesis, which involves preforming power-based side-channel analysis on the C-code that is generated from Lean4. I've been able to play around with the C-code and get it to work in other files fine using the leanc compiler just fine; however, the platform I will be using for the side-channel analysis (the ChipWhisperer) utilizes the arm-none-eabi-gcc compiler.
I've noticed that the object files generated from leanc and the object files that are generated using arm-none-eabi-gcc are incompatible, and I was wondering if anyone has any experience with trying to use other compilers for the generated C-code from Lean4? Or perhaps, has anyone else done any side-channel analysis of Lean4? If there is any additional information that I need to provide to help, let me know, Thanks!

[Mac Malone]

@Stone Olguin Lean uses a custom built clang compiler to build Lean on supported platforms. Thus, getting Lean to work on other platforms / compilers can take significant effort. Namely, I suspect you would need a custom build of Lean for arm-none-eabi-gcc and that such a build would be non-trivial to get functioning. @Sebastian Ullrich or @Henrik Böving could likely provide great detail on whether this is feasible and how to accomplish it given their greater familiarity with Lean's compiler configuration.

[Henrik Böving]

First things first leanc is a clang wrapper so that is already a significant difference to your setup. Furthermore the Lean run time does very much rely on being in a UNIX or Windows like environment right now, for example if you print the linker flags of leanc with leanc --print-ldflags you'll see:

-I /home/nix/.elan/toolchains/leanprover--lean4---nightly/include -fstack-clash-protection -fPIC -fvisibility=hidden -L /home/nix/.elan/toolchains/leanprover--lean4---nightly/lib/lean -Wl,--start-group -lleancpp -lLean -Wl,--end-group -Wl,--start-group -lInit -lleanrt -Wl,--end-group -Wl,-Bstatic -lc++ -lc++abi -Wl,-Bdynamic -Wl,--as-needed -lgmp -Wl,--no-as-needed -lm -ldl -pthread

It relies on things like pthread which are definitely not part of a bare metal environment that you usually get when you use arm-non-eabi so I am rather certain there is a lot of linker hell ahead of you.

If you actually want to go through with this you probably want to start by getting builds of our runtime compiling (and more interestingly linking) with arm-non-eabi-gcc before you even think about writing a proper lean program that does anything. Once you venture into trying to do things like IO etc. you will also very likely be bitten by the fact that Lean very much expects an OS present for things like printing text etc. and this dependency is also not trivial to remove.

And as a more general comment: I do think the idea is very cool but as a time boxed and graded project I would be very scared of going through with this as it is rather uncertain how much work you have to put in to even get any basic Lean program going on your target.

[Henrik Böving]

I'm actually doing a project that runs a programming language on a platform that is not used to it as well for my BsC (namely a rust driver on L4.Fiaso) and I've already had at least 4 roadblocks where if I didn't have access to the people at my workplace that know L4 by heart I would've been screwed completely with my project so eh...for your own good you better want to try this only if you have people that know this type of stuff or you know it yourself. (maybe I am just too traumatized tho who knows :D)

[Stone Olguin]

Alright, seems like it will be quite a task, maybe I'll find a different avenue! Thank you both for responding!
I'd still like to pursue this in some way, so I might work on it a bit more, since I still have a bit of time to work on this project. Would cross-compiling to arm from clang be viable with lean4's C-code? I know that clang can do cross-compilation. I utilize object files in the ChipWhisperer, so possibly cross-compiling to arm when calling leanc to generate the intermediate representation .o files could be used.
I also have a smaller project I made previously that allows me to run the Chipwhisperer using Embedded Rust, so that's another option I guess, but I'll update if that's the path I go!

[Mac Malone]

@Henrik Böving Do you think @Stone Olguin could build yours and @Siddharth Bhat's LLVM backend and use that to cross-compile the Lean program for the platform? Conceivably, as long as core Lean runtime can be be built for the platform and the program being written does not use any OS dependent primitives, then that could work?

[Henrik Böving]

Ysa that could work but the lean runtime will definitely need modifications. For example lean does always start up the task scheduler when it comes up which in turn expects a pthread (or windows equiv) to be around. But I think if you can get past the runtime hurdle it js doable.

[Sebastian Ullrich]

Stone Olguin said:

Would cross-compiling to arm from clang be viable with lean4's C-code?

Not only viable, all our ARM releases are already produced that way.