Roberto Giacobazzi, Faculty (visiting), IMDEA Software Institute
The talk concerns the design of code protecting transformations for white-box cryptography in a MATE (Man-At-The-End) attack scenario. The battle scenario involves attackers, modeled as approximate (abstract) interpreters of source programs intended to extract information about their run-time behavior, and protecting code transformations, modeled as distorted compilers devoted to inhibit attacks. Attacks are inhibited by maximizing imprecision (incompleteness) in all approximate computations made by the attacker. A brief overview on completeness in abstract interpretation (including recent achievements in POPL15) will set the theoretical background. The model is general enough to include generic static and dynamic attacks. Protecting transformations are systematically and formally derived as distorted compilers, by specializing a distorted interpreter for the programming language with respect to the source code to protect. Interestingly this distortion corresponds precisely to defeat the potency of the expected attacker, which consists in its ability to extract a complete and precise view of program’s execution.