C# parser for extracting cryptographic protocols structure from source code

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