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.
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.