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

在密码学领域，侧信道是指可以通过预期输出以外的方式从密码系统中获得的任何信息。在加密算法执行过程中，由于系统功耗随处理的保密数据不同而变化，会产生功率和电磁侧信道漏洞，可能会在不经意间泄露敏感信息。恒功率技术用于防止敏感信息通过功率侧通道泄漏。然而，即使对密码学专家来说，编写这样的代码也是一项挑战。为此，该项目有助于推动开发无功率和电磁侧信道代码的最新技术。该项目的新颖之处在于，它开发了自动化的方法来帮助软件编写人员，包括非专家，在他们的代码中找到电源和电磁侧信道漏洞的潜在位置。此外，该研究还开发了在代码中发现潜在问题后修复代码的方法。该项目更广泛的意义和重要性在于设计和实现保护关键用户数据和代码免受可能用于泄露有价值或私人数据的侧信道攻击的方法和框架。该项目创建了将动态分析与符号分析技术相结合的方法和工具，以识别软件代码中最脆弱的位置。动态分析技术包括动态污染跟踪和随机测试，而符号分析技术包括关系或微分符号执行、可满足性和优化模理论以及模型计数。该项目开发的工具和算法利用了Hamming权重和距离泄漏模型。这些模型依赖于这样一个事实，即在处理敏感数据时，系统的功耗取决于寄存器的位翻转。因此，这些方法开发了新的寄存器分析技术，使用动态和符号执行低级代码，如二进制或中间表示。在符号分析中，该方法在每个保存与正在处理的敏感数据相关的值的中间变量或寄存器中派生出这种现象的形式化表示。此外，该项目开发了使用语法指导的合成方法修复易受攻击的代码位置的新方法。它还依赖于汉明权重泄漏模型和代码的符号分析，以及对实际硬件的测试向量泄漏评估来接受或拒绝候选修复。该奖项反映了美国国家科学基金会的法定使命，并通过使用基金会的知识价值和更广泛的影响审查标准进行评估，被认为值得支持。

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.