Computer-Aided Verification of Physical Security Properties

• Applicant: Dr.-Ing. Pascal Sasdrich
• Subject Area: Security and Dependability, Operating-, Communication- and Distributed Systems ; Computer Architecture, Embedded and Massively Parallel Systems
• Term: since 2023
• Project identifier: Deutsche Forschungsgemeinschaft (DFG) - Project number 510964147

Protection of security-critical implementations against physical attacks, e.g., Side-Channel Analysis (SCA) or Fault Injection Analysis (FIA), is a labor-intensive, sophisticated, and error-prone task due to strong dependence on human factors. Consequently, computer-aided security verification of physically protected implementations can help developers reduce the impact of human factors and mitigate the asymmetry of effort, i.e., while proof of insecurity requires only a single counterexample, security proofs require certainty that there are no counterexamples. With powerful computer-aided security verification tools, the robustness and quality of future designs (in terms of physical security) is increased and security-oriented hardware development cycles are shortened and streamlined. The present project will advance the theoretical foundations and modeling procedures with respect to physical adversaries. In addition to practical instantiation of models and verification routines, advanced computer-aided security verification tools will be developed and investigated. The work program of this project is therefore particularly situated at the intersection of theory and practice in order to investigate research challenges in a coordinated manner from both perspectives. As advancements in security definitions and adversary models continue to drive the scope and perspective of security verification, the increasing complexity of advanced models and definitions is reduced through abstraction and investigation of advanced verification methods. Practical implementation then aids in the validation, evaluation, and application of the models and definitions to develop secure circuits and systems. Finally, the deep integration of efficient algorithms, data structures, and verification strategies into existing Electronic Design Automation (EDA) enables security-oriented development tools for the first time and also paves the way for further research, e.g., on security-aware synthesis and optimization. More specifically, current computer-aided security verification of physical security properties mostly implements rudimentary tools, focuses on proof-of-concept implementations, and only allows verification of micro-circuits. With the help of the project results, the next generation of computer-aided security verification tools will be integrated into modern security-oriented EDA flows and enable comprehensive security verification for the first time, e.g., for complete implementations of symmetric cryptography, advanced Post-Quantum Cryptography (PQC) accelerators, or complex RISC-V processor architectures.

• DFG Programme: Independent Junior Research Groups