For years, the Carnot CEA List, has been using tools that leverage formal methods to verify that there are no bugs in a program. These tools are very effective against conventional cyberattacks. However, they don’t work as well on side-channel attacks. These attacks take advantage of the physical phenomena that occur when a program is run, rather than vulnerabilities in the program itself, to extract information. Temporal attacks are designed to decode cryptographic keys by comparing the processing times for different operations on a computer, for example.
A technique called “constant time” coding can be used to fend off temporal attacks. The idea is to make sure that the execution time for a given task—such as the verification of a password—is not dependent upon the input data. Because this type of coding is so tricky, CEA List researchers developed REL, a tool that can automatically verify that code is “constant time.” The tool has been integrated into the BINSEC code analysis suite and came through tests on 338 cryptographic implementations with flying colors.
The advance, which was presented at the IEEE Symposium on Security & Privacy 2020, will pave the way toward new code analysis methods for other kinds of attacks and, more generally, better and more automated security for cryptographic programs.
Read article at http://www.cea-tech.fr/