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 的法定使命，并通过使用基金会的智力优点和更广泛的影响审查标准进行评估，被认为值得支持。