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

SaTC：CORE：小型：自动检测和修复软件代码中的侧信道漏洞

• 批准号: 2245344
• 负责人: Jakub Szefer
• 金额: $ 60万
• 依托单位: Yale University
• 依托单位国家: 美国
• 项目类别: Continuing Grant
• 财政年份: 2023
• 资助国家: 美国
• 起止时间: 2023-07-01 至 2026-06-30
• 项目状态: 未结题
• 来源: https://www.nsf.gov/awardsearch/showAward?AWD_ID=2245344&HistoricalAwards=false
• 关键词: SaTC; CORE; Small; Automatic; Detection

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.

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