[master] automatic insertion of countermeasures in a verified compiler

Counter-measures against hardware control-flow attacks, speculative execution attacks, or side channel attacks are notoriously difficult to insert at the source level. The topic of this internship is to inject them at compile-time.

Countermeasures to various attacks can be introduced into programs, but this is cumbersome to do manually and furthermore some may be removed by the compiled. It seems a good idea to add such countermeasures at compile time. Yet, this must not disturb the normal execution of programs.

CompCert is a formally verified compiler. Adding countermeasures directly inside CompCert involves formally proving that these countermeasures do not alter the normal execution of the program.

See also this related proposal


Contact | Site Map | Site powered by SPIP 3.1.15 + AHUNTSIC [CC License]

info visites 1803416