## 2 Related Work
### Security Validation  
However, the aforementioned general composition methods do not take into consideration the special intrinsic of security. Theoretical works for secure system composition are presented in [36; 37; 38; 39]. In [36], the authors document a set of composition theorems which can prove protocols' security under standard stand-alone and compositional definitions of security. The study in [37] documents a formal validation of automated policy refinement. The analysis evaluates the management procedures in network security systems. It formally validates policy hierarchies for model-based management and propagates from an abstract level to its immediate lower neighbor. The outcomes are two theorems that ensure the compliance among the actual system behavior and the abstract design policies. In [38], methods of concurrent general composition and universal composability are examined on public-key models and scenarios with no trust infrastructure. Newer studies [39] update the security composition theory with properties like mitigation of eavesdropping and identity faking. Therefore, a modeling framework is proposed [39] for security verification and is applied in distributed and industrial IoT infrastructures. The framework performs model-checking techniques and the overall analysis is supported by the Alloy Analyzer [40]. Yet, theoretical works cannot be immediately applied in real and dynamic systems. Nevertheless, the deduced security and composition outcomes are considered by practical solutions and developed tools for more robust formal documentation.  
Also, in the field of Knowledge Representation and Reasoning event-driven model-based approaches are suggested to better express the dynamic behavior of the IoT ecosystem in a formal manner. Thus, security verification techniques are additionally proposed to tackle this issue (e.g., [41; 42; 43; 44]).  
SMoLES-SEC [41] integrates the Security Model Analysis Language (SMAL) [41] to the pure SMoLES. SMAL embodies security extensions to the DSML's meta-model composition and defines access control policies for IoT settings. However, the reasoning capabilities are bounded due to this constrained expressiveness. Also, SMoLES-SEC fails to define the security features which are valid after the composition as well as the overall security status of the composed setting.  
The study in [42] proposes a framework for runtime enforcement mechanisms. An analyzed system is modeled as an automaton. Then, the framework can track a sequence of states and events to derive wherever the security policy constraints are satisfied at runtime. The enforcement mechanism develops two main operations: (i) allows legal functionality without changes and (ii) blocks illegal functionality.  
A modeling and visualization tool for security evaluation and secure system management is presented in [43]. Threat modeling is applied in the composed setting for the evaluation of metrics at the architectural level. Then, hierarchical presentation of security metrics is performed based on decomposition methods for the measured security objectives, while deriving the overall security status.  
The work in [44] proposes IoT service secure composition verification based on Service Dependency Trees (SDTs). Each IoT device node builds its own SDT, denoting the external service nodes that the provided services are depending on. Also, each node may be aware of all recursive SDTs for its composed services. Henceforth, secure service composition can be assessed by permitting only integration with SDTs were all the paths and involved entities are considered trusted. However, constructing a SDT for a real IoT system is not ease, as well as, their consistency and trustworthiness in an actual complex and dynamically composed setting become challenging.