Raptis, G. E., Khan, M. T. ORCID: https://orcid.org/0000-0002-5752-6420, Koulamas, C. and Serpanos, D. (2025) Synthesizing inline security monitors for ICS using Generative AI and FormalBench. In: IECON 2025: 51st Annual Conference of the IEEE Industrial Electronics Society 14th - 17th Oct. 2025. IEEE Xplore . Institute of Electrical and Electronics Engineers, Inc. (IEEE), Piscataway, New Jersey, pp. 1-6. (doi:10.1109/IECON58223.2025.11221437)

PDF (Conference Paper) 51788 KHAN_Synthesizing_Inline_Security_Monitors_For_ICS_Using_Generative_AI_And_FormalBench_(VoR)_2025.pdf - Published Version Restricted to Repository staff only Download (1MB) | Request a copy

Abstract

Industrial Control Systems (ICS) increasingly face cybersecurity threats due to their distributed architecture and critical role in infrastructure operations. We adopt inline security monitoring as a practical run-time verification strategy to address these risks. However, authoring formal specifications remains time-consuming and error-prone, requiring deep domain expertise. In this paper, we explore how large language models (LLMs) can support the synthesis of inline security monitors by generating Java Modeling Language (JML) specifications for distributed ICS applications. We use a water distribution system (WDS) as our testbed and FormalBench to generate prompts to guide the GPT-4o model in producing JML annotations. We then evaluate these outputs using the FormalBench framework. Our findings show that LLMs capture key security properties and generate context-aware assertions with minimal intervention, taking a first step toward automating the specification process and enhancing the security and resilience of distributed ICS environments.

Item Type:	Conference Proceedings
Title of Proceedings:	IECON 2025: 51st Annual Conference of the IEEE Industrial Electronics Society 14th - 17th Oct. 2025
Uncontrolled Keywords:	training, Java, Generative AI, large language models, industrial control, robustness, security, formal specifications, integrated circuit modeling, monitoring, industrial Control Systems (ICS), security monitoring;inline monitors;formal specification, generative AI, large language models (LLMs), Java Modeling Language (JML); cyber-physical systems, run-time verification, water distribution systems
Subjects:	Q Science > Q Science (General) Q Science > QA Mathematics Q Science > QA Mathematics > QA75 Electronic computers. Computer science
Faculty / School / Research Centre / Research Group:	Faculty of Engineering & Science Faculty of Engineering & Science > School of Computing & Mathematical Sciences (CMS)
Last Modified:	26 Nov 2025 15:06
URI:	https://gala.gre.ac.uk/id/eprint/51788

Actions (login required)

View Item

Downloads