Synthesizing Inline Security Monitors for ICS Using Generative AI and FormalBench

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.