Automated Security Verification
Automated Security Verification is an active research field within the Chair of Security Engineering, focusing on the development and application of automated techniques to ensure the security and integrity of hardware systems. Our tools employ a variety of methods from formal verification and model checking, including Binary Decision Diagrams (BDDs) and Multi-Terminal Binary Decision Diagrams (MTBDDs), to identify and mitigate vulnerabilities in hardware circuits against Side-Channel Analysis (SCA), Fault Injection Analysis (FIA), and Combined Analysis (CA).
Our pioneering work, SILVER - Statistical Independence and Leakage Verification, introduces a new framework to analyze and verify masked implementations against various security notions using different security models as references. This framework processes the resulting gate-level netlist of a hardware synthesis, relying on BDDs and the concept of statistical independence of probability distributions.
Building on this, our follow-up work, FIVER - Robust Verification of Countermeasures against Fault Injections, develops a fault verification framework to validate the security of countermeasures against fault-injection attacks designed for ICs. This framework operates at the netlist level, parsing the given digital circuit into a model based on VDDs and performing symbolic fault injections. This novel verification approach evaluates protected hardware designs against fault injections, offering new opportunities for comprehensive analyses under given fault models.
Ultimately, these efforts culminated in our work on VERICA - Verification of Combined Attacks, where we present the first automated verification framework capable of verifying the physical security properties of hardware circuits with respect to combined physical attacks.
Collectively, these works underscore the significant potential of automated security verification. We continue to advance research in this area, exploring new methodologies and applications to further enhance security and performance.
Security-Aware Tooling
One important research area at the Chair for Security Engineering is the design of security-aware tools for the design and exploration of cryptographic algorithms, both in software and hardware. Our tools have to fulfill multiple goals: the generated designs should be as efficient as possible with regard to area or latency. On the other hand, the designs also need to be protected against physical attacks such as Side-Channel Analysis (SCA) or Fault-Injection Analysis (FIA), which typically increases the required area and latency.
EASIMask is a work where we present a tool that is able to automatically protect a hardware design against SCA using masking. In multiple case studies, we demonstrate that our automatically masked designs are comparable to hand-crafted designs in terms of latency, area, and security.
Following up on this work, we developed HADES, a framework that puts an efficient Design Space Exploration (DSE) in the focus. Based on our concept of templates, an abstract and generic hardware component, HADES can explore many different design configurations, predict their performance, and generate the best-suited candidate regarding area or latency. Most notably, HADES also considers the cost of applying masking countermeasures against SCA and can generate masked designs.