Towards formal verification of cyber security standards

Стандарты кибербезопасности часто используются для обеспечения защищенности промышленных систем управления. В последнее время такие системы становятся все более децентрализованными, что делает их все более уязвимыми для разного рода кибератак. Одна из проблем реализации стандартов кибербезопасности в промышленных системах управления состоит в том, что невозможно своевременно проверить, соответствуют ли разрабатываемые системы этим стандартам или нет. Помимо прочего, соответствие стандарту кибербезопасности только валидируется, а не верифицируется формально, что, как правило, не дает убедительных доказательств правильного использования стандарта. В статье предлагается подход, в котором проверка защищенности промышленных систем управления осуществляется путем формального анализа. Подход состоит в следующем: определяются строительные блоки, необходимые для формального описания системы; составляется формальная модель системы; модель анализируется с помощью инструмента Alloy Analyzer. Предлагаемый подход может использоваться на ранних стадиях проектирования, где проблемы не так дороги для исправления. Чтобы показать применимость подхода, были смоделированы две кибератаки, а также стратегии противодействия им. Подход был также оценен на предмет гибкости - возможности совмещения разных аспектов стандартов кибербезопасности. В статье также обсуждаются будущие направления исследования