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

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