SaTC: CORE: Small: Automatic Detection and Repair of Side Channel Vulnerabilities in Software Code

In the field of cryptography, a side-channel refers to any information that can be obtained from a cryptographic system through means other than the expected output. Power and electromagnetic side-channel vulnerabilities occur during the execution of the cryptographic algorithm when the power consumption of the system varies depending on the secret data being processed, which can inadvertently reveal sensitive information. Constant-power techniques are used to prevent the leakage of sensitive information through power side-channels. However, writing such code is challenging even for expert cryptographers. To this end, this project helps advance the state-of-the-art in developing code free of power and electromagnetic side channels. The project’s novelties are in that it develops automated methods to assist software writers, including non-experts, in finding potential locations of the power and electromagnetic side-channel vulnerabilities in their code. Additionally, the research develops methods to repair the code after a potential problem in the code has been identified. The project's broader significance and importance lie in the design and realization of methods and frameworks to protect critical user data and code from side-channel attacks that could be used to leak valuable or private data. The project creates methods and tools that combine dynamic analysis with symbolic analysis techniques to identify the most vulnerable locations in software code. Dynamic analysis techniques involve dynamic taint tracking and random testing, while symbolic analysis techniques include relational or differential symbolic execution, satisfiability and optimization modulo theories, and model counting. The tools and algorithms developed in the project leverage the Hamming weight and distance leakage models. These models rely on the fact that power consumption of the system varies depending on bit flips at registers while sensitive data is being processed. Therefore, the methods develop new register analysis techniques that use dynamic and symbolic execution of low-level code, such as binaries or intermediate representations. In symbolic analysis, the method derives a formal representation of this phenomenon at each intermediate variable or register that holds values related to sensitive data being processed. Additionally, this project develops new methods to repair vulnerable code locations using a syntax-guided synthesis approach. It also relies on the Hamming weight leakage model and symbolic analysis of code, as well as test-vector leakage assessment on real hardware to accept or reject candidate repairs. This award reflects NSF's statutory mission and has been deemed worthy of support through evaluation using the Foundation's intellectual merit and broader impacts review criteria.