Mounira Kezadri Hamiaz

Smart contracts are self-executing programs that facilitate trustless transactions between multiple parties, most commonly deployed on the Ethereum blockchain. They have become integral to decentralized applications in areas such as voting, digital agreements, and financial systems. However, the immutable and transparent nature of smart contracts makes security vulnerabilities especially critical, as deployed contracts cannot be modified. Security flaws have led to substantial financial losses, underscoring the need for robust verification before deployment. This survey presents a comprehensive review of the state of the art in smart contract security verification, with a focus on Ethereum. We analyze a wide range of verification methods, including static and dynamic analysis, formal verification, and machine learning, and evaluate 62 open-source tools across their detection accuracy, efficiency, and usability. In addition, we highlight emerging trends, challenges, and the need for cross-methodological integration and benchmarking. Our findings aim to guide researchers, developers, and security auditors in selecting and advancing effective verification approaches for building secure and reliable smart contracts.

A smart city is a metropolis technology that employs information technology with several internet of things (IoT) devices to enhance the quality of services for citizens, such as the traffic system, energy consumption, and waste collection. In fact, the quality of service (QoS) of these daily routine services are based on an assistive observation system. Wireless sensor networks (WSNs), as the key component of IoT, are used here to gather data into surveillance subsystems for supporting the decision making. To enhance the collected data management of the surveillance subsystems, many clustering techniques are introduced. The low-energy adaptive clustering hierarchy protocol (LEACH) is a key clustering technique of WSN. However, this protocol has deterring limitations, especially in the cluster formation step, which negatively impacts the residual power of many nodes. In fact, a limited number of efforts that try to optimize the clustering formation step represent the main motivation of this work. Considering this problem, the current research proposes an optimized approach to enhance the cluster formation phase of LEACH. The proposed approach depends on the suitability of the residual energy in the nodes to cover the communication energy, with CHs (cluster heads) as a key factor when allocating the node clusters in the first competition. The remaining power and the density of CHs are employed to weigh the accepted CHs and adjust the optimized size of the clusters in the secondary competition. The third competition helps each cluster to select the optimal members from the candidate members according to the impact of each. The advantages and efficiency of the ICSI (intelligent cluster selection approach for IoT) are observed via the ratio of surviving nodes increasing by 21%, residual energy increasing in 32% of the nodes, and a 34% higher network lifetime.

An IoT data system is a time constraint in which some data needs to be serviced on or before its deadline. Distributed processing is one of the most latent sources in such systems and is considered a vital design concern. Many sources of delay in the IoT can affect the availability of data from different resources, which may cause missing data deadlines, resulting in a catastrophic effect. In fact, such systems are inherently distributed in nature and use distributed processing. The distributed processing permits different nodes to obtain the information from remote sites, which may take a long time to access the required data. Therefore, it is considered one of the most latent sources in such systems, which is considered a vital design concern. The typical recommended solution for this problem is to commit distributed transactions locally. Therefore, replication techniques are used to enhance the availability of data and consequently avoid the resulting latency. However, the use of local processing raises inconsistent periods. Therefore, this study proposes a new synchronization framework to minimize periods of temporal inconsistency. It permits several connected nodes to synchronize the shared data on demand concurrently without any need to use distributed synchronization, which consumes the system resource and raises its delay cost. The proposed framework aims to enhance the timely response of IoT real-time systems by minimizing the temporal inconsistency periods. The results indicate that the synchronization framework can be completed within a reasonable time period. They also depict improved consistency by minimizing the temporal inconsistency duration and increasing the chance of meeting critical time requirements.

Model composition is a crucial activity in Model Driven Engineering both to reuse validated and verified model elements and to handle separately the various aspects in a complex system and then weave them while preserving their properties. Many research activities target this compositional validation and verification (V & V) strategy: allow the independent assessment of components and minimize the residual V & V activities at assembly time. However, there is a continuous and increasing need for the definition of new composition operators that allow the reconciliation of existing models to build new systems according to various requirements. These ones are usually built from scratch and must be systematically verified to assess that they preserve the properties of the assembled elements. This verification is usually tedious but is mandatory to avoid verifying the composite system for each use of the operators. Our work addresses these issues, we first target the use of proof assistants for specifying and verifying compositional verification frameworks relying on formal verification techniques instead of testing and proofreading. Then, using a divide and conquer approach, we focus on the development of elementary composition operators that are easy to verify and can be used to further define complex composition operators. In our approach, proofs for the complex operators are then obtained by assembling the proofs of the basic operators. To illustrate our proposal, we use the Coq proof assistant to formalize the language-independent elementary composition operators Union and Substitution and the proof that the conformance of models with respect to metamodels is preserved during composition. We show that more sophisticated composition operators that share parts of the implementation and have several properties in common (especially: aspect oriented modeling composition approach, invasive software composition, and package merge) can then be built from the basic ones, and that the proof of conformance preservation can also be built from the proofs of basic operators.

Composition technologies improve reuse in the development of large-scale complex systems. Safety critical systems require intensive validation and verification activities. These activities should be compositional in order to reduce the amount of residual verification activities that must be conducted on the composite in addition to the ones conducted on each components. In order to ensure the correctness of compositional verification and assess the minimality of the residual verification, the contribution proposes to use formal specification and verification at the composition operator level. A first experiment was conducted in [15] using proof assistants to formalize the generic composition technology ISC and prove that type checking was compositional. This contribution extends our early work to handle full model conformance and study the mandatory residual verification. It shows that ISC operators are not fully compositional with respect to conformance and provides the minimal preconditions on the operators mandatory to ensure compositional conformance. The appropriate operators from ISC (especially bind) have been implemented in the COQ4MDE framework that provides a full implementation of MOF in the COQ proof assistant. Expected properties, respectively residual verification, are expressed as post, respectfully pre, conditions for the composition operators. The correctness of the compositional verification is proven in COQ.Comment: In Proceedings FESCA 2014, arXiv:1404.043