Cloud computing supports the Internet of Things (IoT) in handling diverse and large-scale data. However, outsourcing data control to the cloud raises security concerns, particularly in key management. Although Ciphertext-Policy Attribute-Based Encryption (CP-ABE) preserves data confidentiality, it entrusts key management to a centralized attribute authority, resulting in the key escrow problem. Furthermore, existing CP-ABE schemes lack mechanisms for key verification and identity authentication, leaving IoT systems susceptible to key errors and impersonation attacks. To overcome these limitations, we propose Secure and User-autonomous Attribute-based Data Sharing (SUAD) for cloud-assisted IoT. The SUAD scheme transfers key management from the authority to data users themselves, thereby eliminating key escrow. Built on a data user-centric architecture, the SUAD scheme removes the decryption privilege of the attribute authority. To prevent key forgeries and operational errors, we design a correctness verification mechanism covering five critical keys and the decryption result, along with a two-way interactive authentication protocol based on the Schnorr scheme for reliable identity verification. The SUAD scheme further supports dynamic user management, enabling user logout, replacement, and joining while optimizing maintenance overhead through periodic updates. We formally prove that SUAD achieves selective IND-CCA security in the random oracle model. Both theoretical analysis and experimental evaluations demonstrate that SUAD enhances user autonomy and strengthens security without incurring additional encryption or decryption costs, confirming its practicality for IoT deployments.

Analyzing privacy breaches in Internet-based messaging applications is challenging due to overlapping and sometimes conflicting requirements such as confidentiality, anonymity, unlinkability, and user consent. Existing static analysis techniques typically target isolated aspects of privacy, limiting their scope. In this work, we introduce a static analysis framework based on a composite privacy model that captures the interdependencies among these requirements. This unified model enables the systematic identification of technical privacy violations and their associated legal implications, such as infringements of data protection laws and digital rights. We apply our framework to Ejabberd, a real-time communication server used in messaging platforms like WhatsApp. Our analysis focuses on confidentiality and consent-driven privacy concerns, including the right to be informed and the right to erasure. The results highlight the effectiveness of our approach in bridging technical analysis with legal accountability.

Privacy of Internet-based messaging applications involves establishing multiple requirements such as confidentiality, anonymity, pseudonymity, and consent, each typically addressed in isolation using different techniques. To the best of our knowledge, no unified framework supports the privacy analysis of these aspects together. Therefore, the main goal of our work is to detect privacy breaches based on a unified modelling of the relationship among the privacy requirements by static program analysis. In this paper, we present initial results on the privacy (i.e., confidentiality) analysis of Ejabberd server – an open-source XMPP backend server used by popular messaging applications like WhatsApp. Based on the confidentiality modelling, we perform a privacy analysis of key Ejabberd modules that are responsible for user authentication. The findings highlight the module implementations that involve potential privacy breaches and serve as a basis for our future work towards developing a unified privacy evaluation framework.

Over the past few years, the transition from centralized to distributed industrial control systems (ICS) has introduced new challenges related to coordination, communication reliability, and cybersecurity. These challenges include conditions such as deadlocks and livelocks, which adversaries can exploit to compromise ICS safety and availability. To ensure secure and resilient operations in distributed ICS, run-time monitoring must go beyond detection to include responsive recovery. In this paper, we extend the ASM2S framework, a model-based inline security monitoring approach, by integrating recovery capabilities directly into the monitoring loop. Our approach uses formal specifications to allow system behavior, threat conditions, and recovery actions to be explicitly defined and evaluated at run-time. We demonstrate the approach using a water distribution system use case. Our work enhances the run-time assurance of distributed ICS by enabling automatic detection and recovery from security violations, offering a robust foundation for self-healing critical infrastructure.

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.

The increasing complexity and decentralization of Industrial Control Systems (ICS) have expanded the attack surface for cyber-security threats, particularly in critical infrastructure domains. Inline monitoring using formal annotations like the Java Modeling Language (JML) offers a lightweight yet precise method to detect behavioral anomalies. However, the manual creation of such specifications is resource-intensive and requires domain expertise. This paper explores generative artificial intelligence (AI), specifically large language models (LLMs), to automate the synthesis of inline formal security monitors. We benchmark three state-of-the-art LLMs (GPT-4o, DeepSeek-V3, and Gemini 2.5 Flash) on their ability to generate JML annotations for ICS software drawn from the ASM2S water distribution system. Our evaluation across five dimensions (syntax, semantics, property coverage, alarm semantics, and effort savings) reveals distinct trade-offs. GPT-4o demonstrates strong syntactic and structural alignment with ASM2S, while DeepSeek-V3 offers richer behavioral modeling. Gemini 2.5 Flash showcases conceptual depth but introduces non-verifiable constructs. These findings demonstrate the potential of LLMs as co-pilots in secure-by-design ICS development and underscore the need for syntax-aware fine-tuning and interactive verification workflows.

In the decentralized Industrial Control Systems (ICS) era, water distribution systems (WDS) are critical in ensuring water safe and reliable delivery. However, their growing complexity, connectivity, and distributed nature expose them to cybersecurity risks. Renowned WDS software, like EPANET, lacks features to address such risks, which, however, can be addressed by complementary solutions, like ASM2S. In this paper, we compare the capabilities offered by these two tools and make a first step towards exploring their combination, aiming to equip WDS tools with enhanced hydraulic, water quality, and cybersecurity modeling and monitoring characteristics.

In the decentralized Industrial Control Systems (ICS) domain, water distribution systems (WDS) are critical in ensuring water safe and reliable delivery. However, their growing complexity, connectivity, and distributed nature expose them to cybersecurity risks. Run-time inline monitoring can address such risks. This paper focuses on implementing run-time inline security monitoring for deadlocks in WDS, providing examples and simulation results. The results indicate the run-time detection of deadlocks, enhancing WDS’s overall reliability and efficiency.

Over the past few years, there has been a noticeable transition from centralized Industrial Control Systems (ICS) to distributed systems. However, the challenges of distributed systems (e.g., communication delays and packet loss) can give rise to undesired situations like deadlocks, which malicious actors may target. To address such conditions, implementing run-time security monitoring can ensure these systems’ reliable and secure operation. In this paper, we introduce a novel approach for run-time security monitoring for distributed ICS, extending previous works that focus on autonomous and centralized systems. Our approach makes it possible to specify physical and cyber resources and their changing limitations within a distributed environment. By doing so, our approach offers a valuable contribution to ICS security by tackling limitations introduced by distributed ICS. Furthermore, it provides an efficient mechanism for monitoring the security of these systems in real time.

We present the initial results of developing a security risk analyzer for Internet of Things (IoT) applications that analyses both evitable and inevitable yet known and unknown cyber-attacks and as a result produces the adversarial strategies (multi-stages of attack) that can compromise the application. Our risk analyzer is rigorous and qualitative, performing technical analysis, as well as quantitative yet useful, identifying sub-attacks and their quantitative risks. In contrast, conventional security risk analyzers either provide too specific risk assessment or provide a too generic risk assessment of a given application. Such analyzers are typically not practical against constantly changing attacks of the variable extent and complex modern IoT applications. We demonstrate the usability of our methodology through the detection of an example attack model from a real-world incident in real-time.

Simulations have gained paramount importance in terms of software development for wireless sensor networks and have been a vital focus of the scientific community in this decade to provide efficient, secure, and safe communication in smart cities. Network Simulators are widely used for the development of safe and secure communication architectures in smart city. Therefore, in this technical survey report, we have conducted experimental comparisons among ten different simulation environments that can be used to simulate smart-city operations. We comprehensively analyze and compare simulators COOJA, NS-2 with framework Mannasim, NS-3, OMNeT++ with framework Castalia, WSNet, TOSSIM, J-Sim, GloMoSim, SENSE, and Avrora. These simulators have been run eight times each and comparison among them is critically scrutinized. The main objective behind this research paper is to assist developers and researchers in selecting the appropriate simulator against the scenario to provide safe and secure wired and wireless networks. In addition, we have discussed the supportive simulation environments, functions, and operating modes, wireless channel models, energy consumption models, physical, MAC, and network-layer protocols in detail. The selection of these simulation frameworks is based on features, literature, and important characteristics. Lastly, we conclude our work by providing a detailed comparison and describing the pros and cons of each simulator.

In this paper, we present our ongoing work to develop an efficient and scalable verification method to achieve runtime security of real-time applications with strict performance requirements. The method allows to specify (functional and non-functional) behaviour of a real-time application and a set of known attacks/threats. The challenge here is to prove that the runtime application execution is at the same time (i) correct w.r.t. the functional specification and (ii) protected against the specified set of attacks, without violating any non-functional specification (e.g., real-time performance). To address the challenge, first we classify the set of attacks into computational, data integrity and communication attacks. Second, we decompose each class into its declarative properties and definitive properties. A declarative property specifies an attack as a one big-step relation between initial and final state without considering intermediate states, while a definitive property specifies an attack as a composition of many small-step relations considering all intermediate states between initial and final state. Semantically, the declarative property of an attack is equivalent to its corresponding definitive property. Based on the decomposition and the adequate specification of underlying runtime environment (e.g., compiler, processor and operating system), we prove rigorously that the application execution in a particular runtime environment is protected against declarative properties without violating runtime performance specification of the application. Furthermore, from the specification, we generate a security monitor that assures that the application execution is secure against each class of attacks at runtime without hindering real-time performance of the application.

Industrial cyber-physical systems (ICPSs) are widely deployed in monitoring and control of the nation's critical industrial processes, such as water distribution networks and power grids. ICPSs are the tight integration of cyber (software) and physical entities connected via communication networks. Communication networks are typically realized via wireless channels to reduce the cost of wires and installation. However, they are also inherently unreliable, easy to disrupt, and subvert, which makes them a potential target for cyberattacks. The failure of communication can cause data loss or delays, which can compromise system functionality and have catastrophic consequences due to the strict real-time requirements of ICPSs. Current run-time security monitors protect ICPSs either at communication level (through network intrusion monitors) or at application level (through threat detection monitors). Such monitors are layer-specific and, thus, fail to detect advanced threats arising from the multilayer disruption. In this article, we present a multilayer run-time security monitor that can detect discrepancies caused by interdependent application and communication layer attacks and prevent their propagation into the system's control loops. We demonstrate the effectiveness of the approach via an example of the ICPS used for control and monitoring of a water distribution network.

Automated program repair has the potential to reduce the developers’ effort to fix errors in their code. In particular, modern programming languages, such as Java, C, and C#, represent time as integer variables that suffer from integer overflow, introducing subtle errors that are hard to discover and repair. Recent researches on automated program repair rely on test cases to discover failures to correct, making them suitable only for regression errors. We propose a new strategy to automatically repair programs that suffer from timestamp overflows that are manifested in comparison expressions. It unifies the benefits of static analysis and automatic program repair avoiding dependency on testing to identify and correct defected code. Our approach performs an abstract analysis over the time domain of a program using a Time Type System to identify the problematic comparison expressions. The repairing strategy rewrites the timestamp comparisons exploiting the binary representation of machine numbers to correct the code. We have validated the applicability of our approach with 20 open source Java projects. The results show that it is able to correctly repair all 246 identified errors. To further validate the reliability of our approach, we have proved the soundness of both, type system and repairing strategy. Furthermore, several patches for three open source projects have been acknowledged and accepted by their developers.

Machine learning (ML) based secure and autonomous cyber physical systems are often not reliable and interpretable mainly because the employed ML techniques suffer from false alarms that may result in physical and financial loss. We assert that reliability and interpret-ability of the ML methods depends on underlying statistical models that infer results. Therefore, we introduce a rigorous method for the model selection. Current selection methods choose a model using statistical criteria (e.g., AIC, BIC). These criteria may lead to selection of an inappropriate model (e.g. over/under-fitting) because they only consider relative-quality (statistical) of the model without considering absolute-quality (formal) of the model based on the model/data specification. To this end, we argue the suitability of recently developed-decidability procedures/solvers. Such solvers infer if a selected model can(not) classify a given data and produce a formal proof that can be used to assure reliability and security of modelled system. We demonstrate feasibility of the method through a simple example of an autonomous insulin pump.

Abstract Cyber physical system (CPS) applications are widely used to control critical infrastructure of various application domains, eg, medical health care, energy, and power, to name a few. Such applications usually take input data from sensors, estimate current state of the system, and then based on the estimation, make critical decisions to control the underlying infrastructure automatically. Therefore, security and integrity of the (system state) data are critically important to ensure safe operations of CPS. In this paper, we present a review of security of various data management systems used in CPS. Since CPS are composed of systems of (sub)systems that generate a huge amount of data (ie, periodical sensor input data), therefore, recently, NoSQL and NewSQL data management systems have emerged as popular data management systems to support efficient and scalable analysis of unstructured data. Unfortunately, these systems were not initially build for data security and thus are vulnerable to numerous security attacks. Considering flexible data model and efficient access methods in NoSQL and NewSQL, we discuss the security attacks on such data management systems and their corresponding solutions to mitigate them. In particular, we analyze the system and data security of popular NoSQL and NewSQL systems. To analyze that, we defined feature vectors for system and data security and compared the data systems against them. Finally, we propose security solutions for data management systems by identifying various security vulnerabilities in internal security algorithms of such systems.

The automatic verification of time properties of models extracted from programs is challenging, mainly because modern programming languages, such as Java, represent time without a proper semantics. Current approaches to extract time models from source code either represent time only as a tree-like sequence of events or require developers to manually provide a formal model of the time behavior. This makes it difficult for software developers to verify various aspects of their systems, such as timeouts, delays and periodicity of the execution. In this paper, we introduce a formal definition of the time semantics for the Java programming language. Based on the semantics, we present an approach to automatically extract timed automata and their time constraints from Java programs at method level. First, our approach detects the Java statements that involve time, from which it then extracts the timed automata. Our extracted automata are directly amenable to the verification of time properties of the corresponding Java methods. We evaluated the accuracy of our approach on twenty open source Java projects that implement time behavior in their source code. The results show that our approach achieves 100% precision and recall in identifying time related information. They also show that 95% of the timed automata extracted from source code correctly model the time behavior of the method. Finally, we show the applicability of our timed automata to identify eight real errors in four open source Apache systems.

Modern medical devices aim at providing invasive e-health care services to patients with long-term conditions. Typically, these services are implemented as embedded software applications that remotely and automatically control the operations of the devices according to the patient's condition as monitored by the underlying sensors. Such applications are neither safe nor secure mainly because of unreliable sensors, which may provide incorrect input data either due to its malfunctioning or due to some accidental (by privileged user) or intentional (by adversary) interference. Hence, the incorrect sensor data may lead to identification of inaccurate patient condition, which may threaten the patient's life. To ensure safety and security of e-health applications, current approaches employ data analysis techniques to monitor sensor data and alarm when some unusual value is detected and employ access control strategies to ensure that controller decisions are consistent with sensor input data. However, such approaches fail to detect stealthy attacks, e.g. bad data (false data injection) and bad computations because they do not understand what the application or device is trying to do. To this end, we evaluate our existing approach (i.e., ARMET) to assure safety and security of an emerging and critically real-time application domain of e-health. The approach is based on the specification of the application and device, which has a design and a run-time component. Given an application specification, the design component employs logical verification methods to assure that the application design is resilient to some bad data, i.e., there are no sensor input data values with meaningful threshold which are admissible to the specification but are not true. Given the specification, the runtime component monitors application's execution and assures that the execution is consistent with the specification and alarms whenever it detects a violation, i.e., there is a bad computation. We evaluate the methodology through its application to an example medical e-health application that controls and monitors blood glucose through an insulin pump.

In this paper, we introduce a design methodology to develop reliable and secure industrial control systems (ICSs) based on the behavior of their computational resources (i.e., process/application) and underlying physical resources (e.g., the controlled plant). The methodology has three independent, but complementary, components that employ novel approaches and techniques in the design of reliable and secure ICSs. First, we introduce reliable-and-secure-by-design development of secure industrial control applications through stepwise sound refinement of an executable specification, employing deductive synthesis to enforce functional and nonfunctional (e.g., security and safety) properties of ICS applications. Second, we present a runtime security monitor at the middleware level of ICSs that protects ICS operation in the field through comparison of the application execution and the application specification execution in real time; the runtime security monitor can be synthesized from the executable specification. Finally, based on the specification, we perform a vulnerability analysis for false data injection (FDI) attacks, which leads to ICS application designs that are resilient to this type of attacks. We demonstrate the methodology through its application to a basic and typical ICS example application, describing all the tools used and ARMET, the middleware monitor that constitutes the core component of the methodology.

The verification of the time behavior in distributed, multi-threaded programs is challenging, mainly because modern programming languages only provide means to represent time without a proper semantics. Current approaches to extract time models from source code represent time only as a sequence of events or require developers to manually provide a formal model of the time behavior. This makes it difficult for developers to verify various aspects of their systems, such as timeouts, delays and periodicity of the execution. In this paper, we introduce a definition of the time semantics of the Java programming language. Based on the semantics, we present an approach to automatically extract timed automata and their time constraints from the Java methods source code. First, we detect Java statements which involve time, from which we then extract the timed automata that are directly amenable to the verification of time properties of the methods. We evaluated the accuracy of our approach on ten open source Java projects that heavily use time in their source code. The results show a precision of 98.62% and recall of 95.37% in extracting time constraints from Java code. Finally, we demonstrate the effectiveness of our approach with five reported bugs of four different Apache systems that we could confirm.