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.

当软件实现的物理效果依赖于诸如加密密钥之类的秘密数据时，该软件实现显示旁通道泄漏。相关的物理影响包括指令执行时间、内存访问时间、功耗和电磁辐射。在首次演示差分功耗分析15年后，侧通道攻击正在影响各种处理器中的软件实现。然而，如果没有自动化工具的支持，程序员仍然不得不求助于手动且容易出错的对策插入。这是有问题的，因为侧通道泄漏是一种很难从源代码中推断或预测的实现效果。该项目将创建自动软件工具，可以帮助软件开发人员快速、正确地合成和验证抗旁路软件。本项目将开发的软件代码自动转换技术将以开源编译器的形式发布，从而将结果带给更大的社区。本项目将开发设计自动化技术，以系统地消除侧通道泄漏对秘密数据的依赖。建议的对策将基于归纳综合和形式验证，并将作为对软件代码的编译器驱动的转换进行集成。旁信道泄漏的估计将通过一个参数化的处理器体系结构模型来指导。这将确保抗旁路代码可以跨不同的架构目标进行移植。与现有的对策设计相比，该方法具有通用性和应用无关性；它可以由非专业程序员使用；它通过形式化的分析技术提供逐结构的正确保证。安全的交叉性带来了对汽车、工业、医疗保健或智能电网等广泛应用领域的旁路抗设计的需求。来自这些领域的开发人员需要工具来帮助他们快速构建正确和安全的软件，而不必处理抗侧沟设计的陷阱。自动插入侧通道对策将满足这一需求，并导致更便宜和更安全的产品。该项目的研究成果包括一个开源的、可扩展的编译器，以及一个验证使用该编译器生成的抗旁路代码的硬件演示平台。这些构件使正式方法和编译器社区能够研究新的对策技术，并帮助密码工程社区创建基准测试套件来验证这些对策。私人投资机构将在各自的社区中宣传这一潜力，方法是举办暑期学校，教授他们的研究成果。PIS还将开发一门研究生课程，将嵌入式系统设计专业的学生与编译器设计专业的学生进行合作。