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的法定任务，并被认为是通过基金会的知识分子优点和更广泛的审查标准来通过评估来获得的支持。