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 build...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.展开更多
We report on the verification of a multi-party contract signing protocol described by Baum-Waidner and Waidner （BW）. Based on Paulson＇s inductive approach, we give the protocol model that includes infinitely many s...We report on the verification of a multi-party contract signing protocol described by Baum-Waidner and Waidner （BW）. Based on Paulson＇s inductive approach, we give the protocol model that includes infinitely many signatories and contract texts signing simuhaneously. We consider composite attacks of the dishonest signatory and the external intruder, formalize cryptographic primitives and protocol arithmetic including attack model, show formal description of key distribution, and prove signature key secrecy theorems and fairness property theorems of the BW protocol using the interactive theorem prover Isabelle/HOL.展开更多
基金This work was supported by the National Key R&D Program of China,Grant No.2018YFA0306703.
文摘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.
基金Supported by the National Natural Science Foun-dation of China (60373068)
文摘We report on the verification of a multi-party contract signing protocol described by Baum-Waidner and Waidner （BW）. Based on Paulson＇s inductive approach, we give the protocol model that includes infinitely many signatories and contract texts signing simuhaneously. We consider composite attacks of the dishonest signatory and the external intruder, formalize cryptographic primitives and protocol arithmetic including attack model, show formal description of key distribution, and prove signature key secrecy theorems and fairness property theorems of the BW protocol using the interactive theorem prover Isabelle/HOL.
