[1] |
AGRAWAL D , BAKTIR S , KARAKOYUNLU D ,et al. Trojan detection using IC fingerprinting[C]// IEEE Symposium on Security and Privacy (SP '07), 2007: 296-310.
|
[2] |
FLOTTES M , DUPUIS S , BA P ,et al. On the limitations of logic testing for detecting hardware Trojans Horsesv[C]// 10th International Conference on Design & Technology of Integrated Systems in Nanoscale Era (DTIS),Naples. 2015: 1-5.
|
[3] |
HELY D , MARTIN J , DARIO G ,et al. Experiences in side channel and testing based hardware Trojan detection[C]// IEEE 31st VLSI Test Symposium (VTS). 2013: 1-4.
|
[4] |
CLARKE E M , GRUMBERGO , PELED D ,et al. Model checking[M]. Cambridge: MIT press, 1999.
|
[5] |
BARTOLETTI M , DEGANO P , FERRARI G L ,et al. Model checking usage policies[C]// Trustworthy Global Computing. 2009: 19-35.
|
[6] |
ALESSANDRO C , EDMUND C , FAUSTO G ,et al. NUSMV:a new symbolic model checker[J]. STTT 2, 2000: 410-425
|
[7] |
MCMILLAN K L . Symbolic model checking:an approach to the state explosion problem[M]. Kluwer Academic, 1993.
|
[8] |
SZWED P , . Efficiency of formal verification of ArchiMate business processes with NuSMV model checker[C]// Federated Conference on Computer Science and Information Systems (FedCSIS),Lodz. 2015: 427-1436.
|
[9] |
XU N , MA Z , JIANG J ,et al. Model checking instance based on NuSMV[C]// IEEE SmartWorld,Ubiquitous Intelligence & Computing,Advanced & Trusted Computing,Scalable Computing &Communications,Cloud & Big Data Computing,Internet of People and Smart City Innovation (SmartWorld/SCALCOM/UIC/ATC/CBDCom/IOP/SCI). 2018: 2052-2056.
|
[10] |
SEBASTIANI R , ROVERI Marco , PISTORE M ,et al. NuSMV2:an open source tool for symbolic model checking[C]// International Conference on Computer Aided Verification. 2002.
|
[11] |
HASAN SR , KAMHOUA CA , KWIAT KA ,et al. Translating circuit behavior manifestations of hardware Trojans using model checkers into run-time Trojan detection monitors[C]// IEEE Asian Hardware-Oriented Security and Trust (AsianHOST). 2016: 1-6.
|
[12] |
DESAI K , STEVENS K.S , O'LEARY J ,et al. Symbolic verification of timed asynchronous hardware protocols[C]// IEEE Computer Society Annual Symposium on VLSI (ISVLSI). 2013: 47-152.
|
[13] |
PAKONEN A , BUZHINSKY I . Verification of fault tolerant safety I&C systems using model checking[C]// International Conference on Industrial Technology. 2019.
|
[14] |
BEHRMANN G , DAVID A , LARSEN K G . A Tutorial on UPPAAL[C]// Proc of Int school on Formal Methods for the Design of Computer Communication & Software Systems. 2004: 200-236.
|
[15] |
AAAMIR N , FAROOQUE A , AMJAD A ,et al. Comparison of model checking tools using timed automata - PRISM and UPPAAL[C]// IEEE International Conference on Computer and Communication Engineering Technology (CCET). 2018: 248-253.
|
[16] |
YAN X , LI Y , LI X . Real-time simulation of automotive systems based on UPPAAL[C]// Proceedings of 2017 IEEE 8th International Conference on Software Engineering and Service Science. 2017: 193-196.
|
[17] |
CHAUDHTY Y.A.K , HAMMED M . Formal verification of cloud based distributed System using UPPAAL[C]// International Conference on Innovation and Intelligence for Informatics,Computing,and Technologies (3ICT). 2019: 1-4.
|
[18] |
YAN X , WANG L , CHE X ,et al. Source code testing for automotive software based on UPPAAL model[C]// IEEE International Conference on Software Engineering & Service Science, 2014: 95-98.
|
[19] |
LI H , LIU Q , ZHANG J ,et al. A Survey of hardware Trojan detection,diagnosis and prevention[C]// IEEE International Conference on Computer-aided Design & Computer Graphics. 2016.
|
[20] |
HASAN S.R , KAMHOUA C.A , KWIAT K.A ,et al. A novel framework to introduce hardware Trojan monitors using model checking based counterexamples:inspired by game theory[C]// 2018 IEEE 61st International Midwest Symposium on Circuits and Systems (MWSCAS). 2018: 853-856.
|
[21] |
LODHI F K , ABBASI I H , KAMBOH A M ,et al. Formal verification of gate-level multiple side channel parameters to detect hardware Trojans[C]// Communications in Computer and Information Science. 2016.
|
[22] |
HAFEEZ A I , FAIQ K , OSMAN H ,et al. McSeVIC:a model checking based framework for security vulnerability analysis of integrated circuits[J]. IEEE Access, 2018,6: 1.
|
[23] |
RATHMAIR M , SCHUPFER F , KRIEG C . Applied formal methods for hardware Trojan detection[C]// IEEE International Symposium on Circuits & Systems. 2014: 169-172.
|
[24] |
ZHANG Y , YU L , LI H ,et al. Small Trojan testing using bounded model checking[C]// IEEE International Test Conference. 2018.
|
[25] |
ZHAO J F , . Case study:discovering hardware Trojans based on model checking[C]// The 8th International Conference. 2018: 64-68.
|
[26] |
KRIEG C , RATHMAIR M , SCHUPFER F . A process for the detection of design-level hardware Trojans using verification methods[C]// High Performance Computing & Communications,IEEE Intl Symp on Cyberspace Safety & Security,IEEE Intl Conf on Embedded Software & Syst. 2015.
|
[27] |
高洪博 . 指令诱发型硬件木马检测技术研究[D]. 郑州:信息工程大学, 2013.
|
|
GAO H B . Research on detection techniques of instruction-triggered hardware Trojan horse[D]. Zhengzhou:Information Engineering University, 2013.
|
[28] |
GAO H , LI Q , ZHU Y ,et al. Code-controlled hardware Trojan horse[C]// International Conference on Information Computing &Applications. 2012: 171-178.
|
[29] |
HE J J , GUO X , MEADE T ,et al. SoC interconnection protection through formal verification[J]. Integration, 2019,64: 143-151.
|
[30] |
RAJENDRAN J , DHANDAYUTHAPANY A M , VEDULA V ,et al. Formal security verification of third party intellectual property cores for information leakage[C]// IEEE International Conference on VLSI Design & International Conference on Embedded Systems. 2016: 547-552.
|
[31] |
CLARKE E M , KLIEBER W , MILO N ,et al. Model checking and the state explosion problem[J]. Lecture Notes in Computer Science, 2011: 1-30.
|
[32] |
CRUZ J , FARAHMANDI F , AHMED A ,et al. Hardware Trojan detection using ATPG and model checking[C]// International Conference on Vlsi Design & International Conference on Embedded Systems. 2018: 91-96.
|