MF2-DMTD: A Formalism and Game-Based Reasoning Framework for Optimized Drone-Type Moving Target Defense

Moving-target-defense(MTD)fundamentally avoids an illegal initial compromise by asymmetrically increasing the uncertainty as the attack surface of the observable defender changes depending on spatial-temporal mutations.However,the existing naive MTD studies were conducted focusing only on wired network mutations.And these cases have also been no formal research on wireless aircraft domains with attributes that are extremely unfavorable to embedded system operations,such as hostility,mobility,and dependency.Therefore,to solve these conceptual limitations,this study proposes normalized drone-type MTD that maximizes defender superiority by mutating the unique fingerprints of wireless drones and that optimizes the period-based mutation principle to adaptively secure the sustainability of drone operations.In addition,this study also specifies MF2-DMTD(model-checkingbased formal framework for drone-type MTD),a formal framework that adopts model-checking and zero-sum game,for attack-defense simulation and performance evaluation of drone-type MTD.Subsequently,by applying the proposed models,the optimization of deceptive defense performance of drone-type MTD for each mutation period also additionally achieves through mixed-integer quadratic constrained programming(MIQCP)and multiobjective optimization-based Pareto frontier.As a result,the optimal mutation cycles in drone-type MTD were derived as(65,120,85)for each control-mobility,telecommunication,and payload component configured inside the drone.And the optimal MTD cycles for each swarming cluster,ground control station(GCS),and zone service provider(ZSP)deployed outside the drone were also additionally calculated as(70,60,85),respectively.To the best of these authors’knowledge,this study is the first to calculate the deceptive efficiency and functional continuity of the MTD against drones and to normalize the trade-off according to a sensitivity analysis with the optimum.

A Formal Reputation System for Trusting Wireless Sensor Network

In this paper, a formal system is proposed based on beta reputation for the development of trustworthy wireless sensor networks （FRS-TWSN）. Following this approach, key concepts related to reputation are formal described step by step for wireless sensor networks where sensor nodes maintain reputation for other sensors and use it to evaluate their trustworthiness. By proving some properties of beta reputation system, the beta distribution is founded to fit well to describe reputation system. Also, a case system is developed within this framework for reputation representation, updates and integration. Simulation results show this scheme not only can keep stable reputation but also can prevent the system from some attacks as bad mouthing and reputation cheating.

Model Checking Electronic CommerceSecurity Protocols Based on CTL

We present a model based on Computational Temporal Logic (CTL) methods forverifying security requirements of electronic commerce, protocols. The model describes formally theauthentication, confidentiality integrity, non-repudiation) denial of serviee and access control ofthe e-lectronic commerce protocols. We illustrate as case study a variant of the Lu-Smolka protocolproposed by Lu-Smolka Moreover, we have discovered two attacks that allow a dishonest user topurchase a good debiting the amountto another user. And also, we compared our work with relativeresearch works and found lhat the formal way of this paper is more general to specify securityprotocols for E-Commerce.

Formal Protection Architecture for Cloud Computing System

Cloud computing systems play a vital role in national security. This paper describes a conceptual framework called dualsystem architecture for protecting computing environments. While attempting to be logical and rigorous, formalism method is avoided and this paper chooses algebra Communication Sequential Process.

Survey of Smart Contract Technology and Application Based on Blockchain

With the vigorous development of blockchain technology represented by Bitcoin, blockchain technology has gradually surpassed the era of programmable currency and entered the era of smart contracts. Smart contracts are event- driven and stateful. With the in-depth development of blockchain technology, smart contracts use protocols and user interfaces to complete all steps of the contract process, allowing users to implement personalized code logic on the blockchain. Contract technology has the characteristics of decentralization, autonomy, observability, verifiability, and information sharing. It can effectively build programmable finance and programmable society, and is widely used in digital payment, financial asset disposal, multi-signature contracts, cloud computing, Internet of Things, sharing economy and other fields. First, it explains the basic concepts, full life cycle, basic classification, basic structure, key technologies, development status and main technology platforms of smart contracts;then discusses the application scenarios and development issues of smart contract technology, aiming to provide smart contract technology. The research and development provides reference.

Graphical Transformation of OWL Ontologies to Event-B Formal Models

Formal methods use mathematical models to develop systems.Ontologies are formal specifications that provide reusable domain knowledge representations.Ontologies have been successfully used in several data-driven applications,including data analysis.However,the creation of formal models from informal requirements demands skill and effort.Ambiguity,inconsistency,imprecision,and incompleteness are major problems in informal requirements.To solve these problems,it is necessary to have methods and approaches for supporting the mapping of requirements to formal specifications.The purpose of this paper is to present an approach that addresses this challenge by using theWeb Ontology Language(OWL)to construct Event-B formal models and support data analysis.Our approach reduces the burden of working with the formal notations of OWL ontologies and Event-B models and aims to analyze domain knowledge and construct Event-B models from OWL ontologies using visual diagrams.The idea is based on the transformation of OntoGraf diagrams of OWL ontologies to UML-B diagrams for the purpose of bridging the gap between OWL ontologies and Event-B models.Visual data exploration assists with both data analysis and the development of Event-B formal models.To manage complexity,Event-B supports stepwise refinement to allow each requirement to be introduced at themost appropriate stage in the development process.UML-B supports refinement,so we also introduce an approach that allows us to divide and layer OntoGraf diagrams.

Self Fault-Tolerance of Protocols: A Case Study

The prerequisite for the existing protocols' correctness is that protocols can be normally operated under the normal conditions, rather than dealing with abnormal conditions. In other words, protocols with the fault-tolerance can not be provided when some fault occurs. This paper discusses the self fault-tolerance of protocols. It describes some concepts and methods for achieving self fault-tolerance of protocols. Meanwhile, it provides a case study, investigates a typical protocol that does not satisfy the self fault-tolerance, and gives a new redesign version of this existing protocol using the proposed approach.

A Hybrid Formal Description Method Based on FSM,CSP and ADT for Communication Protocol

Since communication protocol deals with complex issues related to distribution such as communication, concurrency and synchronization, their development needs to be traced by using sophisticated formal description methods. This paper presents a new hybrid formal method for communication protocol specification. In this method, finite state machine (FSM), communication sequential process (CSP) and abstract data type (ADT) are mixed and the best features of these approaches are offered. In this paper, the main formal description techniques (FDT) for protocol engineering are brieny introduced and a hybrid formal description method based on the FSM, CSP and ADT for communication protocol is described. Finally, this paper presents the formal specification of an example protocol for LAN by using the proposed hybrid formal method. The results of studies show that the hybrid formal description method for communication protocol is an available and effective approach.

A Comparative Typological Study of Italian and Georgian Jargon Words

Italian youth speak their own language.The language used by youth can be considered a special language.Italian youth language has different functions.The functions which should be distinguished are:entertainment,expression,identity,and secrecy.Today,jargon has the function of entertainment more than that of secrecy.In Georgia,jargon has always been considered a foul and vulgar language.Georgian jargon words are less common than Italian ones.Georgian jargon has become popular recently.The material reviewed in the paper includes 2,700 items taken from dictionaries and the Internet.We divided them into two thematic groups:(1)related to everyday life;and(2)related to vicious aspects of life.The first group includes topics,such as money,work,the police,and youth discourse.The second group includes theft,drugs,sex life,and alcohol.The aim of this paper is to conduct a comparative study of groups of jargon identified as a result of thematic classification,in terms of methods of word formation.The study will allow us to identify semantic and formal methods of jargon word formation applied in these two unrelated languages,as well as similarities and differences between Italian and Georgian jargon words and phraseological units.

Specification and Verification of Dynamically Reconfigurable Systems Using Dynamic Linear Hybrid Automata

A dynamically reconfigurable system can change its configuration during operation, and studies of such systems are being carried out in many fields. In particular, medical technology and aerospace engineering must ensure system safety because any defect will have serious consequences. Model checking is a method for verifying system safety. In this paper, we propose the Dynamic Linear Hybrid Automaton (DLHA) specification language and show a method to analyze reachability for a system consisting of several DLHAs.

ALGEBRAIC OPERATION OF SPECIAL MATRICES RELATED TO METHOD OF LEAST SQUARES

The following situation in using the method of least squares to solve problems often occurs.After m experiments completed and a solution of least squares obtained,the ( m+1 ) th experiment is made further in order to improve the results.A method of algebraic operation of special matrices involved in the problem is given in this paper for obtaining a new solution for the m +1 experiments based upon the old solution for the primary m experiments. This method is valid for more general matrices.

On the use of formal methods to model and verify neuronal archetypes

Having a formal model of neural networks can greatly help in understanding and verifying their properties,behavior,and response to external factors such as disease and medicine.In this paper,we adopt a formal model to represent neurons,some neuronal graphs,and their composition.Some specific neuronal graphs are known for having biologically relevant structures and behaviors and we call them archetypes.These archetypes are supposed to be the basis of typical instances of neuronal information processing.In this paper we study six fundamental archetypes(simple series,series with multiple outputs,parallel composition,negative loop,inhibition of a behavior,and contralateral inhibition),and we consider two ways to couple two archetypes:(i)connecting the output(s)of the first archetype to the input(s)of the second archetype and(ii)nesting the first archetype within the second one.We report and compare two key approaches to the formal modeling and verification of the proposed neuronal archetypes and some selected couplings.The first approach exploits the synchronous programming language Lustre to encode archetypes and their couplings,and to express properties concerning their dynamic behavior.These properties are verified thanks to the use of model checkers.The second approach relies on a theorem prover,the Coq Proof Assistant,to prove dynamic properties of neurons and archetypes.

Formal methods, statistical debugging and exploratory analysis in support of system development: Towards a verification and validation calculator tool

In this paper,we propose an approach to formally verify and rigorously validate a simulation system against the specification of the real system.We implement the approach in a verification and validation calculator tool that takes as input a set of statements that capture the requirements,internal conditions of the system and expected outputs of the real system and produces as output whether the simulation satisfies the requirements,faithfully represents the internal conditions of the system and produces the expected outputs.We provide a use case to show how subject matter experts can apply the tool.

Confidential computing and related technologies:a critical review

This research critically reviews the definition of confidential computing(CC)and the security comparison of CC with other related technologies by the Confidential Computing Consortium(CCC).We demonstrate that the definitions by CCC are ambiguous,incomplete and even conflicting.We also demonstrate that the security comparison of CC with other technologies is neither scientific nor fair.We highlight the issues in the definitions and comparisons and provide initial recommendations for fixing the issues.These recommendations are the first step towards more precise definitions and reliable comparisons in the future.

Global-to-Local Approach to Rigorously Developing Distributed System with Exception Handling

Cooperative distributed system covers a wide range of applications such as the systems for industrial controlling and business-to-business trading, which are usually safety-critical. Coordinated exception handling （CEH） refers to exception handling in the cooperative distributed systems, where exceptions raised on a peer should be dealt with by all relevant peers in a consistent manner. Some CEH algorithms have been proposed. A crucial problem in using these algorithms is how to develop the peers which are guaranteed coherent in both normal execution and exceptional execution. Straightforward testing or model checking is very expensive. In this paper, we propose an effective way to rigorously develop the systems with correct CEH behavior. Firstly, we formalize the CEH algorithm by proposing a Peer Process Language to precisely describe the distributed systems and their operational semantics. Then we dig out a set of syntactic conditions, and prove its sufficiency for system coherence. Finally~ we propose a global-to-local approach, including a language describing the distributed systems from a global perspective and a projection algorithm, for developing the systems. Given a well-formed global description, a set of peers can be generated automatically. We prove the system composed of these peers satisfies the conditions, that is, it is always coherent and correct for CEH.

A Network Software Architecture Suitable for Service Customization

This paper explores the service customization in the view of network softwarearchitectures. The authors first abstract a network system into a framework that consists ofseveral layered basic systems and then propose a component-based network software architecture forone basic system of network software, which is suitable for service customization . The networksoftware architecture is formalized with the theory of Communicating Sequential Process and show itspossible applications in areas of personal service environment and service customization.

Event-Based Operational Semantics and a Consistency Result for Real-Time Concurrent Processes with Action Refinement

In this paper an event-based operational interleaving semantics is proposed for real-time processes, for which action refinement and a denotational true concurrency semantics are developed and defined in terms of timed event structures. The authors characterize the timed event traces that are generated by the operational semantics in a denotational way, and show that this operational semantics is consistent with the denotational semantics in the sense that they generate the same set of timed event traces, thereby eliminating the gap between the true concurrency and interleaving semantics. Keywords action refinement - real-time process algebra - semantics - timed event structure - formal method This work was supported by the National Natural Science Foundation of China (Grant No. 60373113) and the “Hundred-Talent Program” of Chinese Academy of Sciences.Xiu-Li Sun was born in 1975. She received her B.S. degree in 1998 and M.S. degree in 2002 from Taiyuan University of Technology, Shanxi. She is studying in the Institute of Computer Application, Chengdu for her doctorate.Wen-Ying Zhang was born in 1972. Now he is a Ph.D. candidate of Computer Application, the Chinese Academy of Sciences. His current research interests include formal verification, digital watermarking and pattern recognition.Jin-Zhao Wu was born in 1965. He obtained his Ph.D. degree in 1994 from the Institute of System Science, CAS. From 1994 to 1999 he was a postdoctoral researcher. His research interests include formal specification and verification, automatic reasoning, logic programming.

Formal Specification and Model-Checking of CSMA/CA Using Finite Precision Timed Automata

This paper presents the formal specification and model-checklng of Carrier Sense Multiple Access with Collision Avoidance（ CSMA/CA） protocol using the model checker we developed for real-time systems, which are specified as networks of finite precision timed automata. The CSMA/CA protocol proposed in the IEEE 802.11 standard is designed to reduce the probability of collision during a transmission in wireless random access environments. However, it does not eliminate completely the possibility of a collision between two or more frames transmitted simultaneously. We investigate what will give rise to a collision between frames and use our automatic verification tool for model-checking.

Formal verification technique for grid service chain model and its application

Ensuring the correctness and reliability of large-scale resource sharing and complex job processing Is an Important task for grid applications. From a formal method perspective, a grid service chain model based on state PI calculus Is proposed In this work as the theoretical foundation for the service composition and collaboration in grid. Following the Idea of the Web Service Resource Framework （WSRF）, state PI calculus enables the life-cycle management of system states by associating the actions in the original PI calculus with system states. Moreover, model checking technique is exploltad for the design-time and run-time logical verification of grid service chain models. A grid application scenario of the dynamic analysis of material deformation structure is also provided to show the effectiveness of the proposed work.

Binary Logic State Transition Oriented Formal General Reliability Model

There were various conventional modeling techniques with varied semantics for system reliability assessment, such as fault trees(FT), Markov process(MP), and Petri nets. However, it is strenuous to construct and to maintain models utilizing these formalisms throughout the life cycle of system under development. This paper proposes a unified formal modeling language to build a general reliability model. The method eliminates the gap between the actual system and reliability model and shows details of the system clearly. Furthermore,the model could be transformed into FT and MP through specific rules defined by a formal language to assess system-level reliability.