Formally verified compilers guarantee the absence of correctness bugs introduced during the compilation, but do not deal with other type of bugs, such as security bugs. In our previous work, we addressed the challenge of turning CompCert, a formally verified compiler, into a formally verified secure compiler. The notion of security we focused on is the preservation of “cryptographic constant-time”, a popular side-channel protection against timing-based and cache-based attacks. However, proving that CompCert is secure with respect to this property first required to modify several parts of the compiler. This extended abstract will focus on the changes we made to the CompCert compiler.