LLM-based Generation of Formal Specification for Run-time Security Monitoring of ICS

Industrial Control Systems (ICS) are vulnerable to cybersecurity threats due to their distributed architecture and critical role in infrastructure sectors. Ensuring their secure operation requires deploying runtime monitoring mechanisms to detect behavioral deviations, with inline security monitoring arising as a practical solution. However, writing these specifications manually is time-consuming, error-prone, and requires deep domain expertise. In this paper, we explore the feasibility of using large language models (LLMs) to assist in generating JML-based inline security monitors for ICS applications. Using a water distribution system as a testbed, we prompt the model with structured templates and evaluate its output against expertwritten specifications. Our results highlight that LLMs can correctly infer key security properties and produce contextaware assertions with minimal guidance, marking an early but promising step toward automated monitor synthesis.

Authors

Institutions

Publication Details

Published
2025-08-04
DOI
https://doi.org/10.1109/csr64739.2025.11130130
Citations
4
Primary Topic
Embedded Systems Design Techniques
Type
article
Field-Weighted Citation Impact
9.08
Controls
|||
ALL TIME
JAN
FEB
MAR
APR
MAY
JUN
JUL
AUG
SEP
OCT
article

LLM-based Generation of Formal Specification for Run-time Security Monitoring of ICS

Muhammad Taimoor Khan, Dimitrios Serpanos, George E. Raptis, Christos Koulamas
4 citations
Embedded Systems Design Techniques
9.08
article

LLM-based Generation of Formal Specification for Run-time Security Monitoring of ICS

Muhammad Taimoor Khan, Dimitrios Serpanos, George E. Raptis, Christos Koulamas
article en
4 citations

Abstract

Industrial Control Systems (ICS) are vulnerable to cybersecurity threats due to their distributed architecture and critical role in infrastructure sectors. Ensuring their secure operation requires deploying runtime monitoring mechanisms to detect behavioral deviations, with inline security monitoring arising as a practical solution. However, writing these specifications manually is time-consuming, error-prone, and requires deep domain expertise. In this paper, we explore the feasibility of using large language models (LLMs) to assist in generating JML-based inline security monitors for ICS applications. Using a water distribution system as a testbed, we prompt the model with structured templates and evaluate its output against expertwritten specifications. Our results highlight that LLMs can correctly infer key security properties and produce contextaware assertions with minimal guidance, marking an early but promising step toward automated monitor synthesis.

Computer Technology Institute and Press “DIOPHANTUS” (GR), Industrial Systems Institute (GR), University of Greenwich (GB)
Openalex Percentile: Top 2%
Embedded Systems Design Techniques
9.08
AI Navigator

Ask Laika to Summarize, Analyze, and Connect papers live on the map.

Summarize Papers & Methodologies

Extract key findings, datasets, and comparative methods across publications.

Benchmark Rankings & Visual Analytics

Rank top research institutions, authors, funders, topics, and journals by Field-Weighted Citation Impact (FWCI) and paper volume with instant charts.

Connect Distant Disciplines

Bridge topological clusters on the map to find hidden collaborative intersections.