TWC: Small: Secure by Construction: An Automated Approach to Comprehensive Side Channel Resistance

TWC：小型：通过构造实现安全：综合侧通道阻力的自动化方法

• 批准号: 1617203
• 负责人: Patrick Schaumont
• 金额: $ 50万
• 依托单位: Virginia Polytechnic Institute and State University
• 依托单位国家: 美国
• 项目类别: Standard Grant
• 财政年份: 2016
• 资助国家: 美国
• 起止时间: 2016-09-01 至 2020-08-31
• 项目状态: 已结题
• 来源: https://www.nsf.gov/awardsearch/showAward?AWD_ID=1617203&HistoricalAwards=false
• 关键词: TWC; Small; Secure; Construction; Automated

A software implementation shows side-channel leakage when the physical effects of its implementation have a dependency to secret data such as cryptographic keys. Relevant physical effects include instruction execution time, memory access time, power consumption and electromagnetic radiation. Fifteen years after differential power analysis was first demonstrated, side-channel attacks are affecting software implementations in a broad variety of processors. Yet, without the support of automatic tools, programmers still have to resort to manual and error-prone insertion of countermeasures. This is problematic because side-channel leakage is an implementation effect that is difficult to infer or predict from source code. This project will create automatic software tools that can help software developers synthesize and verify side-channel resistant software, quickly and correctly. The automatic software code transformation techniques to be developed in this project will be released as an open-source compiler, thereby bringing the results in reach of a larger community.This project will develop design automation techniques to systematically remove the dependency of side channel leakage to secret data. The proposed countermeasures will be based on inductive synthesis and formal verification, and they will be integrated as compiler-driven transformations on the software code. The estimation of side-channel leakage will be guided through a parameterized processor architecture model. This will ensure that the side-channel resistant code is portable across different architecture targets. Compared to existing countermeasure designs, the proposed approach is generic and application independent; it can be used by non-specialist programmers; and it offers correct-by-construction guarantees through formal analysis techniques.The cross-cutting nature of security brings a need for side-channel resistant design to a wide variety of application domains including automotive, industrial, health-care, or smart-grid. Developers from these fields need tools to help them to quickly build correct and secure software without having to deal with the pitfalls of side-channel resistant design. Automatic insertion of side-channel countermeasures will address this need and lead to cheaper and more secure products. The research outcomes of this project include an open-source, extensible compiler, and a hardware demonstration platform to validate the side-channel resistant code generated using the compiler. These artifacts enable the formal methods and compiler community to investigate new countermeasure techniques, and they help the cryptographic engineering community to create a benchmark suite to validate these countermeasures. The PIs will advertise this potential in their respective communities by developing a summer school to teach the outcomes of their research. The PIs will also develop a graduate course that teams up students in embedded system design with students in compiler design.

当其实现的物理效应依赖秘密数据（例如加密密钥）时，软件实现将显示侧向通道泄漏。相关的物理效果包括指令执行时间，内存访问时间，功耗和电磁辐射。首次证明差异功率分析的十五年后，侧通道攻击会影响各种处理器的软件实现。但是，没有自动工具的支持，程序员仍然必须诉诸于手动和错误的对策插入。这是有问题的，因为侧通道泄漏是一种实现效果，很难从源代码中推断或预测。该项目将创建自动软件工具，可以帮助软件开发人员快速，正确地合成和验证侧通道抗渠道的软件。本项目中要开发的自动软件代码转换技术将作为开源编译器发布，从而使结果达到了一个较大的社区。此项目将开发设计自动化技术，以系统地消除侧通道泄漏对秘密数据的依赖性。所提出的对策将基于归纳合成和正式验证，并将它们作为编译器驱动的软件代码转换集成。侧通道泄漏的估计将通过参数化处理器架构模型进行指导。这将确保侧通道抗性代码在不同的体系结构目标上可移植。与现有的对策设计相比，所提出的方法是通用和应用程序独立的；非专家程序员可以使用它；它通过正式的分析技术提供了正确的构造保证。安全性的性质为包括汽车，工业，卫生保健或智能网格在内的各种应用程序领域提供了抵抗侧向通道的设计。这些领域的开发人员需要工具来帮助他们快速构建正确和安全的软件，而无需处理侧通道设计的陷阱。自动插入侧通道对策将满足这一需求，并导致更便宜，更安全的产品。该项目的研究成果包括开源，可扩展的编译器和硬件演示平台，以验证使用编译器生成的侧通道抵抗代码。这些文物使形式的方法和编译器社区能够调查新的对策技术，并帮助加密工程社区创建一个基准套件来验证这些对策。 PI将通过开发一所暑期学校来教授他们的研究结果，在各自社区中宣传这一潜力。 PI还将开发一门研究生课程，与学生设计的学生组合嵌入式系统设计。