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

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

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.