This paper focuses on the security evaluation method of VLSI design front-end based on formal verification theory, which is adopted in the security check of a space Application Specific Integrated Circuit (ASIC).
The hardware security of space VLSI is an important issue of the reliable operation of spacecraft system in orbit. This paper focuses on the security evaluation method of VLSI design front-end based on formal verification theory. This method is adopted in the security check of a space Application Specific Integrated Circuit (ASIC). Using assertions of key registers, the potential design vulnerability of ASIC is found, which can lead to tampering of configuration data tampering under lock-in mode, and resulting in abnormal reset and even downtime of the whole chip. Finally, the security design improvement suggestions are given against the tampering.