Using gate-level side channel parameters for formally analyzing vulnerabilities in integrated circuits.

•A formal framework for vulnerability analysis of integrated circuits and Hardware Trojan (HT) detection is presented.•nuXmv model checker is used for gate-level circuit modeling, and validation of side channel parameters.•A novel vulnerability analysis algorithm based on a set of LTL properties is proposed to analyze behavior of circuits.•HT detection and behavior analysis are performed while considering the impact of process variations.