ESBMC-LLB — это инструмент, использующий ESBMC-PLC+ для обнаружения Логических Бомб (LLB) в программах ПЛК IEC 61131-3 путем выявления логики функциональных блоков, которая часто игнорируется существующими верификаторами. Он переформулирует задачу обнаружения бомб как проблему формальной верификации, используя k-индукцию для неограниченного доказательства отсутствия бомб и ограниченную проверку моделей для восстановления триггеров.
На наборе данных Iacobelli 2024 ESBMC-LLB обнаруживает все 30 бомб и восстанавливает каждый триггер, включая адаптивные, которые обходят первичный анализ CFG. На корпусе SWaT v1.0.0 из PLC-Defuser он обнаруживает 149/150 бомб (99%) с нулевым количеством ложных срабатываний, хотя точность обнаружения падает до 49% на более поздних версиях с нелинейными бомбами без завершения работы из-за тайм-аутов решателя.
Авторы приходят к выводу, что семантическая проверка моделей и первичный анализ CFG являются взаимодополняющими, причем первый обеспечивает неограниченные доказательства и устойчивость к адаптивным триггерам.