Инвазивный подход к верификации функционально-структурных спецификаций, реализованных в заказных интегральных схемах
Ключевые слова:
заказная интегральная схема, идентификация, верификация, функционально-структурная спецификация, алгоритм шифрованияАннотация
Представлен подход к верификации функционально-структурных спецификаций, реализованных в заказных интегральных схемах, основанный на инвазивных методах исследования. Актуальность проведённого исследования обусловлена необходимостью проведения верификации функционально-структурных спецификаций, поставляемых сторонними исполнителями аппаратных реализаций алгоритмов обеспечения информационной безопасности, сложностью выявления на аппаратном уровне модификаций этих алгоритмов и внедрённых в них недокументированных возможностей и отсутствием единых универсальных или стандартизированных методов решения этой задачи. Сформулирована математическая постановка задачи исследования, суть которой состоит в проверке равенства значений параметров заявленной спецификации с их значениями, восстановленными методом обратного проектирования. Представлены результаты применения предложенного подхода к верификации функционально-структурных спецификаций на примерах аппаратно-реализованных алгоритмов шифрования DES и AES. Восстановленные функционально-структурные блоки алгоритмов (в частности – блок подстановок) были успешно верифицированы.
Литература
1. Нагибин Д.В., Платонов А.А., Сабиров Т.Р. Методика идентификации реализованных в заказных интегральных схемах функционально-структурных спецификаций // Труды Военно-космической академии имени А.Ф. Можайского. 2024. № 690. С. 112–120.
2. Mustafa Dhiaa Al-Hassan, Qusay Zuhair Abdulla. Robust Password Encryption Technique with an Extra Security Layer // Iraqi Journal of Science. 2023. vol. 64. no. 3. pp. 1477–1486. DOI: 10.24996/ijs.2023.64.3.36.
3. Alsuwaiedi H.K.A., Rahma A.M.S. A new modified DES algorithm based on the development of binary encryption functions // Journal of King Saud University – Computer and Information Sciences. 2023. vol. 35(8). DOI: 10.1016/j.jksuci.2023.101716.
4. Agate V., Concone F., de Paola A., Ferraro P., Lo Re G., Morana M. Bayesian Modeling for Differential Cryptanalysis of Block Ciphers: A DES Instance // IEEE Access. 2023. vol. 11. pp. 4809–4820. DOI: 10.1109/ACCESS.2023.3236240.
5. Wu Y., Dai X. Encryption of accounting data using DES algorithm in Computing Environment // Journal of Intelligent & Fuzzy Systems. 2020. vol. 39. pp. 5085–5095. DOI: 10.3233/JIFS-179994.
6. Nitaj A., Susilo W., Tonien J. Enhanced S-boxes for the Advanced Encryption Standard with maximal periodicity and better avalanche property // Computer Standards & Interfaces. 2024. vol. 87. DOI: 10.1016/j.csi.2023.103769.
7. Zahid A.H., Arshad M.J. An innovative design of substitution-boxes using cubic polynomial mapping // Symmetry. 2019. vol. 11(3). DOI: 10.3390/sym11030437.
8. Zahid A.H., Arshad M.J., Ahmad M. Substitution-boxes using cubic fractional transformation // Entropy. 2019. vol. 21(3). DOI: 10.3390/e21030245.
9. Котенко И.В., Левшун Д.С., Чечулин А.А., Ушаков И.А., Красов А.В. Комплексный подход к обеспечению безопасности киберфизических систем на системе микроконтроллеров // Вопросы кибербезопасности. 2018. № 3(27). С. 29–38. DOI: 10.21681/2311-3456-2018-3-29-38.
10. Десницкий В.А., Чечулин А.А., Котенко И.В., Левшун Д.С., Коломеец М.В. Комбинированная методика проектирования защищенных встроенных устройств на примере системы охраны периметра // Труды СПИИРАН. 2016. № 5(48). С. 5–31. DOI: 10.15622/sp.48.1.
11. Desnitsky V., Levshun D., Chechulin A., Kotenko I. Design technique for secure embedded devices: application for creation of integrated cyber-physical security system // Journal of Wireless Mobile Networks, Ubiquitous Computing, and Dependable Applications (JoWUA). 2016. vol. 7. pp. 60–80.
12. Ковалев В.В., Компаниец Р.И., Новиков В.А. Верификация программ на основе соотношений подобия // Труды СПИИРАН. 2015. vol. 1(38). С. 233–245. DOI: 10.15622/sp.38.13.
13. Cousot P., Cousot R. A Galois connection calculus for abstract interpretation // Proceedings of the 41st Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL’14). ACM, 2014. pp. 3–4. DOI: 10.1145/2535838.2537850.
14. Fang Z., Darais D., Near J.P., Zhang Y. Zero Knowledge Static Program Analysis // Proceedings of the 2021 ACM SIGSAC Conference on Computer and Communications Security (CCS'21). New York, USA: Association for Computing Machinery, 2021. pp. 2951–2967. DOI: 10.1145/3460120.3484795.
15. Котенко И.В., Резник С.А., Шоров А.В. Верификация протоколов безопасности на основе комбинированного использования существующих методов и средств // Труды СПИИРАН. 2009. № 8. С. 292–310. DOI: 10.15622/sp.8.14.
16. Tran D.D., Ogata K. IPSG: Invariant Proof Score Generator // 2022 IEEE 46th Annual Computers, Software, and Applications Conference (COMPSAC). 2022. pp. 1050–1055. DOI: 10.1109/COMPSAC54236.2022.00164.
17. Riesco A., Ogata K., Futatsugi K. A Maude environment for cafeOBJ // Formal Aspects of Computing. 2017. vol. 29. pp. 309–334. DOI: 10.1007/s00165-016-0398-7.
18. Clavel M., Durán F., Eker S., Lincoln P., Martí-Oliet N., Meseguer J., Talcott C. All about Maude – a High-Performance Logical Framework. How to Specify, Program and Verify Systems in Rewriting Logic // Lecture Notes in Computer Science. 2007. 802 p. DOI: 10.1007/978-3-540-71999-1.
19. Tran D.D., Ogata K. Formal verification of TLS 1.2 by automatically generating proof scores // Computers & Security. 2022. vol. 123. DOI: 10.1016/j.cose.2022.102909.
20. Saeed Mahlaqa, Ibrar Muhammad, Mahmood Dua, Delshadi Amirmohammad, Saleemi Aqdas. Enhancing Computer Security through Formal Verification of Cryptographic Protocols Using Model Checking and Partial Order Techniques // The Asian Bulletin of Big Data Management. 2024. vol. 4(2). pp. 225–238. DOI: 10.62019/abbdm.v4i02.176.
21. Curaba C., D'Ambrosi D., Minisini A., Antol'in N.P.-C. CryptoFormalEval: Integrating LLMs and Formal Verification for Automated Cryptographic Protocol Vulnerability Detection. 2024. arXiv preprint arXiv:2411.13627.
22. Riesco A., Ogata K. An integrated tool set for verifying CafeOBJ specifications // Journal of Systems and Software. 2022. vol. 189. DOI: 10.1016/j.jss.2022.111302.
23. Awadhutkar P., Tamrawi A., Goluch R., Kothari S. Control flow equivalence method for establishing sanctity of compiling // Computers & Security. 2022. vol. 115. DOI: 10.1016/j.cose.2022.102608.
24. Cheng D., Dong Ch., He W., Chen Zh., Liu X., Zhang H. A fine-grained detection method for gate-level hardware Trojan based on bidirectional Graph Neural Networks // Journal of King Saud University – Computer and Information Sciences. 2023. vol. 35(10). DOI: 10.1016/j.jksuci.2023.101822.
25. Chen Sh., Wang T., Huang Zh., Hou X. Detection method of Golden Chip-Free Hardware Trojan based on the combination of ResNeXt structure and attention mechanism // Computers & Security. 2023. vol. 134. DOI: 10.1016/j.cose.2023.103428.
26. Rozesara M., Ghazinoori S., Manteghi M., Tabatabaeian S.H. A reverse engineering-based model for innovation process in complex product systems: Multiple case studies in the aviation industry // Journal of Engineering and Technology Management. 2023. vol. 69. DOI: 10.1016/j.jengtecman.2023.101765.
27. Lavanya T., Rajalakshmi K. Heterogenous ensemble learning driven multi-parametric assessment model for hardware Trojan detection // Integration. 2023. vol. 89. pp. 217–228. DOI: 10.1016/j.vlsi.2022.12.011.
28. Esirci F.N., Bayrakci A.A. Delay based hardware Trojan detection exploiting spatial correlations to suppress variations // Integration. 2023. vol. 91. pp. 107–118. DOI: 10.1016/j.vlsi.2023.03.006.
29. Cassano L., Iamundo M., Lopez T.A., Nazzari A., Di Natale G. DETON: DEfeating hardware Trojan horses in microprocessors through software ObfuscatioN // Journal of Systems Architecture. 2022. vol. 129. DOI: 10.1016/j.sysarc.2022.102592.
30. Damljanovic A., Ruospo A., Sanchez E., Squillero G. Machine learning for hardware security: Classifier-based identification of Trojans in pipelined microprocessors // Applied Soft Computing. 2022. vol. 116. DOI: 10.1016/j.asoc.2021.108068.
31. Palumbo A., Cassano L., Luzzi B., Hernández J.A., Reviriego P., Bianchi G., Ottavi M. Is your FPGA bitstream Hardware Trojan-free? Machine learning can provide an answer // Journal of Systems Architecture. 2022. vol. 128. DOI: 10.1016/j.sysarc.2022.102543.
32. Токарева Н.Н. Симметричная криптография. Краткий курс: учебное пособие / Под ред. А.Л. Перегожина // Новосибирск: Новосиб. гос. Ун-т., 2012. 234 с.
33. Шнайер Б. Прикладная криптография. Протоколы, алгоритмы и исходный код на С. М.: Диалектика. 2017. 1040 с.
34. Макаренко С.И. Информационное противоборство и радиоэлектронная борьба в сетецентрических войнах начала XXI века. Санкт-Петербург: Наукоемкие технологии, 2017. 549 с. URL: http://psyfactor.org/t/Makarenko-InfPro_2017.pdf.
35. Elçi A., Pieprzyk J., Chefranov A.G., Orgun M.A., Wang H., Shankaran R. Theory and Practice of Cryptography Solutions for Secure Information Systems. Hershey, PA: IGI Global Scientific Publishing, 2013. 351 p. DOI: 10.4018/978-1-4666-4030-6.
36. Smart N.P. Cryptography Made Simple. Information Security and Cryptography series. Springer, 2016. 481 p. DOI: 10.1007/978-3-319-21936-3.
37. Бабенко Л.К., Ищукова Е.А. Современные алгоритмы блочного шифрования и методы их анализа. М.: Гелиос АРВ. 2006. 376 с.
2. Mustafa Dhiaa Al-Hassan, Qusay Zuhair Abdulla. Robust Password Encryption Technique with an Extra Security Layer // Iraqi Journal of Science. 2023. vol. 64. no. 3. pp. 1477–1486. DOI: 10.24996/ijs.2023.64.3.36.
3. Alsuwaiedi H.K.A., Rahma A.M.S. A new modified DES algorithm based on the development of binary encryption functions // Journal of King Saud University – Computer and Information Sciences. 2023. vol. 35(8). DOI: 10.1016/j.jksuci.2023.101716.
4. Agate V., Concone F., de Paola A., Ferraro P., Lo Re G., Morana M. Bayesian Modeling for Differential Cryptanalysis of Block Ciphers: A DES Instance // IEEE Access. 2023. vol. 11. pp. 4809–4820. DOI: 10.1109/ACCESS.2023.3236240.
5. Wu Y., Dai X. Encryption of accounting data using DES algorithm in Computing Environment // Journal of Intelligent & Fuzzy Systems. 2020. vol. 39. pp. 5085–5095. DOI: 10.3233/JIFS-179994.
6. Nitaj A., Susilo W., Tonien J. Enhanced S-boxes for the Advanced Encryption Standard with maximal periodicity and better avalanche property // Computer Standards & Interfaces. 2024. vol. 87. DOI: 10.1016/j.csi.2023.103769.
7. Zahid A.H., Arshad M.J. An innovative design of substitution-boxes using cubic polynomial mapping // Symmetry. 2019. vol. 11(3). DOI: 10.3390/sym11030437.
8. Zahid A.H., Arshad M.J., Ahmad M. Substitution-boxes using cubic fractional transformation // Entropy. 2019. vol. 21(3). DOI: 10.3390/e21030245.
9. Котенко И.В., Левшун Д.С., Чечулин А.А., Ушаков И.А., Красов А.В. Комплексный подход к обеспечению безопасности киберфизических систем на системе микроконтроллеров // Вопросы кибербезопасности. 2018. № 3(27). С. 29–38. DOI: 10.21681/2311-3456-2018-3-29-38.
10. Десницкий В.А., Чечулин А.А., Котенко И.В., Левшун Д.С., Коломеец М.В. Комбинированная методика проектирования защищенных встроенных устройств на примере системы охраны периметра // Труды СПИИРАН. 2016. № 5(48). С. 5–31. DOI: 10.15622/sp.48.1.
11. Desnitsky V., Levshun D., Chechulin A., Kotenko I. Design technique for secure embedded devices: application for creation of integrated cyber-physical security system // Journal of Wireless Mobile Networks, Ubiquitous Computing, and Dependable Applications (JoWUA). 2016. vol. 7. pp. 60–80.
12. Ковалев В.В., Компаниец Р.И., Новиков В.А. Верификация программ на основе соотношений подобия // Труды СПИИРАН. 2015. vol. 1(38). С. 233–245. DOI: 10.15622/sp.38.13.
13. Cousot P., Cousot R. A Galois connection calculus for abstract interpretation // Proceedings of the 41st Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL’14). ACM, 2014. pp. 3–4. DOI: 10.1145/2535838.2537850.
14. Fang Z., Darais D., Near J.P., Zhang Y. Zero Knowledge Static Program Analysis // Proceedings of the 2021 ACM SIGSAC Conference on Computer and Communications Security (CCS'21). New York, USA: Association for Computing Machinery, 2021. pp. 2951–2967. DOI: 10.1145/3460120.3484795.
15. Котенко И.В., Резник С.А., Шоров А.В. Верификация протоколов безопасности на основе комбинированного использования существующих методов и средств // Труды СПИИРАН. 2009. № 8. С. 292–310. DOI: 10.15622/sp.8.14.
16. Tran D.D., Ogata K. IPSG: Invariant Proof Score Generator // 2022 IEEE 46th Annual Computers, Software, and Applications Conference (COMPSAC). 2022. pp. 1050–1055. DOI: 10.1109/COMPSAC54236.2022.00164.
17. Riesco A., Ogata K., Futatsugi K. A Maude environment for cafeOBJ // Formal Aspects of Computing. 2017. vol. 29. pp. 309–334. DOI: 10.1007/s00165-016-0398-7.
18. Clavel M., Durán F., Eker S., Lincoln P., Martí-Oliet N., Meseguer J., Talcott C. All about Maude – a High-Performance Logical Framework. How to Specify, Program and Verify Systems in Rewriting Logic // Lecture Notes in Computer Science. 2007. 802 p. DOI: 10.1007/978-3-540-71999-1.
19. Tran D.D., Ogata K. Formal verification of TLS 1.2 by automatically generating proof scores // Computers & Security. 2022. vol. 123. DOI: 10.1016/j.cose.2022.102909.
20. Saeed Mahlaqa, Ibrar Muhammad, Mahmood Dua, Delshadi Amirmohammad, Saleemi Aqdas. Enhancing Computer Security through Formal Verification of Cryptographic Protocols Using Model Checking and Partial Order Techniques // The Asian Bulletin of Big Data Management. 2024. vol. 4(2). pp. 225–238. DOI: 10.62019/abbdm.v4i02.176.
21. Curaba C., D'Ambrosi D., Minisini A., Antol'in N.P.-C. CryptoFormalEval: Integrating LLMs and Formal Verification for Automated Cryptographic Protocol Vulnerability Detection. 2024. arXiv preprint arXiv:2411.13627.
22. Riesco A., Ogata K. An integrated tool set for verifying CafeOBJ specifications // Journal of Systems and Software. 2022. vol. 189. DOI: 10.1016/j.jss.2022.111302.
23. Awadhutkar P., Tamrawi A., Goluch R., Kothari S. Control flow equivalence method for establishing sanctity of compiling // Computers & Security. 2022. vol. 115. DOI: 10.1016/j.cose.2022.102608.
24. Cheng D., Dong Ch., He W., Chen Zh., Liu X., Zhang H. A fine-grained detection method for gate-level hardware Trojan based on bidirectional Graph Neural Networks // Journal of King Saud University – Computer and Information Sciences. 2023. vol. 35(10). DOI: 10.1016/j.jksuci.2023.101822.
25. Chen Sh., Wang T., Huang Zh., Hou X. Detection method of Golden Chip-Free Hardware Trojan based on the combination of ResNeXt structure and attention mechanism // Computers & Security. 2023. vol. 134. DOI: 10.1016/j.cose.2023.103428.
26. Rozesara M., Ghazinoori S., Manteghi M., Tabatabaeian S.H. A reverse engineering-based model for innovation process in complex product systems: Multiple case studies in the aviation industry // Journal of Engineering and Technology Management. 2023. vol. 69. DOI: 10.1016/j.jengtecman.2023.101765.
27. Lavanya T., Rajalakshmi K. Heterogenous ensemble learning driven multi-parametric assessment model for hardware Trojan detection // Integration. 2023. vol. 89. pp. 217–228. DOI: 10.1016/j.vlsi.2022.12.011.
28. Esirci F.N., Bayrakci A.A. Delay based hardware Trojan detection exploiting spatial correlations to suppress variations // Integration. 2023. vol. 91. pp. 107–118. DOI: 10.1016/j.vlsi.2023.03.006.
29. Cassano L., Iamundo M., Lopez T.A., Nazzari A., Di Natale G. DETON: DEfeating hardware Trojan horses in microprocessors through software ObfuscatioN // Journal of Systems Architecture. 2022. vol. 129. DOI: 10.1016/j.sysarc.2022.102592.
30. Damljanovic A., Ruospo A., Sanchez E., Squillero G. Machine learning for hardware security: Classifier-based identification of Trojans in pipelined microprocessors // Applied Soft Computing. 2022. vol. 116. DOI: 10.1016/j.asoc.2021.108068.
31. Palumbo A., Cassano L., Luzzi B., Hernández J.A., Reviriego P., Bianchi G., Ottavi M. Is your FPGA bitstream Hardware Trojan-free? Machine learning can provide an answer // Journal of Systems Architecture. 2022. vol. 128. DOI: 10.1016/j.sysarc.2022.102543.
32. Токарева Н.Н. Симметричная криптография. Краткий курс: учебное пособие / Под ред. А.Л. Перегожина // Новосибирск: Новосиб. гос. Ун-т., 2012. 234 с.
33. Шнайер Б. Прикладная криптография. Протоколы, алгоритмы и исходный код на С. М.: Диалектика. 2017. 1040 с.
34. Макаренко С.И. Информационное противоборство и радиоэлектронная борьба в сетецентрических войнах начала XXI века. Санкт-Петербург: Наукоемкие технологии, 2017. 549 с. URL: http://psyfactor.org/t/Makarenko-InfPro_2017.pdf.
35. Elçi A., Pieprzyk J., Chefranov A.G., Orgun M.A., Wang H., Shankaran R. Theory and Practice of Cryptography Solutions for Secure Information Systems. Hershey, PA: IGI Global Scientific Publishing, 2013. 351 p. DOI: 10.4018/978-1-4666-4030-6.
36. Smart N.P. Cryptography Made Simple. Information Security and Cryptography series. Springer, 2016. 481 p. DOI: 10.1007/978-3-319-21936-3.
37. Бабенко Л.К., Ищукова Е.А. Современные алгоритмы блочного шифрования и методы их анализа. М.: Гелиос АРВ. 2006. 376 с.
Опубликован
2025-04-01
Как цитировать
Нагибин, Д. В., Петренко, А. С., Давыденко, В. С., Котенко, И. В., & Федорченко, Е. В. (2025). Инвазивный подход к верификации функционально-структурных спецификаций, реализованных в заказных интегральных схемах. Информатика и автоматизация, 24(2), 526-555. https://doi.org/10.15622/ia.24.2.6
Раздел
Математическое моделирование и прикладная математика
Copyright (c) Дмитрий Владимирович Нагибин, Алексей Сергеевич Петренко, Владислав Сергеевич Давыденко, Игорь Витальевич Котенко, Елена Владимировна Федорченко
Это произведение доступно по лицензии Creative Commons «Attribution» («Атрибуция») 4.0 Всемирная.
Авторы, которые публикуются в данном журнале, соглашаются со следующими условиями: Авторы сохраняют за собой авторские права на работу и передают журналу право первой публикации вместе с работой, одновременно лицензируя ее на условиях Creative Commons Attribution License, которая позволяет другим распространять данную работу с обязательным указанием авторства данной работы и ссылкой на оригинальную публикацию в этом журнале. Авторы сохраняют право заключать отдельные, дополнительные контрактные соглашения на неэксклюзивное распространение версии работы, опубликованной этим журналом (например, разместить ее в университетском хранилище или опубликовать ее в книге), со ссылкой на оригинальную публикацию в этом журнале. Авторам разрешается размещать их работу в сети Интернет (например, в университетском хранилище или на их персональном веб-сайте) до и во время процесса рассмотрения ее данным журналом, так как это может привести к продуктивному обсуждению, а также к большему количеству ссылок на данную опубликованную работу (Смотри The Effect of Open Access).