Open Access iconOpen Access

ARTICLE

crossmark

Formal Verification Platform as a Service: WebAssembly Vulnerability Detection Application

LiangJun Deng1, Hang Lei1, Zheng Yang1, WeiZhong Qian1,*, XiaoYu Li1, Hao Wu2, Sihao Deng3, RuChao Sha1, WeiDong Deng4

1 School of Information and Software Engineering, University of Electronic Science and Technology of China, Chengdu, 610054, China
2 School of Physics, University of Electronic Science and Technology of China, Chengdu, 611731, China
3 ICB-PMDM-LERMPS UMR 6303, CNRS, UTBM, Université de Bourgogne Franche-Comté, Belfort, 90010, France
4 Chengdu Railway Science and Technology Innovation Co. LTD, Chengdu, 640041, China

* Corresponding Author: WeiZhong Qian. Email: email

Computer Systems Science and Engineering 2023, 45(2), 2155-2170. https://doi.org/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 and performance efficiency. It determines the efficiency of formal verification, involving launching, running, and memory usage. For instance, path explosion increases exponentially, resulting in out-of-memory. The experimental results conclude that program languages like golang severely impact code inflation. FVPS reduces the wasm code size by over 90%, achieving two orders of optimization magnitude, from 2000 kilobyte (KB) to 90 KB. That means we can cope with golang applications up to 20 times larger than the original in scale. This work eliminates the gap between Hyperledger Fabric smart contracts and WebAssembly. Our approach is pragmatic, adaptable, extendable, and flexible. Nowadays, FVPS is successfully applied in a Railway-Port-Aviation blockchain transportation system.

Keywords


Cite This Article

L. Deng, H. Lei, Z. Yang, W. Qian, X. Li et al., "Formal verification platform as a service: webassembly vulnerability detection application," Computer Systems Science and Engineering, vol. 45, no.2, pp. 2155–2170, 2023.



cc This work is licensed under a Creative Commons Attribution 4.0 International License , which permits unrestricted use, distribution, and reproduction in any medium, provided the original work is properly cited.
  • 675

    View

  • 372

    Download

  • 1

    Like

Share Link