Objective: The learning objective of this module is for trainees to gain hand experiences with property-based security verification. Trainees will learn how to generate properties by analyzing the hardware design and identifying security assets. Property-based security verification is a promising solution that can help protect SoC designs at the pre-silicon stage. A designer can formally describe the secure behavior of SoC and then using present formal tools, verify if a SoC design abides to the secure behavior. This draft introduces property-based security verification on an AES crypto module using Cadence’s JasperGold formal tool.
Target Audience: Government officers, Scientists
Prerequisite Knowledge and Skills:
- programming knowledge: Verilog HDL
- Cadence JasperGold
Resources Provided at the Training | Deliverables:
- Detailed description of set-ups used in training
- A video demo of the module
Learning Outcome: By the end of this course and experiment, trainees will learn how to perform for checking information leakage vulnerability for a basic AES implementation. This setup can be used for a variety of other targets, including implementation of other encryption cores (i.e., RSA, SHA, PRESENT etc.). Moreover, the trainees to understand how to develop security properties focusing on different threat models and to protect different assets. Then how to convert those properties into assertions and use industry standard verification tools to formally verify the assertions from security perspective.