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.
TWC: Small: Secure by Construction: An Automated Approach to Comprehensive Side Channel Resistance