Model checking for real-time attack detection in water distribution systems

Системы распределения воды представляют собой критическую инфраструктуру. Эти архитектуры очень важны, и нестандартное поведение может отразиться на безопасности человека. Фактически, злоумышленник, получивший контроль над такой архитектурой, может нанести множество повреждений как инфраструктуре, так и людям. В этой статье мы предлагаем подход к выявлению нестандартного поведения, ориентированного на системы распределения воды. Разработанный подход рассматривает формальную среду проверки. Журналы, полученные из систем распределения воды, анализируются в формальную модель, и, используя временную логику, мы характеризуем поведение системы распределения воды во время атаки. Оценка, относящаяся к системе распределения воды, подтвердила эффективность разработанного подхода при выявлении трех различных нестандартных режимов работы.