C# парсер для извлечения структуры криптографических протоколов из исходного кода

Криптографические протоколы являются ядром любой защищенной системы. С их помощью передаются данные, которые нуждаются в защите от третьих лиц. Как правило, криптографический протокол разрабатывается, анализируется с использованием средств формальной верификации и, если он безопасен, реализуется на языке программирования, на котором разрабатывается система. Однако при практической реализации криптографического протокола могут возникать ошибки из-за человеческого фактора, предположений, которые необходимы для возможности реализации протокола, что влечет за собой подрыв его безопасности. Таким образом, оказывается, что сам протокол изначально считался безопасным, но его реализация на самом деле небезопасна. Кроме того, формальная верификация использует довольно абстрактные понятия и не позволяет полностью проанализировать протокол. В данной статье представлен алгоритм анализа исходного кода языка программирования C # для извлечения структуры криптографических протоколов. Описаны особенности реализации протоколов на практике. Алгоритм основан на определении ключевых областей кода, содержащих специфические для криптографических протоколов конструкции, и определении цепочки преобразований переменных из состояния отправки или получения сообщений до их начальной инициализации с учетом возможных криптографических преобразований для составления дерева, из которого будет извлечена упрощенная структура криптографического протокола. Алгоритм реализован на языке программирования C# с использованием синтаксического анализатора Roslyn. В качестве примера представлен криптографический протокол, который содержит основные операции и функции, а именно: асимметричное и симметричное шифрование, хеширование, подпись, генерация случайных чисел, конкатенация данных. Работа анализатора показана с использованием этого протокола в качестве примера. Описана будущая работа.

1. Chaki S., Datta A. ASPIER: An automated framework for verifying security protocol implementations. In Proc. of the 22nd IEEE Computer Security Foundations Symposium, 2009, pp. 172-185.

2. Goubault-Larrecq J., Parrennes F. Cryptographic protocol analysis on real C code. Lecture Notes in Computer Science, vol. 3385, 2005, pp. 363-379.

3. Goubault-Larrecq J., Parrennes F. Cryptographic protocol analysis on real C code. Technical report, Laboratoire Spécification et Vérification, Report LSV-09-18, 2009.

4. Jürjens J. Using interface specifications for verifying crypto-protocol implementations. In Proc. of the Workshop on foundations of interface technologies (FIT). 2008.

5. Jürjens J. Automated security verification for crypto protocol implementations: Verifying the jessie project. Electronic Notes in Theoretical Computer Science, vol. 250, № 1, 2009, pp. 123-136.

6. O’Shea N. Using Elyjah to analyse Java implementations of cryptographic protocols. In Proc. of the Joint Workshop on Foundations of Computer Security, Automated Reasoning for Security Protocol Analysis and Issues in the Theory of Security (FCS-ARSPA-WITS-2008). – 2008.

7. Backes M., Maffei M., Unruh D. Computationally sound verification of source code. In Proc. of the 17th ACM conference on Computer and communications security, 2010, pp. 387-398.

8. Bhargavan K. et al. Cryptographically verified implementations for TLS. In Proc. of the 15th ACM conference on Computer and communications security, 2008, pp. 459-468.

9. Bhargavan K., Fournet C., Gordon A. D. Verified reference implementations of WS-Security protocols. Lecture Notes in Computer Science, vol. 4184, 2006, pp. 77-106.

10. Bhargavan K. et al. Verified interoperable implementations of security protocols. ACM Transactions on Programming Languages and Systems, vol. 31, №. 1, 2008.

11. Bhargavan K. et al. Verified implementations of the information card federated identity-management protocol. In Proc. of the 2008 ACM symposium on Information, computer and communications security, 2008, pp. 123-135.

12. Bhargavan K. et al. Cryptographically verified implementations for TLS. In Proc. of the 15th ACM conference on Computer and communications security, 2008, pp. 459-468.

13. Needham R. M., Schroeder M. D. Using encryption for authentication in large networks of computers. Communications of the ACM, vol. 21, №. 12, 1978. pp. 993-999.

14. Capek P., Kral E., Senkerik R. Towards an empirical analysis of. NET framework and C# language features' adoption. In Proc. of the 2015 International Conference on Computational Science and Computational Intelligence (CSCI), 2015, pp. 865-866.

15. Babenko L., Pisarev I. Distributed E-Voting System Based On Blind Intermediaries Using Homomorphic Encryption. In Proc. of the 11th International Conference on Security of Information and Networks, 2018.

16. Viganò L. Automated security protocol analysis with the AVISPA tool. Electronic Notes in Theoretical Computer Science, vol. 155, № 12, 2006, pp. 61-86.

17. Cremers C. J. F. The scyther tool: Verification, falsification, and analysis of security protocols. In Proc. of the International Conference on Computer Aided Verification, 2008, pp. 414-418.

18. Küsters R., Truderung T. Using ProVerif to analyze protocols with Diffie-Hellman exponentiation. In Proc. of the 22nd IEEE Computer Security Foundations Symposium, 2009, pp. 157-171.