This paper proposes a time-controlled data destruction scheme based on AONT-CTR encryption and smart contracts to address the challenges of achieving trusted data destruction and preventing data leakage. The study first explores the All-Or-Nothing Transformation (AONT) in data preprocessing and compares different operating modes of the AES algorithm. Building on this foundation, the paper introduces the AONT-CTR encryption method, which offers strong indivisibility. A data destruction strategy is then designed, based on data overwriting standards and smart contracts, which narrows the scope of destruction from the entire dataset to key information, such as the encrypted data header and encrypted keys. By overwriting these critical components, complete data destruction is ensured. Experimental results demonstrate that the proposed scheme provides both superior reliability and performance compared to conventional data destruction methods. When destroying 1,000 data files, the proposed method consumes only 56% of the time required by traditional approaches, confirming its efficiency and feasibility.

With the rapid increase in the number of online users and the inadequacies of digital identity technology, a series of challenges have emerged. Blockchain, with its distributed data storage, consensus mechanisms, and encryption algorithms, offers new solutions to the problems of digital identity management. Consequently, this paper proposes a blockchain-based digital identity management mechanism to address data isolation issues arising from the complexities of identity account management. Additionally, it introduces a data permission management mechanism that combines CP-ABE with blockchain to tackle the limitations of traditional identity authentication technologies regarding user data control. Experimental results demonstrate that the proposed algorithm performs well in terms of latency, throughput, and security.

This paper presents a bionic foldable wing that imitates the hind wing of ladybirds. Based on the folding mechanism of the hind wing of ladybirds and the theory of origami, the motion model of the bionic foldable wing is established, yield the motion law of the crease angles and the variation relationship between the panels are obtained. Bionic foldable wings utilise shape memory alloy to drive wings to fold, and embedded torsion springs to release energy to realize the function of wing unfolding. In the experiments of the vehicle equipped with foldable wings, the lift and attitude torque of bionic foldable wings are measured by the F/T sensor. The experimental results indicated that its aerodynamic performance is basically close to that of our optimized non-foldable wings. Moreover, the vehicle with foldable wings has been able to overcome gravity to achieve flight, which provides a novel concept for the research on flapping wing.

Blockchain applications, especially DeFi, frequently require off-chain data through oracles. Distributed oracles have higher security, but the system is also more complex. This paper designs a unified formal description method for the communication process, security protocol, data aggregation and other related procedures and protocols of the oracle. This method has no ambiguity and has a high logical description ability. Therefore, it has good convertibility with Event-B and some other formal verification tools, as well as logic methods such as first-order logic, set theory, and CTL, which can provide a basis for technical personnel to establish formal models, protocol development, and implementation. The paper defines and analyzes this protocol description method and presents examples of some core protocols.

Smart contract is a trusted service provided on the blockchain, while cloud service is a traditional service mode with a large number of resources. The combination of the blockchain and cloud service is of great significance to the trusted expansion of services and the access to services inside and outside the blockchain. In this paper, we study the smart contract extension service in blockchain-cloud collaborative computing. The service module decoupling method of smart contract is proposed, and the parallel execution algorithm of smart contract service is designed, which improves the execution efficiency of smart contract service. Finally, this paper designs a secure data interaction method of smart contract and cloud service, which helps to maintain the data consistency between cloud computing and blockchain. The experimental results show that the proposed method can save at most 42.13% of the running time, and it can promote the data consistency between the cloud service and the blockchain.

Blockchain is an innovative application of distributed storage, consensus algorithm, encryption algorithm, and other computer technologies. The consensus algorithm is the key to keep consistent among blockchain nodes. In most existing consensus algorithms, the leader node is responsible for proposing new block and communicating with other nodes. The leader node is easy to be the target of malicious attackers. With the increase of the number of nodes, the throughput and scalability of the blockchain system are also unsatisfactory. To address such issues, we propose the AnonymousFox consensus algorithm, which is suitable for the consortium blockchain and private blockchain. First, we design an anonymous leader node sorting algorithm, which hides the identity of the leader node through a variety of encryption algorithms. It periodically changes the ordered leader list to hide the target of malicious attackers. In addition, we design a consensus algorithm based on the anonymous identity of the leader node. Through one-to-many message communication, the amount of messages is greatly reduced. The complexity of the algorithm is$O(n)$. It solves the problem of ordered replication of state machines when the leader node is anonymous. We analyze the algorithm, it ensures safety and liveness when the fault nodes are less than one-third of the total. We evaluate the throughput, latency, scalability, resource consumption, exception processing, smart contract, and blockchain network through experiments. The throughput of the proposed algorithm is 49.3% higher than that of the practical Byzantine fault tolerance (PBFT) algorithm. The experimental results show that the proposed algorithm has high performance and scalability.

Smart contracts are the artifact of the blockchain that provides immutable and verifiable specifications of physical transactions. Solidity is a domain-specific programming language with the purpose of defining smart contracts. It aims at reducing the transaction costs occasioned by the execution of contracts on the distributed ledgers such as Ethereum. However, Solidity contracts need to adhere to safety and security requirements that require formal verification and certification. This paper proposes a method to meet such requirements by translating Solidity contracts to Event-B models, supporting certification. To that purpose, we define a restrained Solidity subset and a transfer function that translates Solidity contracts to Event-B models. Besides, we have implemented a translator to improve the conversion efficiency. As a case study, we take advantage of Event-B method capabilities to simulate models at different levels of abstraction and to express the properties of a typical smart contract: Honeypot contract. Lastly, we verify the generated proof obligations of the Event-B model with the help of the Rodin platform.

The cover image is based on the Original Article Verification Algebra for Multi-Tenant Applications in VaaS Architecture by Kan Luo et al., https://doi.org/10.1002/stvr.1763.

Summary This paper proposes an algebraic system, verification algebra (VA), for reducing the number of component combinations to be verified in multi‐tenant architecture (MTA). MTA is a design architecture used in SaaS (Software‐as‐a‐Service) where a tenant can customize its applications by integrating services already stored in the SaaS databases or newly supplied services. Similar to SaaS, VaaS (Verification‐as‐a‐Service) is a verification service in a cloud that leverages the computing power offered by a cloud environment with automated provisioning, scalability and service composition. In VaaS architecture, however, there is a challenging problem called ‘combinatorial explosion’ that it is difficult to verify a large number of compositions constructed by both quantities of components and various combination structures even with computing resources in cloud. This paper proposes rules to emerge combinations status for future verification, on the basis of the existing results. Both composition patterns and properties are considered and analysed in VA rules.

The published online cover has been updated.

A smart contract is a computable protocol that automatically enforces contract terms in a computer, transforming real-world contract terms into digital promises of the virtual world. Early smart contracts have been stuck in the theoretical phase due to the lack of a credible execution environment and the means to control digital assets. With the emergence of blockchain technology, it has solved the problems mentioned above. Smart contracts are stored on blockchain, ensuring the credibility of contract execution through the joint execution of contracts by the various nodes in the blockchain network. However, the current technology of blockchain-based smart contracts is still not mature enough and faces many major challenges. Among them, the extensibility and performance of smart contracts are the most important and most concerned ones. This paper studies the extensibility and performance of smart contracts by combining blockchain-based smart contracts with cloud technologies to address the extensibility and performance issues of smart contracts. Combined with micro-service technology, a new type of smart contract architecture is proposed, and then the key technologies in each layer of the architecture are further studied.

Digital Currency for Central Bank is becoming an important policy for country. CBDC (Central Bank Digital Currency) model should take advantages in the supervision, payment and consumption. Blockchain possesses the feature of de-centrality, tamper-resistant, and traceability. So this paper attempts to use the blockchain as the fundamental technology of CBDC. However, the challenges such as the protection for users privacy, supervision and transaction speed should be overcome. This paper proposes a CBDC model called MBDC which is based on the permission blockchain technology. The model makes use of the multi-blockchain architecture and ChainID to improve the models scalability and process payments more quickly. In this model, central bank and commercial banks and other agencies build and maintain the blockchain. On one hand, central bank could master the issuance of currency. On the other hand, relying on the user account address protocol, central bank could separate the users identity and transaction information. In this way, central bank could avoid double-spending issues and protect users privacy. In addition, the establishment of DC (Data Center) and layers of supervision provide strong supervision for the model. Finally, we also demonstrate, both theoretically and experimentally, the performance of model on the scalability and the speed of transaction execution etc.

Testing-as-a-Service (TaaS) is a software testing service in a cloud that can leverage the computation power provided by the cloud. Specifically, a TaaS can be scaled to large and dynamic workloads, executed in a distributed environment with hundreds of thousands of processors, and these processors may support concurrent and distributed test execution and analysis. This paper proposes an autonomous decentralized combinatorial testing system based on Adaptive Reasoning (AR) and Test Algebra (TA) for Combinatorial Testing (CT). AR performs testing and identifies faulty interactions, and TA eliminates related configurations from testing and there can be carried out concurrently. By combining these two, it is possible to perform large CT. We performed experiments with 2^10 components and 98:34% of configurations have been eliminated out of total number of configurations by AR and TA analysis.

SIGNAL belongs to the synchronous languages family. Such languages are widely used in the design of safety-critical real-time systems such as avionics, space systems, and nuclear power plants. This paper reports a key step of a verified SIGNAL compiler prototype, that is the transformation from a subset of SIGNAL to S-CGA (a variant of clocked guarded actions) and the proof of semantics preservation. Compared with the existing SIGNAL compiler, we use clocked guarded actions as the intermediate representation, to integrate more synchronous programs into our verified compiler prototype in the future. However, in contrast to the SIGNAL language, clocked guarded actions can evaluate a variable even if its clock does not hold. Thus, we propose a variant of clocked guarded actions, namely S-CGA, which constrains variable accesses as done by SIGNAL. To conform with the revised semantics of clocked guarded actions, we also do some adjustments on the existing translation rules from SIGNAL to clocked guarded actions. Finally, the verified transformation is mechanized in the theorem prover Coq.

The analysis and verification of an AADL model usually requires its transformation into the meta-model of this model-checker or that schedulability analysis tool. However, one challenging problem is to prove that the transformation into the target model of computation (MoC) preserves the semantics of the original AADL model or at least some of its properties. Moreover, the AADL standard lacks a formal semantics to make the validation of this translation possible. Albeit some of the related works give informal explanations on the model transformations they apply to interpret or compile AADL, the formal proof of semantics preservation remains in most cases altogether impossible. Our contribution is to bridge this gap by providing two formal semantics for a synchronous subset of AADL, which includes periodic threads and data port communications. Its operational semantics is formalized as a TTS (Timed Transition System). This formalization is one prerequisite to the formal proof of semantics preservation for our model transformation from AADL sources to our target verification formalism: TASM (Timed Abstract State Machine). In this paper, an abstract syntax of (our subset of) AADL is given, together with the abstract syntax of TASM. The translation is formalized by a family of semantics functions, which associates each AADL construct to a TASM fragment. Then, the proof of simulation equivalence between the TTSs of the AADL and the TASM models is formalized and mechanized using the proof assistant Coq.

AADL is an Architecture Description Language which describes embedded real-time systems. Behavior annex is an extension of the dispatch mechanism of AADL execution model. This paper proposes a formal semantics for the AADL behavior annex using Timed Abstract State Machine (TASM). Firstly, the semantics of AADL default execution model is given, and then we formally define some aspects semantics of behavior annex. A prototype of real-time behavior modeling and verification is proposed, and finally, a case study will be given to validate the feasibility.

This paper presents some real-time concepts as they are found in the AADL language and proposes their expression in two formalisms suitable for formal analysis: FIACRE which is based on timed transition systems and TASM which extends abstract state machines with resource consumption mechanisms.