Add support for indirect branch tracking (IBT)

[didickman]

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.

[xavierleroy]

See #557 for a tentative implementation of IBT.

[didickman]

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!

[xavierleroy]

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 d5dcac4 . I'll restart #557 later.

[monniaux]

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

[didickman]

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.

[monniaux]

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