CompCert Add support for indirect branch tracking (IBT)

On newer Intel x86/64 CPUs and on OpenBSD, CompCert produced binaries will crash due to lack of IBT support. As a quick solution we can append “-z nobtcfi” to clinker_options in configure to disable IBT safeguards. However a preferable solution would be to add support for IBT on this platform. This can be partially solved by outputting “endbr64” after “.cfi_startproc” in backend/Printasmaux.ml. And then all that should be left is solving for jump tables. Thank you.

Jul 02 '25 13:07 didickman

See #557 for a tentative implementation of IBT.

Jul 28 '25 09:07 xavierleroy

Works nicely for me in my basic testing with an intel CPU that supports IBT. Responding to the note about x86/32 -- indeed OpenBSD does not implement IBT for legacy 32-bit x86 either. Only 64-bit systems have IBT/BTI. Would be great to merge this pull request when ready. Thanks!

Jul 28 '25 23:07 didickman

I'm late on the next release of CompCert and #557 is not as ready to be merged as I would like. As a temporary measure, I added -z nobtcfi to the linker options on x86 BSD, commit d5dcac406 . I'll restart #557 later.

Aug 29 '25 13:08 xavierleroy

@didickman Would what is done in Chamois suit your needs? https://gricad-gitlab.univ-grenoble-alpes.fr/certicompil/Chamois-CompCert

Sep 09 '25 10:09 monniaux

Extremely interesting project! Thanks for sharing! I will definitely take a look into this. In case of interest I am using CompCert on the industrial use side not for research.

Sep 09 '25 11:09 didickman

@didickman We support branch target protection and other countermeasures on AArch64 and x86(-64). Feel free to contact me (email) if interested.

Sep 09 '25 11:09 monniaux