llsoftsec
Compiler preserving constant-time property
Hello. I am currently reading the book and enjoying every bit of it. Thank you for this work. I have some feedback regarding some topics. I work closely in the area of providing software countermeasures against timing-based side-channel attacks. Regarding this line "At the moment, we do not know of a compiler implementation that actively helps to guarantee both (a) and (b)." in section 3.1. I have worked on Jasmin language and compiler that preserves the constant-time property. Even there is another well-known formally verified compiler called "CompCert" that preserves at least (a). (I am not sure about (b)). If given a chance, I am happy to elaborate on that section and add pointers to these works.
Papers: (1) https://members.loria.fr/VLaporte/files/CCS2021_StructuredLeakage.pdf (2) https://eprint.iacr.org/2022/630 (3) https://eprint.iacr.org/2019/926
![allcontributors[bot] avatar](https://avatars.githubusercontent.com/in/23186?v=4 "Published by a pub.dev verified publisher"){kind=small}