{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,31]],"date-time":"2026-01-31T10:29:16Z","timestamp":1769855356479,"version":"3.49.0"},"reference-count":42,"publisher":"Springer Science and Business Media LLC","issue":"1","license":[{"start":{"date-parts":[[2024,2,1]],"date-time":"2024-02-01T00:00:00Z","timestamp":1706745600000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2024,3,20]],"date-time":"2024-03-20T00:00:00Z","timestamp":1710892800000},"content-version":"vor","delay-in-days":48,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"funder":[{"DOI":"10.13039\/501100002352","name":"Ain Shams University","doi-asserted-by":"crossref","id":[{"id":"10.13039\/501100002352","id-type":"DOI","asserted-by":"crossref"}]}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["J Electron Test"],"published-print":{"date-parts":[[2024,2]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>In modern chip designs, shared resources are used extensively. Arbiters usage is crucial to settle conflicts when multiple requests compete for these shared resources. Making sure these arbiter circuits work correctly is vital not just for their proper functionality, but also for security reasons. The work in this paper introduces a method based on formal verification to thoroughly assess the proper functional aspects of various arbiter setups. This is achieved through SystemVerilog assertions and model checking. Additionally, we explore a non-invasive method for the modeling and insertion of different types of hardware Trojans. These Trojans, with their unique triggers and payloads, are modeled formally without the need for any alterations to the actual circuit. The results provide a detailed analysis of the cost involved in running the formal verification environment on versions of arbiters that are free from Trojans. This analysis is carried out using Questa PropCheck formal analysis tool, which offers valuable insights into the time and memory resources required. Furthermore, the results highlights how the formally modeled and inserted Trojans interfere with hold criteria of the arbiters\u2019 properties, where at least a single property fires due to the inserted Trojan. This work can be extended to be a generic approach with the potential to validate both the proper operation and security aspects of complex systems.<\/jats:p>","DOI":"10.1007\/s10836-024-06100-2","type":"journal-article","created":{"date-parts":[[2024,3,20]],"date-time":"2024-03-20T06:02:28Z","timestamp":1710914548000},"page":"117-135","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":3,"title":["Non-Invasive Hardware Trojans Modeling and Insertion: A Formal Verification Approach"],"prefix":"10.1007","volume":"40","author":[{"given":"Hala","family":"Ibrahim","sequence":"first","affiliation":[]},{"given":"Haytham","family":"Azmi","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0002-6033-733X","authenticated-orcid":false,"given":"M. Watheq","family":"El-Kharashi","sequence":"additional","affiliation":[]},{"given":"Mona","family":"Safar","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2024,3,20]]},"reference":[{"key":"6100_CR1","doi-asserted-by":"crossref","unstructured":"Al-Anwar A, Alkabani Y, El-Kharashi MW, Bedour H (2013) Hardware trojan protection for third party IPs. In: 2013 Euromicro Conference on Digital System Design. IEEE, pp 662\u2013665","DOI":"10.1109\/DSD.2013.133"},{"key":"6100_CR2","unstructured":"Alfke P,\u00a0\u00a0Xilinx (1998) Efficient shift registers,\u00a0LFSR counters, and long pseudo-random sequence generators.\u00a0https:\/\/docs.xilinx.com\/v\/u\/en-US\/xapp052. Accessed 1 Feb 2024"},{"key":"6100_CR3","doi-asserted-by":"publisher","first-page":"104407","DOI":"10.1109\/ACCESS.2020.2999544","volume":"8","author":"MW Anwar","year":"2020","unstructured":"Anwar MW, Rashid M, Azam F, Naeem A, Kashif M, Butt WH (2020) A unified model-based framework for the simplified execution of static and dynamic assertion-based verification. IEEE Access 8:104407\u2013104431","journal-title":"IEEE Access"},{"key":"6100_CR4","unstructured":"Auerbach G, Copty F, Paruthi V (2010) Formal verification of arbiters using property strengthening and underapproximations. In: Formal Methods in Computer Aided Design, pp 21\u201324. IEEE"},{"key":"6100_CR5","doi-asserted-by":"crossref","unstructured":"Bagga S, Gupta R, Jose J (2023) Modelling and analysis of confluence attack by hardware trojan in noc. In: Emerging Electronic Devices, Circuits and Systems: Select Proceedings of EEDCS Workshop Held in Conjunction with ISDCS 2022, pp 231\u2013246. Springer","DOI":"10.1007\/978-981-99-0055-8_19"},{"key":"6100_CR6","unstructured":"Becker DU (2012) Efficient Microarchitecture for Network-on-chip Routers. Stanford University"},{"issue":"4","key":"6100_CR7","doi-asserted-by":"publisher","first-page":"933","DOI":"10.1109\/TC.2021.3066466","volume":"71","author":"J Cheng","year":"2021","unstructured":"Cheng J, Fleming ST, Chen YT, Anderson J, Wickerson J, Constantinides GA (2021) Efficient memory arbitration in high-level synthesis from multi-threaded code. IEEE Trans Comput 71(4):933\u2013946","journal-title":"IEEE Trans Comput"},{"key":"6100_CR8","unstructured":"Cruz J, Gaikwad P, Nair A, Chakraborty P, Bhunia S (2022) Automatic hardware trojan insertion using machine learning. arXiv preprint arXiv:2204.08580.\u00a0https:\/\/arxiv.org\/abs\/2204.08580.\u00a0Accessed 1 Feb 2024"},{"key":"6100_CR9","volume-title":"Principles and Practices of Interconnection Networks","author":"WJ Dally","year":"2004","unstructured":"Dally WJ, Towles BP (2004) Principles and Practices of Interconnection Networks. Elsevier"},{"key":"6100_CR10","doi-asserted-by":"publisher","first-page":"237","DOI":"10.1007\/s41635-021-00122-4","volume":"5","author":"W Danesh","year":"2021","unstructured":"Danesh W, Banago J, Rahman M (2021) Turning the table: using bitstream reverse engineering to detect fpga trojans. J Hardw Syst Secur 5:237\u2013246","journal-title":"J Hardw Syst Secur"},{"key":"6100_CR11","doi-asserted-by":"crossref","unstructured":"Das S, Karfa C (2022) Formal modeling and verification of starvation freedom in nocs. In: Artificial Intelligence Driven Circuits and Systems: Select Proceedings of ISED 2021, pp. 101\u2013114. Springer","DOI":"10.1007\/978-981-16-6940-8_9"},{"key":"6100_CR12","unstructured":"EDA S (2023) Questa\u00aePropCheck. https:\/\/verificationacademy.com\/products\/questa-propcheck. Accessed\u00a01 Feb 2024"},{"key":"6100_CR13","doi-asserted-by":"publisher","first-page":"29","DOI":"10.1016\/j.micpro.2015.12.005","volume":"41","author":"H Elmiligi","year":"2016","unstructured":"Elmiligi H, Gebali F, El-Kharashi MW (2016) Multidimensional analysis of embedded systems security. Microprocess Microsyst 41:29\u201336","journal-title":"Microprocess Microsyst"},{"key":"6100_CR14","doi-asserted-by":"crossref","unstructured":"Golubcovs S, Mokhov A, Bystrov A, Sokolov D, Yakovlev A (2019) Generalised asynchronous arbiter. In: 2019 19th International Conference on Application of Concurrency to System Design (ACSD), pp 3\u201312. IEEE","DOI":"10.1109\/ACSD.2019.00005"},{"key":"6100_CR15","doi-asserted-by":"crossref","unstructured":"Guo X, Dutta RG, Jin Y, Farahmandi F, Mishra P (2015) Pre-silicon security verification and validation: A formal perspective. In: Proceedings of the 52nd Annual Design Automation Conference, pp 1\u20136","DOI":"10.1145\/2744769.2747939"},{"key":"6100_CR16","doi-asserted-by":"publisher","first-page":"225","DOI":"10.1007\/s41635-018-0042-5","volume":"2","author":"V Govindan","year":"2018","unstructured":"Govindan V, Chakraborty RS, Santikellur P, Chaudhary AK (2018) A hardware trojan attack on fpga-based cryptographic key generation: impact and detection. J Hardw Syst Secur 2:225\u2013239","journal-title":"J Hardw Syst Secur"},{"key":"6100_CR17","doi-asserted-by":"publisher","first-page":"189","DOI":"10.1007\/s41635-018-0058-x","volume":"3","author":"JR Hamlet","year":"2019","unstructured":"Hamlet JR, Mayo JR, Kammler VG (2019) Targeted modification of hardware trojans. J Hardw Syst Secur 3:189\u2013197","journal-title":"J Hardw Syst Secur"},{"key":"6100_CR18","doi-asserted-by":"publisher","first-page":"143","DOI":"10.1016\/j.vlsi.2018.09.007","volume":"64","author":"J He","year":"2019","unstructured":"He J, Guo X, Meade T, Dutta RG, Zhao Y, Jin Y (2019) Soc interconnection protection through formal verification. Integration 64:143\u2013151","journal-title":"Integration"},{"key":"6100_CR19","unstructured":"Ikram S, Barner C, Sweeney J, Ellis J, Dufresne B (2015) Formal verification of a multistage arbiter.\u00a0SNUG Boston,\u00a0Synopsys"},{"key":"6100_CR20","doi-asserted-by":"publisher","first-page":"246","DOI":"10.1007\/s41635-020-00100-2","volume":"4","author":"SA Islam","year":"2020","unstructured":"Islam SA, Sah LK, Katkoori S (2020) A framework for hardware trojan vulnerability estimation and localization in rtl designs. J Hardw Syst Secur 4:246\u2013262","journal-title":"J Hardw Syst Secur"},{"key":"6100_CR21","doi-asserted-by":"publisher","first-page":"173","DOI":"10.1007\/s41635-017-0008-z","volume":"1","author":"R JayashankaraShridevi","year":"2017","unstructured":"JayashankaraShridevi R, Ancajas DM, Chakraborty K, Roy S (2017) Security measures against a rogue network-on-chip. J Hardw Syst Secur 1:173\u2013187","journal-title":"J Hardw Syst Secur"},{"key":"6100_CR22","doi-asserted-by":"crossref","unstructured":"Kailas K, Paruthi V, Monwai B (2009) Formal verification of correctness and performance of random priority-based arbiters. In: 2009 Formal Methods in Computer-Aided Design, pp 101\u2013107. IEEE","DOI":"10.1109\/FMCAD.2009.5351137"},{"issue":"2","key":"6100_CR23","doi-asserted-by":"publisher","first-page":"185","DOI":"10.1108\/CW-10-2020-0268","volume":"48","author":"AA Khan","year":"2022","unstructured":"Khan AA, Mir RN, Din N-U (2022) Adaptive hybrid arbiter design for real-time traffic-aware scheduling. Circuit World 48(2):185\u2013203","journal-title":"Circuit World"},{"key":"6100_CR24","unstructured":"Kukimoto Y. Introduction to Formal Verification. https:\/\/ptolemy.berkeley.edu\/projects\/embedded\/research\/vis\/doc\/VisUser\/vis_user\/node4.html (Last Accessed 9 June 2023)"},{"key":"6100_CR25","doi-asserted-by":"publisher","first-page":"329","DOI":"10.1007\/s41635-020-00108-8","volume":"4","author":"VB Kumar","year":"2020","unstructured":"Kumar VB, Deb S, Gupta N, Bhasin S, Haj-Yahya J, Chattopadhyay A, Mendelson A (2020) Towards designing a secure risc-v system-on-chip: Itus. J Hardw Syst Secur 4:329\u2013342","journal-title":"J Hardw Syst Secur"},{"key":"6100_CR26","doi-asserted-by":"publisher","first-page":"279","DOI":"10.1007\/s10836-021-05936-2","volume":"37","author":"L Liu","year":"2021","unstructured":"Liu L, Wang T, Wang X (2021) Method of implanting hardware trojan based on ehw in part of circuit. J Electron Test 37:279\u2013284","journal-title":"J Electron Test"},{"key":"6100_CR27","doi-asserted-by":"publisher","first-page":"529","DOI":"10.1007\/s10836-019-05816-w","volume":"35","author":"Y Liu","year":"2019","unstructured":"Liu Y, He J, Ma H, Zhao Y (2019) Hardware trojan detection leveraging a novel golden layout model towards practical applications. J Electron Test 35:529\u2013541","journal-title":"J Electron Test"},{"key":"6100_CR28","doi-asserted-by":"crossref","unstructured":"Moein S, Khan S, Gulliver TA, Gebali F, El-Kharashi MW (2015) An attribute based classification of hardware trojans. In: 2015 Tenth International Conference on Computer Engineering & Systems (ICCES). IEEE, pp 351\u2013356","DOI":"10.1109\/ICCES.2015.7393074"},{"key":"6100_CR29","doi-asserted-by":"crossref","unstructured":"Moein S, Subramnian J, Gulliver TA, Gebali F, El-Kharashi MW (2015) Classification of hardware trojan detection techniques. In: 2015 Tenth International Conference on Computer Engineering & Systems (ICCES). IEEE, pp 357\u2013362","DOI":"10.1109\/ICCES.2015.7393075"},{"key":"6100_CR30","doi-asserted-by":"publisher","first-page":"343","DOI":"10.1007\/s41635-020-00107-9","volume":"4","author":"R Mukherjee","year":"2020","unstructured":"Mukherjee R, Govindan V, Koteshwara S, Das A, Parhi KK, Chakraborty RS (2020) Probabilistic hardware trojan attacks on multiple layers of reconfigurable network infrastructure. J Hardw Syst Secur 4:343\u2013360","journal-title":"J Hardw Syst Secur"},{"key":"6100_CR31","doi-asserted-by":"crossref","unstructured":"Nikhila S, Yamuna B, Balasubramanian K, Mishra D (2019) Fpga based implementation of a floating point multiplier and its hardware trojan models. In: 2019 IEEE 16th India Council International Conference (INDICON), pp. 1\u20134. IEEE","DOI":"10.1109\/INDICON47234.2019.9030341"},{"key":"6100_CR32","doi-asserted-by":"crossref","unstructured":"Rajendran J, Dhandayuthapany AM, Vedula V, Karri R (2016) Formal security verification of third party intellectual property cores for information leakage. In: 2016 29th International Conference on VLSI Design and 2016 15th International Conference on Embedded Systems (VLSID), pp 547\u2013552. IEEE","DOI":"10.1109\/VLSID.2016.143"},{"key":"6100_CR33","doi-asserted-by":"crossref","unstructured":"Rathmair M, Schupfer F, Krieg C (2014) Applied formal methods for hardware trojan detection. In: 2014 IEEE International Symposium on Circuits and Systems (ISCAS), pp 169\u2013172. IEEE","DOI":"10.1109\/ISCAS.2014.6865092"},{"key":"6100_CR34","doi-asserted-by":"crossref","unstructured":"Sep\u00falveda J, Aboul-Hassan D, Sigl G, Becker B, Sauer M (2018) Towards the formal verification of security properties of a network-on-chip router. In: 2018 IEEE 23rd European Test Symposium (ETS), pp 1\u20136. IEEE","DOI":"10.1109\/ETS.2018.8400692"},{"key":"6100_CR35","doi-asserted-by":"publisher","first-page":"85","DOI":"10.1007\/s41635-017-0001-6","volume":"1","author":"B Shakya","year":"2017","unstructured":"Shakya B, He T, Salmani H, Forte D, Bhunia S, Tehranipoor M (2017) Benchmarking of hardware trojans and maliciously affected circuits. J Hardw Syst Secur 1:85\u2013102","journal-title":"J Hardw Syst Secur"},{"issue":"5","key":"6100_CR36","doi-asserted-by":"publisher","first-page":"54","DOI":"10.1109\/MDAT.2017.2713352","volume":"34","author":"MB Slimane","year":"2017","unstructured":"Slimane MB, Hafaiedh IB, Robbana R (2017) Formal-based design and verification of soc arbitration protocols: A comparative analysis of tdma and round-robin. IEEE Des Test 34(5):54\u201362","journal-title":"IEEE Des Test"},{"key":"6100_CR37","doi-asserted-by":"crossref","unstructured":"Tang W, Su J, Gao Y (2023) Hardware trojan detection method based on dual discriminator assisted conditional generation adversarial network. In: J Electron Test, pp 1\u201312","DOI":"10.1007\/s10836-023-06054-x"},{"issue":"4","key":"6100_CR38","doi-asserted-by":"publisher","first-page":"473","DOI":"10.1007\/s10836-021-05960-2","volume":"37","author":"M Tebyanian","year":"2021","unstructured":"Tebyanian M, Mokhtarpour A, Shafieinejad A (2021) Sc-cotd: Hardware trojan detection based on sequential\/combinational testability features using ensemble classifier. J Electron Test 37(4):473\u2013487","journal-title":"J Electron Test"},{"issue":"4","key":"6100_CR39","doi-asserted-by":"publisher","first-page":"576","DOI":"10.1109\/TETC.2016.2585046","volume":"5","author":"N Veeranna","year":"2016","unstructured":"Veeranna N, Schafer BC (2016) Hardware trojan detection in behavioral intellectual properties (ip\u2019s) using property checking techniques. IEEE Trans Emerg Topics Comput 5(4):576\u2013585","journal-title":"IEEE Trans Emerg Topics Comput"},{"key":"6100_CR40","doi-asserted-by":"publisher","first-page":"56","DOI":"10.1007\/s41635-017-0005-2","volume":"1","author":"N Veeranna","year":"2017","unstructured":"Veeranna N, Schafer BC (2017) Trust filter: Runtime hardware trojan detection in behavioral mpsocs. J Hardw Syst Secur 1:56\u201367","journal-title":"J Hardw Syst Secur"},{"key":"6100_CR41","unstructured":"Weber M (2001) Arbiters: design ideas and coding styles. SNUG Boston,\u00a0Silicon Logic Engineering, Inc."},{"issue":"1","key":"6100_CR42","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/s41635-020-00102-0","volume":"5","author":"Y Yilmaz","year":"2021","unstructured":"Yilmaz Y, Aniello L, Halak B (2021) Assure: A hardware-based security protocol for resource-constrained iot systems. J Hardw Syst Secur 5(1):1\u201318","journal-title":"J Hardw Syst Secur"}],"container-title":["Journal of Electronic Testing"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10836-024-06100-2.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1007\/s10836-024-06100-2\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10836-024-06100-2.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,5,8]],"date-time":"2024-05-08T06:15:34Z","timestamp":1715148934000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/s10836-024-06100-2"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024,2]]},"references-count":42,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2024,2]]}},"alternative-id":["6100"],"URL":"https:\/\/doi.org\/10.1007\/s10836-024-06100-2","relation":{},"ISSN":["0923-8174","1573-0727"],"issn-type":[{"value":"0923-8174","type":"print"},{"value":"1573-0727","type":"electronic"}],"subject":[],"published":{"date-parts":[[2024,2]]},"assertion":[{"value":"1 November 2023","order":1,"name":"received","label":"Received","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"10 January 2024","order":2,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"20 March 2024","order":3,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}},{"order":1,"name":"Ethics","group":{"name":"EthicsHeading","label":"Declarations"}},{"value":"The authors have no relevant financial or non-financial interests to disclose.","order":2,"name":"Ethics","group":{"name":"EthicsHeading","label":"Competing interests"}}]}}