19 / 2017-11-08 09:57:00

Security Path Checking of a Circuit with Behavior Description

model checking,NuSMV,IP core,circuit verification

Model Checking is one of the formal tools that uses state space searching to automatically verify whether a finite state system meets the design specifications. IP core is widely used in circuit design. However, it still remains unknown that whether the critical security data would be modified or leaked through IP cores. In this paper, an innovative tool chain based on black box tint technique is proposed. We used tint based method to tint every input and output, which could verify security properties of every path in a circuit. NuSMV was selected as the model checker. Finally, the experiments suggested that the security path checking of a circuit can be easily verified by using this pattern.