LiangJun Deng¹, Hang Lei¹, Zheng Yang¹, WeiZhong Qian^1,*, XiaoYu Li¹, Hao Wu², Sihao Deng³, RuChao Sha¹, WeiDong Deng⁴

Computer Systems Science and Engineering, Vol.45, No.2, pp. 2155-2170, 2023, DOI:10.32604/csse.2023.027680

Abstract In order to realize a general-purpose automatic formal verification platform based on WebAssembly technology as a web service (FVPS), which aims to provide an automated report of vulnerability detections, this work builds a Hyperledger Fabric blockchain runtime model. It proposes an optimized methodology of the functional equivalent translation from source program languages to formal languages. This methodology utilizes an external application programming interface (API) table to replace the source codes in compilation, thereby pruning the part of housekeeping codes to ease code inflation. Code inflation is a significant metric in formal language translation. Namely, minor code inflation enhances verification scale… More >

Somayeh Soltani¹, Seyed Amin Hosseini Seno¹, Juli Rejito², Rahmat Budiarto^3,*

CMC-Computers, Materials & Continua, Vol.71, No.3, pp. 5891-5910, 2022, DOI:10.32604/cmc.2022.023697

Abstract Satellite networks are recognized as the most essential communication infrastructures in the world today, which complement land networks and provide valuable services for their users. Extensive coverage and service stability of these networks have increased their popularity. Since eavesdropping and active intrusion in satellite communications are much easier than in terrestrial networks, securing satellite communications is vital. So far, several protocols have been proposed for authentication and key exchange of satellite communications, but none of them fully meet the security requirements. In this paper, we examine one of these protocols and identify its security vulnerabilities. Moreover, we propose a robust… More >

Tingting Zhang^{1, 2, 3, *}, Yushi Lan², Minggang Yu¹, Changyou Zheng¹, Kun Liu¹

CMC-Computers, Materials & Continua, Vol.62, No.2, pp. 893-904, 2020, DOI:10.32604/cmc.2020.06216

Abstract Web Services Choreography Description Language lacks a formal system to accurately express the semantics of service behaviors and verify the correctness of a service choreography model. This paper presents a new approach of choreography model verification based on Description Logic. A meta model of service choreography is built to provide a conceptual framework to capture the formal syntax and semantics of service choreography. Based on the framework, a set of rules and constraints are defined in Description Logic for choreography model verification. To automate model verification, the UML-based service choreography model will be transformed, by the given algorithms, into the… More >