Инвазивный подход к верификации функционально-структурных спецификаций, реализованных в заказных интегральных схемах
- Авторы: Нагибин Д.В1, Петренко А.С1, Давыденко В.С1, Котенко И.В2, Федорченко Е.В2
-
Учреждения:
- Федеральное государственное бюджетное военное образовательное учреждение высшего образования «Военно-космическая академия имени А.Ф. Можайского» Министерства обороны Российской Федерации
- Федеральное государственное бюджетное учреждение науки «Санкт-Петербургский Федеральный исследовательский центр Российской академии наук» (СПб ФИЦ РАН)
- Выпуск: Том 24, № 2 (2025)
- Страницы: 526-555
- Раздел: Математическое моделирование и прикладная математика
- URL: https://journal-vniispk.ru/2713-3192/article/view/289696
- DOI: https://doi.org/10.15622/ia.24.2.6
- ID: 289696
Цитировать
Полный текст
Аннотация
Представлен подход к верификации функционально-структурных спецификаций, реализованных в заказных интегральных схемах, основанный на инвазивных методах исследования. Актуальность проведённого исследования обусловлена необходимостью проведения верификации функционально-структурных спецификаций, поставляемых сторонними исполнителями аппаратных реализаций алгоритмов обеспечения информационной безопасности, сложностью выявления на аппаратном уровне модификаций этих алгоритмов и внедрённых в них недокументированных возможностей и отсутствием единых универсальных или стандартизированных методов решения этой задачи. Сформулирована математическая постановка задачи исследования, суть которой состоит в проверке равенства значений параметров заявленной спецификации с их значениями, восстановленными методом обратного проектирования. Представлены результаты применения предложенного подхода к верификации функционально-структурных спецификаций на примерах аппаратно-реализованных алгоритмов шифрования DES и AES. Восстановленные функционально-структурные блоки алгоритмов (в частности – блок подстановок) были успешно верифицированы.
Об авторах
Д. В Нагибин
Федеральное государственное бюджетное военное образовательное учреждение высшего образования «Военно-космическая академия имени А.Ф. Можайского» Министерства обороны Российской Федерации
Email: nagibin.86@internet.ru
улица Ждановская 13
А. С Петренко
Федеральное государственное бюджетное военное образовательное учреждение высшего образования «Военно-космическая академия имени А.Ф. Можайского» Министерства обороны Российской Федерации
Email: a.petrenko1999@rambler.ru
улица Ждановская 13
В. С Давыденко
Федеральное государственное бюджетное военное образовательное учреждение высшего образования «Военно-космическая академия имени А.Ф. Можайского» Министерства обороны Российской Федерации
Email: nagibin.86@internet.ru
улица Ждановская 13
И. В Котенко
Федеральное государственное бюджетное учреждение науки «Санкт-Петербургский Федеральный исследовательский центр Российской академии наук» (СПб ФИЦ РАН)
Email: ivkote@comsec.spb.ru
14-я линия В.О. 39
Е. В Федорченко
Федеральное государственное бюджетное учреждение науки «Санкт-Петербургский Федеральный исследовательский центр Российской академии наук» (СПб ФИЦ РАН)
Email: doynikova@comsec.spb.ru
14-я линия В.О. 39
Список литературы
- Нагибин Д.В., Платонов А.А., Сабиров Т.Р. Методика идентификации реализованных в заказных интегральных схемах функционально-структурных спецификаций // Труды Военно-космической академии имени А.Ф. Можайского. 2024. № 690. С. 112–120.
- 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.
- 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.
- 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.
- 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.
- 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.
- 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.
- Zahid A.H., Arshad M.J., Ahmad M. Substitution-boxes using cubic fractional transformation // Entropy. 2019. vol. 21(3). doi: 10.3390/e21030245.
- Котенко И.В., Левшун Д.С., Чечулин А.А., Ушаков И.А., Красов А.В. Комплексный подход к обеспечению безопасности киберфизических систем на системе микроконтроллеров // Вопросы кибербезопасности. 2018. № 3(27). С. 29–38. doi: 10.21681/2311-3456-2018-3-29-38.
- Десницкий В.А., Чечулин А.А., Котенко И.В., Левшун Д.С., Коломеец М.В. Комбинированная методика проектирования защищенных встроенных устройств на примере системы охраны периметра // Труды СПИИРАН. 2016. № 5(48). С. 5–31. doi: 10.15622/sp.48.1.
- 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.
- Ковалев В.В., Компаниец Р.И., Новиков В.А. Верификация программ на основе соотношений подобия // Труды СПИИРАН. 2015. vol. 1(38). С. 233–245. doi: 10.15622/sp.38.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.
- 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.
- Котенко И.В., Резник С.А., Шоров А.В. Верификация протоколов безопасности на основе комбинированного использования существующих методов и средств // Труды СПИИРАН. 2009. № 8. С. 292–310. doi: 10.15622/sp.8.14.
- 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.
- 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.
- 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.
- 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.
- 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.
- 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.
- 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.
- 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.
- 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.
- 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.
- 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.
- 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.
- 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.
- 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.
- 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.
- 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.
- Токарева Н.Н. Симметричная криптография. Краткий курс: учебное пособие / Под ред. А.Л. Перегожина // Новосибирск: Новосиб. гос. Ун-т., 2012. 234 с.
- Шнайер Б. Прикладная криптография. Протоколы, алгоритмы и исходный код на С. М.: Диалектика. 2017. 1040 с.
- Макаренко С.И. Информационное противоборство и радиоэлектронная борьба в сетецентрических войнах начала XXI века. Санкт-Петербург: Наукоемкие технологии, 2017. 549 с. URL: http://psyfactor.org/t/Makarenko-InfPro_2017.pdf.
- 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.
- Smart N.P. Cryptography Made Simple. Information Security and Cryptography series. Springer, 2016. 481 p. doi: 10.1007/978-3-319-21936-3.
- Бабенко Л.К., Ищукова Е.А. Современные алгоритмы блочного шифрования и методы их анализа. М.: Гелиос АРВ. 2006. 376 с.
Дополнительные файлы
