A Secure and Computable Blockchain-Based Data Sharing Scheme in IoT System

The internet of things (IoT) devices are expected to collect vast amounts of data that support different kinds of applications such as health monitor, smart home, and traffic management. However, its characteristics such as resource-constrained nature, dynamicity, and large-scale growth bring challenges to secure IoT data sharing. Nowadays, blockchain-based ciphertext-policy attribute-based encryption (CP-ABE) was proposed to realize secure IoT data sharing. In blockchain-based CP-ABE data sharing schemes, the data are encrypted and stored in the cloud. Once users want to process the data, they should download and then decrypt the ciphertext in the client-end, and after processing the data, users encrypt and upload the ciphertext onto the cloud. This outweighs the advantage of using cloud computing resources. Fully homomorphic encryption (FHE) and homomorphic signature technology may be adopted to realize ciphertext computation and for correctness checking of ciphertext computation results. In this paper, we propose a secure and computable IoT data sharing system to ensure users enjoying the computation convenience of the cloud-end. Specifically, the proposed system integrates CP-ABE and FHE to realize secure IoT data sharing and ciphertext computation. In addition, we generated homomorphic signatures of ciphertexts to enable users to check the correctness of the ciphertext computation results. Moreover, to supervise the cloud, providing the honest IoT data access control, storage, and computing services for users, we recorded the access policy of the data, the hash of the data, the signature of the ciphertext, and the homomorphic signature of the ciphertext on the blockchain. The performance evaluation and security analysis show the proposed scheme is practical and secure.

A Correctness Checking Approach for Collaborative Business Processes in the Cloud

With the increasing popularity of cloud computing, especially the emergence of Business Process as a Service (BPaaS), more and more enterprises construct their process collaborations based on BPaaS services. Indeed, the collaborative business process built by BPaaS services can be seen as a complex system, as it covers multiple business processes (i.e., BPaaS services) and they act independently. Since business processes corresponding to BPaaS services are usually provided by different cloud service providers, and their interactions are unforeseen in advance, in actual execution, some behavioral anomalies (e.g., deadlocks) may occur. To this end, based on BPaaS services, we propose an approach to build process collaborations in the cloud. In this approach, we first model collaborative business processes using open nets. Then, we check their correctness based on stubborn sets. Finally, in case they are partially correct, we generate reliable paths for the coordination execution between business processes. Our approach is implemented in the PIPE (an open tool for Petri nets) and evaluated on actual cases that show its effectiveness and efficiency.

Formal Verification of Three-Valued Digital Waveforms

We investigate a formal verification problem (mathematically rigorous correctness checking) for digital waveforms used in practical development of digital microelectronic devices (digital circuits) at early design stages. According to modern methodologies, a digital circuit design starts at high abstraction levels provided by hardware description languages (HDLs). One of essential steps of an HDLbased circuit design is an HDL code debug, similar to the same step of program development in means and importance. A popular way of an HDL code debug is based on extraction and analysis of a waveform, which is a collection of plots for digital signals: functional descriptions of value changes related to selected circuit places in real time. We propose mathematical means for automation of correctness checking for such waveforms based on notions and methods of formal verification against temporal logic formulae, and focus on such typical featues of HDL-related digital signals and corresponding (informal) properties, such as real time, three-valuededness, and presence of signal edges. The three-valuededness means that at any given time, besides basic logical values 0 and 1, a signal may have a special undefined value: one of the values 0 and 1, but which one of them is either not known, or not important. An edge point of a signal is a time point at which the signal changes its value. The main results are mathematical notions, propositions, and algorithms which allow to formalize and solve a formal verification problem for considered waveforms, including: definitions for signals and waveforms which the mentioned typical digital signal features; a temporal logic suitable for formalization of waveform correctness properties, and a related verification problem statement; a solution technique for the verification problem, which is based on reduction to signal transfromation and analysis; a corresponding verification algorithm together with its correctness proof and “reasonable” complexity bounds.