Jul 2026· Annual International Computer Software and Applications Conference· pp. 2100-2105· 0 citations· 11 references
Abstract
The Cisco Packet Tracer (CPT) is a network and IoT systems design and simulation tool developed by Cisco Systems inc. The tool is widely used in academia and the industry to develop and simulate complex IoT systems for training purposes. Although the graphical notations of CPT are appealing to system developers, the tool does not support formal verification. Therefore, CPT is limited when it comes to the design and development of safety and secutiry critical IoT systems where faults can endanger people's lives or damage properties and businesses. This paper proposes a formal approach to the verification of IoT system models designed in the CPT tool, based on the Calculus of Context-aware Ambients (CCA). First, the graphical notations of CPT are mapped to processes in CCA that specify their behaviours. Then any desired property of a system can be specified as a Linear Temporal Logic (LTL) formula. Finally, the CCA Runtime Verification tool ccaRV is used to verify formally whether the behaviour of an IoT system model designed in CPT violates the system's requirements. The pragmatics of the proposed approach is illustrated using a case study.
Internet of Medical Things (IoMT) systems involve many interconnected devices that continuously collect, process, and share sensitive health data, creating significant privacy risks. Ensuring that these systems comply with GDPR is particularly challenging because legal requirements are complex, often timedependent, and difficult to validate at the level of individual data operations. This paper addresses this challenge by proposing a new formal verification approach that models the main IoMT operations, including data collection, transfer, storage, processing, and automated decision-making, as a GDPR-aware timed automaton. The proposed approach encodes legal requirements as formal rules and verifies compliance using a model checker through safety, liveness, and reachability properties. A remote cardiac monitoring scenario is presented to demonstrate typical data flows and interactions among smart medical devices, with business process models to represent the system. Experimental results show that the approach remains efficient as system complexity increases, providing a practical solution for developing IoMT applications that integrate privacy-by-design principles from the outset.
Masoud Barati· International Conference on...· 0 citations
Internet of Things (IoT) and edge systems induce complex, heterogeneous, and distributed environments where interconnected physical devices and localized computing resources exhibit intricate behaviors. Specifying behavioral requirements in such systems is inherently challenging. Temporal logic, notably Linear Temporal Logic (LTL), is widely adopted for their formal specification, serving as a critical precursor to, e.g., verification or synthesis. This paper systematically investigates scientific literature spanning the past decade. We collect requirements and their corresponding LTL properties, analyzing trends in LTL specification within edge/IoT systems over time. Subsequently, we automatically extract defining features of these requirements and properties, including formula complexity and natural-language characteristics, and analyze their correlations. The insights we derive offer a valuable resource for researchers and practitioners engaged in reasoning within edge/IoT systems. Beyond serving as a reference corpus, the dataset can aid evaluation and validation of other approaches developed by the formal methods community, or serve as training data for machine learning techniques targeting the formalization process.
Angeliki Pantiora, Roman Bögli, Timo Kehrer et al.· Annual International Compute...· 0 citations
Many cloud providers for IoT technologies offer access control mechanisms whose proper configuration is critical for security. However, verifying permissions in isolation is insufficient in a setting where devices have different levels of trust or are compartmentalised in various subsystems. This work analyses IoT access control policies to identify potential security vulnerabilities from unwanted information flow between devices. To this end, we formally model AWS IoT Core's components and define an information flow graph to capture the communication among devices permitted by the access control policies. We build a finite representation of the graph by leveraging an SMT solver, thus enabling the verification of information flow between devices. We implement our approach in a tool called IOT:POKER, and assess it on a realistic scenario and several real-world policies.
Lorenzo Ceragioli, Letterio Galletta, E. Lunati· 0 citations
As fifth-generation (5G) networks evolve toward open and software-based architectures, security verification of the NG Application Protocol (NGAP) between the radio access network and the 5G core has become increasingly important. This paper proposes a stateful security verification methodology that combines stateful fuzzing with specification-guided security verification. The methodology derives an Access and Mobility Management Function (AMF) state model, mutation types, and expected behaviors from Third Generation Partnership Project (3GPP) specifications. For each attack scenario, it establishes the required connection state through normal NGAP procedures, injects a mutated message, and compares the observed AMF responses and processing logs with the specification-defined expected behavior. We evaluated four open-source 5G core implementations using 324 attack scenarios per implementation, resulting in 1296 tests. Of these, 877 produced sufficient evidence to interpret the AMF processing outcome, yielding an interpretable outcome rate of 67.7%. The evaluation covered 27 of the 40 uplink NGAP message types and identified 32 specification violations, including 11 security vulnerabilities, none of which caused a core to crash. These results demonstrate the importance of jointly considering connection states and specification-defined behavior in NGAP security verification.
Seungjoon Na, Hwankuk Kim· Italian National Conference...· 0 citations
A formal verification framework that consists of a combination of specifications of temporal logic, model checking and modeling of service interactions graphs to study the behavior of the system and confirm the correctness properties is suggested.
Aparna S. Patil, Pratibha V. Kashid, Sourabh Rungta et al.· Journal of Intelligent Decis...· 0 citations
Internet of Things (IoT) devices heavily rely on lightweight communication protocols such as MQTT, CoAP, and 6LoWPAN. To minimize memory footprint and computational overhead, these protocols are often implemented using custom C/C++ code, making them highly susceptible to memory corruption vulnerabilities including buffer overflows and integer underflows. Traditional automated testing techniques, such as coverage-guided fuzzing and standard symbolic execution, struggle to effectively explore the deep state spaces of these protocols due to the complex, stateful nature of network handshakes and the path explosion problem. In this paper, we propose ProtoSym, a novel State-Aware Hybrid Concrete-Symbolic Engine designed specifically for IoT protocol vulnerability discovery. Our approach synergistically combines directed concrete execution to navigate complex network state machines with selective symbolic execution to rigorously solve constraints within packet payloads, effectively finding deep-seated security flaws in IoT gateway firmware. We introduce a formal theoretical framework that models protocol states and transitions, enabling precise constraint formulation, and present a directed path exploration strategy that mitigates path explosion while maximizing state coverage. Experimental evaluation on widely-used IoT protocol implementations demonstrates that ProtoSym achieves up to 46.7% higher statespace coverage and discovers $3.7 \times$ more unique vulnerabilities compared to state-of-the-art baselines.
Gautham Koorma, Isaac Pflaum, Radostin Pachamanov et al.· International Conference on...· 0 citations
