Formal Verification Platform as a Service:WebAssembly Vulnerability Detection Application

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.

Formal Verification under Unknown Constraints

We present a formal method of verifying designs with unknown constraints (e.g., black boxes) using Boolean satisfiability (SAT). This method is based on a new encoding scheme of unknown constraints, and solves the corresponding conjunctive normal form (CNF) formulas.Furthermore,this method can avoid the potential memory explosion, which the binary decision diagram (BDD) based techniques maybe suffer from, thus it has the capacity of verifying large designs. Experimental results demonstrate the efficiency and feasibility of the proposed method.

Formal Verification of the Merchant Registration Phase of the SET Protocol

This paper describes the formal verification of the Merchant Registration phase of the Secure Electronic Transactions (SET) protocol, a realistic electronic transaction security protocol which is used to protect the secrecy of online purchases. A number of concepts, notations, functions, predicates, assumptions and rules are introduced. We describe the knowledge of all legal participants, and a malicious spy, to assess the security of the sub-protocol. Avoiding search in a large state space, the method converges very quickly. We implemented our method in the Isabelle/Isar automated reasoning environment, therefore the whole verification process can be executed mechanically and efficiently. Keywords Formal verification - electronic transaction protocol - knowledge-based system This work was supported by EC, EPSRC, the National Natural Science Foundation of China (No.60496320, 60496321), and Hong Kong K C Wang Education Foundation.Xiao-Qi Ma graduated from Nanjing University of Science and Technology, China, in 1997. He received his Master’s degree from the Institute of Software, Chinese Academy of Sciences in 2003. He is currently a PhD student at the University of Reading. His research interests include computer network security, knowledge-based systems, and operating systems.Xiao-Chun Cheng obtained his PhD in 1996. He has worked as a lecturer at the University of Reading since 2000. He is a guest professor at North East Normal University and Beijing Normal University. His research interests include theoretical and applied aspects in decision support systems, knowledge-based systems and intelligent systems.

Formal Verification of TASM Models by Translating into UPPAAL

Timed abstract state machine(TASM) is a formal specification language used to specify and simulate the behavior of real-time systems. Formal verification of TASM model can be fulfilled through model checking activities by translating into UPPAAL. Firstly, the translational semantics from TASM to UPPAAL is presented through atlas transformation language(ATL). Secondly, the implementation of the proposed model transformation tool TASM2UPPAAL is provided. Finally, a case study is given to illustrate the automatic transformation from TASM model to UPPAAL model.

Refinement modeling and verification of secure operating systems for communication in digital twins

In traditional digital twin communication system testing,we can apply test cases as completely as possible in order to ensure the correctness of the system implementation,and even then,there is no guarantee that the digital twin communication system implementation is completely correct.Formal verification is currently recognized as a method to ensure the correctness of software system for communication in digital twins because it uses rigorous mathematical methods to verify the correctness of systems for communication in digital twins and can effectively help system designers determine whether the system is designed and implemented correctly.In this paper,we use the interactive theorem proving tool Isabelle/HOL to construct the formal model of the X86 architecture,and to model the related assembly instructions.The verification result shows that the system states obtained after the operations of relevant assembly instructions is consistent with the expected states,indicating that the system meets the design expectations.

Formal verification of synchronous data-flow program transformations toward certified compilers

Translation validation was invented in the 90＇s by Pnueli et al. as a technique to formally verify the correctness of code generators. Rather than certifying the code generator or exhaustively qualifying it, translation validators attempt to verify that program transformations preserve semantics. In this work, we adopt this approach to formally verify that the clock semantics and data dependence are preserved during the compilation of the Signal compiler. Translation valida- tion is implemented for every compilation phase from the initial phase until the latest phase where the executable code is generated, by proving the transformation in each phase of the compiler preserves the semantics. We represent the clock semantics, the data dependence of a program and its trans- formed counterpart as first-order formulas which are called clock models and synchronous dependence graphs （SDGs）, respectively. We then introduce clock refinement and depen- dence refinement relations which express the preservations of clock semantics and dependence, as a relation on clock mod- els and SDGs, respectively. Our validator does not require any instrumentation or modification of the compiler, nor any rewriting of the source program.

Formal Verification of Temporal Properties for Reduced Overhead in Grid Scientific Workflows

With quick development of grid techniques and growing complexity of grid applications, it is becoming critical for reasoning temporal properties of grid workflows to probe potential pitfalls and errors, in order to ensure reliability and trustworthiness at the initial design phase. A state Pi calculus is proposed and implemented in this work, which not only enables fexible abstraction and management of historical grid verification of grid workflows. Furthermore, a relaxed region system events, but also facilitates modeling and temporal analysis （RRA） approach is proposed to decompose large scale grid workflows into sequentially composed regions with relaxation of parallel workflow branches, and corresponding verification strategies are also decomposed following modular verification principles. Performance evaluation results show that the RRA approach can dramatically reduce CPU time and memory usage of formal verification.

Design and formal verification of a CEM protoco with transparent TTP

In certified email （CEM） protocols, trusted third party （TTP） transparency is an important security require- ment which helps to avoid bad publicity as well as protecting individual users＇ privacy. Cederquist et al. proposed an opti- mistic certified email protocol, which employs key chains to reduce the storage requirement of the TTE We extend their protocol to satisfy the property of TTP transparency, using existing verifiably encrypted signature schemes. An imple- mentation with the scheme based on bilinear pairing makes our extension one of the most efficient CEM protocols satis- fying strong fairness, timeliness, and TTP transparency. We formally verify the security requirements of the extended pro- tocol. The properties of fairness, timeliness and effectiveness are checked in the model checker Mocha, and TTP trans- parency is formalised and analysed using the toolsets/~CRL and CADE

A Formal Method for Service Choreography Verification Based on Description Logic

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 DL-based ontology,and thus the model properties can be verified by reasoning through the ontology with the help of a popular DL reasoned.A case study is given to demonstrate applicability of the method.Furthermore,the work will be compared with other related research.

Distributed Information Flow Verification for Secure Service Composition in Smart Sensor Network

Accelerate processor, efficient software and pervasive connections provide sensor nodes with more powerful computation and storage ability, which can offer various services to user. Based on these atomic services, different sensor nodes can cooperate and compose with each other to complete more complicated tasks for user. However, because of the regional characteristic of sensor nodes, merging data with different sensitivities become a primary requirement to the composite services, and information flow security should be intensively considered during service composition. In order to mitigate the great cost caused by the complexity of modeling and the heavy load of single-node verification to the energy-limited sensor node, in this paper, we propose a new distributed verification framework to enforce information flow security on composite services of smart sensor network. We analyze the information flows in composite services and specify security constraints for each service participant. Then we propose an algorithm over the distributed verification framework involving each sensor node to participate in the composite service verification based on the security constraints. The experimental results indicate that our approach can reduce the cost of verification and provide a better load balance.

Formal Development of Feedback Control System with Fault Accommodation

Control systems are vulnerable to faults in control loops where faults may cause abruptand damaging responses. These systems with fault accommodation are becoming more and moreimportant while appearing in flight control, robots control and nuclear reactor control etc, andcalling for more rigorous development approach. A formal approach is explored in this parer, basedon Extended Duration Calculus, for the development of such kind of systems. A typical exampleof control system with fault accommodation, two-level control system, is used for illstrating ourapproach. Its high level consists of an event-driven supervisor which reeds to the change of plant dueto faults occurrence, and its low level consists of normal controller, reconfigured controller and othercomponents with FDI (Fault Detection and Isolation) mechanism. Firstly performance and systemspecifications of the case are formulated in EDC; Then they are refined step wisely into specificationsof the supervisor and the low level components. Finally the whole system performance is verified inEDC framework.

SUMMARIZATION OF BOOLEAN SATISFIABILITY VERIFICATION

As a complementary technology to Binary Decision Diagram-based(BDD-based) symbolic model checking, the verification techniques on Boolean satisfiability problem have gained an increasing wide of applications over the last few decades, which brings a dramatic improvement for automatic verification. In this paper, we firstly introduce the theory about the Boolean satisfiability verification, including the description on the problem of Boolean satisfiability verification, Davis-Putnam-Logemann-Loveland(DPLL) based complete verification algorithm, and all kinds of solvers generated and the logic languages used by those solvers. Moreover, we formulate a large number optimizations of technique revolutions based on Boolean SATisfiability(SAT) and Satisfiability Modulo Theories(SMT) solving in detail, including incomplete methods such as bounded model checking, and other methods for concurrent programs model checking. Finally, we point out the major challenge pervasively in industrial practice and prospect directions for future research in the field of formal verification.

Modeling and Verification of Aircraft Takeoff Through Novel Quantum Nets

The formal modeling and verification of aircraft takeoff is a challenge because it is a complex safety-critical operation.The task of aircraft takeoff is distributed amongst various computer-based controllers,however,with the growing malicious threats a secure communication between aircraft and controllers becomes highly important.This research serves as a starting point for integration of BB84 quantum protocol with petri nets for secure modeling and verification of takeoff procedure.The integrated model combines the BB84 quantum cryptographic protocol with powerful verification tool support offered by petri nets.To model certain important properties of BB84,a new variant of petri nets coined as Quantum Nets are proposed by defining their mathematical foundations and overall system dynamics,furthermore,some important system properties are also abstractly defined.The proposed QuantumNets are then applied for modeling of aircraft takeoff process by defining three quantum nets:namely aircraft,runway controller and gate controller.For authentication between quantum nets,the use of external places and transitions is demonstrated to describe the encryptiondecryption process of qubits stream.Finally,the developed takeoff quantum network is verified through simulation offered by colored petri-net(CPN)Tools.Moreover,reachability tree(RT)analysis is also performed to have greater confidence in feasibility and correctness of the proposed aircraft takeoff model through the Quantum Nets.

A survey on formal specification and verification of separation kernels

Abstract Separation kernels are fundamental software of safety and security-critical systems, which provide their hosted applications with spatial and temporal separation as well as controlled information flows among partitions. The application of separation kernels in critical domain demands the correctness of the kernel by formal verification. To the best of our knowledge, there is no survey paper on this topic. This paper presents an overview of formal specification and verification of separation kernels. We first present the back- ground including the concept of separation kernel and the comparisons among different kernels. Then, we survey the state of the art on this topic since 2000. Finally, we summa- rize research work by detailed comparison and discussion.

Verify UML Statecharts with SMV

Formal verification has been widely needed in the development of safety critical systems. In order to introduce the design verification activity in UML developing process, we have developed a verifier of UML Statecharts by using the model checker SMV. The approach is to transform a system model in UML Statecharts to one in SMV input language via an intermediate language and then to verify the system properties specified in CTL by invoking SMV. The current experiences, including the formal verification of a simplified directory based cache coherence protocol in UML Statecharts, show that automatic verification can be integrated as a new step of the software process nicely.

Mechanical Proofs about BW Multi-Party Contract Signing Protocol

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.

A Quantitative Security Metric Model for Security Controls:Secure Virtual Machine Migration Protocol as Target of Assessment

Quantitative security metrics are desirable for measuring the performance of information security controls. Security metrics help to make functional and business decisions for improving the performance and cost of the security controls. However, defining enterprise-level security metrics has already been listed as one of the hard problems in the Info Sec Research Council's hard problems list. Almost all the efforts in defining absolute security metrics for the enterprise security have not been proved fruitful. At the same time, with the maturity of the security industry, there has been a continuous emphasis from the regulatory bodies on establishing measurable security metrics. This paper addresses this need and proposes a relative security metric model that derives three quantitative security metrics named Attack Resiliency Measure(ARM), Performance Improvement Factor(PIF), and Cost/Benefit Measure(CBM) for measuring the performance of the security controls. For the effectiveness evaluation of the proposed security metrics, we took the secure virtual machine(VM) migration protocol as the target of assessment. The virtual-ization technologies are rapidly changing the landscape of the computing world. Devising security metrics for virtualized environment is even more challenging. As secure virtual machine migration is an evolving area and no standard protocol is available specifically for secure VM migration. This paper took the secure virtual machine migration protocol as the target of assessment and applied the proposed relative security metric model for measuring the Attack Resiliency Measure, Performance Improvement Factor, and Cost/Benefit Measure of the secure VM migration protocol.

AN ANT COLONY ALGORITHM FOR MINIMUM UNSATISFIABLE CORE EXTRACTION

Explaining the causes of infeasibility of Boolean formulas has many practical applications in electronic design automation and formal verification of hardware.Furthermore,a minimum explanation of infeasibility that excludes all irrelevant information is generally of interest.A smallest-cardinality unsatisfiable subset called a minimum unsatisfiable core can provide a succinct explanation of infea-sibility and is valuable for applications.However,little attention has been concentrated on extraction of minimum unsatisfiable core.In this paper,the relationship between maximal satisfiability and mini-mum unsatisfiability is presented and proved,then an efficient ant colony algorithm is proposed to derive an exact or nearly exact minimum unsatisfiable core based on the relationship.Finally,ex-perimental results on practical benchmarks compared with the best known approach are reported,and the results show that the ant colony algorithm strongly outperforms the best previous algorithm.

Robust Authentication and Session Key Agreement Protocol for Satellite Communications

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 fullymeet the security requirements.In this paper,we examine one of these protocols and identify its security vulnerabilities.Moreover,we propose a robust and secure authentication and session key agreement protocol using the elliptic curve cryptography(ECC).We show that the proposed protocol meets common security requirements and is resistant to known security attacks.Moreover,we prove that the proposed scheme satisfies the security features using the Automated Validation of Internet Security Protocols and Applications(AVISPA)formal verification tool and On-the fly Model-Checker(OFMC)and ATtack SEarcher(ATSE)model checkers.We have also proved the security of the session key exchange of our protocol using theReal orRandom(RoR)model.Finally,the comparison of our scheme with similar methods shows its superiority.

Design and verification of a lightweight reliable virtual machine monitor for a many-core architecture

Virtual machine monitors （VMMs） play a central role in cloud computing. Their reliability and availability are critical for cloud computing. Virtualization and device emu- lation make the VMM code base large and the interface be- tween OS and VMM complex. This results in a code base that is very hard to verify the security of the VMM. For exam- ple, a misuse of a VMM hyper-call by a malicious guest OS can corrupt the whole VMM. The complexity of the VMM also makes it hard to formally verify the correctness of the system＇s behavior. In this paper a new VMM, operating sys- tem virtualization （OSV）, is proposed. The multiprocessor boot interface and memory configuration interface are virtu- alized in OSV at boot time in the Linux kernel. After booting, only inter-processor interrupt operations are intercepted by OSV, which makes the interface between OSV and OS sim- ple. The interface is verified using formal model checking, which ensures a malicious OS cannot attack OSV through the interface. Currently, OSV is implemented based on the AMD Opteron multi-core server architecture. Evaluation re- sults show that Linux running on OSV has a similar perfor- mance to native Linux. OSV has a performance improvement of 4%-13% over Xen.