Invasive Approach to Verification of Functional and Structural Specifications Implemented in Custom Integrated Circuits

Capa

Citar

Texto integral

Resumo

An approach to verification of functional and structural specifications implemented in custom integrated circuits based on invasive research methods is presented. The relevance of this research is determined by the necessity of verification of functional-structural specifications supplied by third-party implementers of hardware implementations of information security algorithms, the difficulty of detecting modifications of these algorithms and undocumented capabilities implemented at the hardware level, and the lack of uniform, universal or standardized methods for solving this problem. The mathematical formulation of the research problem is specified; its essence is to verify the equality of the values of the declared specification parameters and their values restored by the reverse engineering method. The results of the application of the verification technique of functional and structural specifications are presented using examples of its adaptation to the study of hardware-implemented DES and AES encryption algorithms. The restored functional and structural blocks of the algorithms (in particular, the substitution block) were successfully verified.

Sobre autores

D. Nagibin

Federal State Budgetary Military Educational Institution of Higher Education «Military Space Academy named after A.F. Mozhaisky» of the Ministry of Defense of the Russian Federation

Email: nagibin.86@internet.ru
Zhdanovskaya St. 13

A. Petrenko

Federal State Budgetary Military Educational Institution of Higher Education «Military Space Academy named after A.F. Mozhaisky» of the Ministry of Defense of the Russian Federation

Email: a.petrenko1999@rambler.ru
Zhdanovskaya St. 13

V. Davydenko

Federal State Budgetary Military Educational Institution of Higher Education «Military Space Academy named after A.F. Mozhaisky» of the Ministry of Defense of the Russian Federation

Email: nagibin.86@internet.ru
Zhdanovskaya St. 13

I. Kotenko

St. Petersburg Federal Research Center of the Russian Academy of Sciences (SPC RAS)

Email: ivkote@comsec.spb.ru
14-th Line V.O. 39

E. Fedorchenko

St. Petersburg Federal Research Center of the Russian Academy of Sciences (SPC RAS)

Email: doynikova@comsec.spb.ru
14-th Line V.O. 39

Bibliografia

  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 с.

Arquivos suplementares

Arquivos suplementares
Ação
1. JATS XML
Baixar

Согласие на обработку персональных данных с помощью сервиса «Яндекс.Метрика»

1. Я (далее – «Пользователь» или «Субъект персональных данных»), осуществляя использование сайта https://journals.rcsi.science/ (далее – «Сайт»), подтверждая свою полную дееспособность даю согласие на обработку персональных данных с использованием средств автоматизации Оператору - федеральному государственному бюджетному учреждению «Российский центр научной информации» (РЦНИ), далее – «Оператор», расположенному по адресу: 119991, г. Москва, Ленинский просп., д.32А, со следующими условиями.

2. Категории обрабатываемых данных: файлы «cookies» (куки-файлы). Файлы «cookie» – это небольшой текстовый файл, который веб-сервер может хранить в браузере Пользователя. Данные файлы веб-сервер загружает на устройство Пользователя при посещении им Сайта. При каждом следующем посещении Пользователем Сайта «cookie» файлы отправляются на Сайт Оператора. Данные файлы позволяют Сайту распознавать устройство Пользователя. Содержимое такого файла может как относиться, так и не относиться к персональным данным, в зависимости от того, содержит ли такой файл персональные данные или содержит обезличенные технические данные.

3. Цель обработки персональных данных: анализ пользовательской активности с помощью сервиса «Яндекс.Метрика».

4. Категории субъектов персональных данных: все Пользователи Сайта, которые дали согласие на обработку файлов «cookie».

5. Способы обработки: сбор, запись, систематизация, накопление, хранение, уточнение (обновление, изменение), извлечение, использование, передача (доступ, предоставление), блокирование, удаление, уничтожение персональных данных.

6. Срок обработки и хранения: до получения от Субъекта персональных данных требования о прекращении обработки/отзыва согласия.

7. Способ отзыва: заявление об отзыве в письменном виде путём его направления на адрес электронной почты Оператора: info@rcsi.science или путем письменного обращения по юридическому адресу: 119991, г. Москва, Ленинский просп., д.32А

8. Субъект персональных данных вправе запретить своему оборудованию прием этих данных или ограничить прием этих данных. При отказе от получения таких данных или при ограничении приема данных некоторые функции Сайта могут работать некорректно. Субъект персональных данных обязуется сам настроить свое оборудование таким способом, чтобы оно обеспечивало адекватный его желаниям режим работы и уровень защиты данных файлов «cookie», Оператор не предоставляет технологических и правовых консультаций на темы подобного характера.

9. Порядок уничтожения персональных данных при достижении цели их обработки или при наступлении иных законных оснований определяется Оператором в соответствии с законодательством Российской Федерации.

10. Я согласен/согласна квалифицировать в качестве своей простой электронной подписи под настоящим Согласием и под Политикой обработки персональных данных выполнение мною следующего действия на сайте: https://journals.rcsi.science/ нажатие мною на интерфейсе с текстом: «Сайт использует сервис «Яндекс.Метрика» (который использует файлы «cookie») на элемент с текстом «Принять и продолжить».