Volume 32,Issue 6,2021 Table of Contents
2021, 32(6):1581-1596.
DOI: 10.13328/j.cnki.jos.006238
Abstract:
Formal method provides a theoretical tool for security protocol analysis, but the theoretical security is not equivalent to the actual security. A verified protocol standard may not meet the required security properties when converted into a concrete program. Hence, a formal verification method for detecting semantic logic errors in security protocol code is proposed. By automatically abstracting the C source code of the protocol into Pi calculus model, protocol security properties are verified based on the Pi calculus. Finally, the correctness of the scheme transformation is proved and the validity of the method is verified by a Kerberos protocol instance code. C2P tools implemented can help protocol developers to detect semantic logic errors in code.
Formal method provides a theoretical tool for security protocol analysis, but the theoretical security is not equivalent to the actual security. A verified protocol standard may not meet the required security properties when converted into a concrete program. Hence, a formal verification method for detecting semantic logic errors in security protocol code is proposed. By automatically abstracting the C source code of the protocol into Pi calculus model, protocol security properties are verified based on the Pi calculus. Finally, the correctness of the scheme transformation is proved and the validity of the method is verified by a Kerberos protocol instance code. C2P tools implemented can help protocol developers to detect semantic logic errors in code.
2021, 32(6):1597-1611.
DOI: 10.13328/j.cnki.jos.006239
Abstract:
In GitHub platform, many project contributors often ignore the descriptions of pull requests (PRs) when submitting PRs, making their PRs easily neglected or rejected by reviewers. Therefore, it is necessary to generate PR descriptions automatically to help increase PR pass rate. The performances of existing PR description generation methods are usually affected by PR granularity, so it is difficult to generate descriptions for large-granularity PRs effectively. For such reasons, this work focuses on generating descriptions for large-granularity PRs. The text information is first preprocessed in PR and word-sentence heterogeneous graphs are constructed where the words are used as secondary nodes, so as to establish the connections between PR sentences. Subsequently, feature extraction is performed on the heterogeneous graphs, and then the features are input into graph neural network for further graph representation learning, from which the sentence nodes can learn more abundant content information through message delivery between nodes. Finally, the sentences with key information are selected to form a PR description. In addition, the supervised learning method cannot be used for training due to the lack of manually labeled tags in the dataset, therefore, reinforcement learning is used to guide the generation of PR descriptions. The goal of model training is minimizing the negative expectation of rewards, which does not require the ground truth and directly improves the performance of the results. The experiments are conducted on real dataset and the experimental results show that the proposed method is superior to existing methods in F1 and readability.
In GitHub platform, many project contributors often ignore the descriptions of pull requests (PRs) when submitting PRs, making their PRs easily neglected or rejected by reviewers. Therefore, it is necessary to generate PR descriptions automatically to help increase PR pass rate. The performances of existing PR description generation methods are usually affected by PR granularity, so it is difficult to generate descriptions for large-granularity PRs effectively. For such reasons, this work focuses on generating descriptions for large-granularity PRs. The text information is first preprocessed in PR and word-sentence heterogeneous graphs are constructed where the words are used as secondary nodes, so as to establish the connections between PR sentences. Subsequently, feature extraction is performed on the heterogeneous graphs, and then the features are input into graph neural network for further graph representation learning, from which the sentence nodes can learn more abundant content information through message delivery between nodes. Finally, the sentences with key information are selected to form a PR description. In addition, the supervised learning method cannot be used for training due to the lack of manually labeled tags in the dataset, therefore, reinforcement learning is used to guide the generation of PR descriptions. The goal of model training is minimizing the negative expectation of rewards, which does not require the ground truth and directly improves the performance of the results. The experiments are conducted on real dataset and the experimental results show that the proposed method is superior to existing methods in F1 and readability.
2021, 32(6):1612-1630.
DOI: 10.13328/j.cnki.jos.006240
Abstract:
Unfolding technology can partially alleviate the state explosion problem in Petri net through branching processes. However, an unfolding still contains all states of a system. Some practical problems only need to determine the coverability of a specific state, which is expected to reduce the scale of unfolding net. This study proposes a target-oriented reverse unfolding algorithm for the coverability problem of 1-safe Petri nets, which combines heuristic technology to reduce the scale of unfolding nets, thereby improving the efficiency of coverability determination. Furthermore, the reverse unfolding technology is applied to the formal verification of concurrent programs, and the data race detection problem is converted into the coverability problem of a specific state in 1-safe Petri nets. The experiment compares the efficiency between forward unfolding and reverse unfolding in the coverability problem of Petri net. The results show that when the Petri net has more forward branches than backward branches, reverse unfolding is more efficient than forward unfolding. Finally, the key factors influencing the efficiency of reverse unfolding are analyzed.
Unfolding technology can partially alleviate the state explosion problem in Petri net through branching processes. However, an unfolding still contains all states of a system. Some practical problems only need to determine the coverability of a specific state, which is expected to reduce the scale of unfolding net. This study proposes a target-oriented reverse unfolding algorithm for the coverability problem of 1-safe Petri nets, which combines heuristic technology to reduce the scale of unfolding nets, thereby improving the efficiency of coverability determination. Furthermore, the reverse unfolding technology is applied to the formal verification of concurrent programs, and the data race detection problem is converted into the coverability problem of a specific state in 1-safe Petri nets. The experiment compares the efficiency between forward unfolding and reverse unfolding in the coverability problem of Petri net. The results show that when the Petri net has more forward branches than backward branches, reverse unfolding is more efficient than forward unfolding. Finally, the key factors influencing the efficiency of reverse unfolding are analyzed.
2021, 32(6):1631-1646.
DOI: 10.13328/j.cnki.jos.006241
Abstract:
Safety-critical systems such as spacecraft are typical embedded systems with the characteristics of multi-task concurrency and frequent interruptions. The operating system is the most fundamental software of computer, and building a correct operating system is crucial to ensure the reliability of the spacecraft system. Exception management, as the lowest level function of the operating system, is responsible for guiding sudden changes of control flow in response to certain changes in the processor state. Exception management is the basis for the correctness of the entire operating system correctness. This study proposes a verification framework based on Hoare-logic to prove the correctness of exception management for SPARC processor architecture operating systems. Especially for multi-task concurrency and frequent interruption of real-time operating system exception nesting and task switching in exceptions, the exception management is divided into five stages for comprehensive formal modeling, and this framework is implemented in the Coq proving theorem assistant tool. Based on this framework, the correctness of the exception management function of the spacecraft embedded real-time operating system SpaceOS, which is actually used by China's Beidou-3, is verified.
Safety-critical systems such as spacecraft are typical embedded systems with the characteristics of multi-task concurrency and frequent interruptions. The operating system is the most fundamental software of computer, and building a correct operating system is crucial to ensure the reliability of the spacecraft system. Exception management, as the lowest level function of the operating system, is responsible for guiding sudden changes of control flow in response to certain changes in the processor state. Exception management is the basis for the correctness of the entire operating system correctness. This study proposes a verification framework based on Hoare-logic to prove the correctness of exception management for SPARC processor architecture operating systems. Especially for multi-task concurrency and frequent interruption of real-time operating system exception nesting and task switching in exceptions, the exception management is divided into five stages for comprehensive formal modeling, and this framework is implemented in the Coq proving theorem assistant tool. Based on this framework, the correctness of the exception management function of the spacecraft embedded real-time operating system SpaceOS, which is actually used by China's Beidou-3, is verified.
2021, 32(6):1647-1662.
DOI: 10.13328/j.cnki.jos.006242
Abstract:
Model-driven development is widely used in embedded software development because it has a low error rate while it is easy to simulate and verify. In recent years, model-based embedded software development methods and their corresponding tools are also gradually developing and improving. Data flow model is the most frequently used semantic model among all kinds of modeling tools. Nonetheless, the code generation ability of various tools for data flow model is uneven, especially for the branching actors. It is well known that current mainstream modeling tools adopt various ways to avoid complex branch modeling and the generation of its corresponding code. However, branch modeling is very important, and it makes the data transfer logic of the data flow more clearly by using branch actors. In order to solve the problem of code generation caused by complex branch modeling, this study proposed a code generation method based on branch schedule marking for data flow model aimed at complex branch combinations. As for the algorithm proposed in this study, firstly, the scheduling order of the model was determined by topological sorting. Secondly, a code generation location table based on control flow was constructed according to the branch marks which marked by the influence of different branches. Finally, code generation of various mainstream languages could be carried out in terms of the code generation location table. By constructing four instances of data flow models with complex branches for code generation and comparing them with Simulink and Ptolemy in terms of lines of code generation and elapsed time, this study further illustrates the universality of proposed code generation methods in complex branch combinations and the value and significance of this work.
Model-driven development is widely used in embedded software development because it has a low error rate while it is easy to simulate and verify. In recent years, model-based embedded software development methods and their corresponding tools are also gradually developing and improving. Data flow model is the most frequently used semantic model among all kinds of modeling tools. Nonetheless, the code generation ability of various tools for data flow model is uneven, especially for the branching actors. It is well known that current mainstream modeling tools adopt various ways to avoid complex branch modeling and the generation of its corresponding code. However, branch modeling is very important, and it makes the data transfer logic of the data flow more clearly by using branch actors. In order to solve the problem of code generation caused by complex branch modeling, this study proposed a code generation method based on branch schedule marking for data flow model aimed at complex branch combinations. As for the algorithm proposed in this study, firstly, the scheduling order of the model was determined by topological sorting. Secondly, a code generation location table based on control flow was constructed according to the branch marks which marked by the influence of different branches. Finally, code generation of various mainstream languages could be carried out in terms of the code generation location table. By constructing four instances of data flow models with complex branches for code generation and comparing them with Simulink and Ptolemy in terms of lines of code generation and elapsed time, this study further illustrates the universality of proposed code generation methods in complex branch combinations and the value and significance of this work.
2021, 32(6):1663-1681.
DOI: 10.13328/j.cnki.jos.006243
Abstract:
The embedded system has been wildly applied in real-time automatic control systems, and most of these systems are safety-critical. For example, the engine control systems in an automobile, and the avionics in an airplane. It is very important to verify the schedulability property of such real-time embedded system in its early design stages, so that to avoid unexpected loss for the debugging of architecture design frictions. However, it has been proved to be a tough challenge to evaluate the schedulability of a PSRT (preemptive-scheduling real-time) system, especially when taking the constraints of system resources into consideration. The cache memory build inside the processor is such a kind of exclusive-accessing resource that is shared by all the tasks deployed on the processor. In addition, the CPRD (cache-related preemption delay) caused by preemptive task scheduling will bring extra time to the execution time to all the tasks. Thus, the CPRD should be taken into consideration when estimating the WCET (worst case executing time) of tasks in a real-time system. A model-based architecture level schedulability evaluate and verification method, which is designed for priority based PSRT system, is proposed in this study, in order to do cache resource constrained, and CPRD related schedulability evaluation based on AADL system architecture model. In the first step, the study enhances the property set of AADL storage elements, so that to be compatible with cache memory properties in system architecture model constructing. Secondly, the study proposes a set or algorithms to:estimate the CPRDs of a task before it is completed; do system schedule simulation and construct the schedule sequence with the constraint of Cache resource and CPRDs involved; and WCET estimation of the tasks in such a CPRD considered, preemptive-scheduling execution sequence. Finally, methods mentioned above are implemented within a prototype software toolkit, which is designed to do system level schedulability evaluation and verification with CPRD constraints considered. The toolkit is tested with a use case of aircraft airborne open-architecture intelligent information system. The result shows that, compared with schedule sequence constructed without cache memory resource constraints, the WCET estimated for most tasks are extended, and sequence order is changed. In some extreme cases, when CPRD is taken into consideration, some tasks are evaluated to be incompletable. The test shows that the method and algorithms proposed in this study are feasible.
The embedded system has been wildly applied in real-time automatic control systems, and most of these systems are safety-critical. For example, the engine control systems in an automobile, and the avionics in an airplane. It is very important to verify the schedulability property of such real-time embedded system in its early design stages, so that to avoid unexpected loss for the debugging of architecture design frictions. However, it has been proved to be a tough challenge to evaluate the schedulability of a PSRT (preemptive-scheduling real-time) system, especially when taking the constraints of system resources into consideration. The cache memory build inside the processor is such a kind of exclusive-accessing resource that is shared by all the tasks deployed on the processor. In addition, the CPRD (cache-related preemption delay) caused by preemptive task scheduling will bring extra time to the execution time to all the tasks. Thus, the CPRD should be taken into consideration when estimating the WCET (worst case executing time) of tasks in a real-time system. A model-based architecture level schedulability evaluate and verification method, which is designed for priority based PSRT system, is proposed in this study, in order to do cache resource constrained, and CPRD related schedulability evaluation based on AADL system architecture model. In the first step, the study enhances the property set of AADL storage elements, so that to be compatible with cache memory properties in system architecture model constructing. Secondly, the study proposes a set or algorithms to:estimate the CPRDs of a task before it is completed; do system schedule simulation and construct the schedule sequence with the constraint of Cache resource and CPRDs involved; and WCET estimation of the tasks in such a CPRD considered, preemptive-scheduling execution sequence. Finally, methods mentioned above are implemented within a prototype software toolkit, which is designed to do system level schedulability evaluation and verification with CPRD constraints considered. The toolkit is tested with a use case of aircraft airborne open-architecture intelligent information system. The result shows that, compared with schedule sequence constructed without cache memory resource constraints, the WCET estimated for most tasks are extended, and sequence order is changed. In some extreme cases, when CPRD is taken into consideration, some tasks are evaluated to be incompletable. The test shows that the method and algorithms proposed in this study are feasible.
2021, 32(6):1682-1700.
DOI: 10.13328/j.cnki.jos.006244
Abstract:
Deadlocks are a common defect of parallel programs. To detect deadlocks, dynamic deadlock analysis methods build models such as lock graphs and segment graphs according to program running traces. However, a lock graph and its existing variants cannot distinguish different executions of one lock acquisition statement in a loop structure. The lock set used in extended lock graphs cannot capture those locks which were once held and then released. A segmentation graph cannot model the inter-segment dependencies caused by the coupling of lock release/acquisition operation and thread start operation. The above problems have led to a variety of false positives. To address this issue, existing lock graph and segment graph models are improved. Specifically, a lock graph is extended with statement execution order information. A segmentation graph is expanded with lock acquisition and release information. Furthermore, segments in a segmentation graph are more finely divided in the improved model to capture the inter-segment dependencies caused by lock objects. Eventually, based on the improved models, a new deadlock detection method is proposed. It can eliminate the aforementioned false alarms effectively and improve deadlock detection accuracy. A corresponding prototype system is developed for experimental evaluation. The validity of the proposed method is verified through experiments.
Deadlocks are a common defect of parallel programs. To detect deadlocks, dynamic deadlock analysis methods build models such as lock graphs and segment graphs according to program running traces. However, a lock graph and its existing variants cannot distinguish different executions of one lock acquisition statement in a loop structure. The lock set used in extended lock graphs cannot capture those locks which were once held and then released. A segmentation graph cannot model the inter-segment dependencies caused by the coupling of lock release/acquisition operation and thread start operation. The above problems have led to a variety of false positives. To address this issue, existing lock graph and segment graph models are improved. Specifically, a lock graph is extended with statement execution order information. A segmentation graph is expanded with lock acquisition and release information. Furthermore, segments in a segmentation graph are more finely divided in the improved model to capture the inter-segment dependencies caused by lock objects. Eventually, based on the improved models, a new deadlock detection method is proposed. It can eliminate the aforementioned false alarms effectively and improve deadlock detection accuracy. A corresponding prototype system is developed for experimental evaluation. The validity of the proposed method is verified through experiments.
2021, 32(6):1701-1716.
DOI: 10.13328/j.cnki.jos.006245
Abstract:
The taint analysis technology is an effective method to detect the privacy data leakage of Android smart phones. However, the state-of-the-art tools of taint analysis for Android applications mainly focus on the accuracy with few of them addressing the importance of the efficiency and time cost. Actually, the high cost may cause problems such as timeouts or program crashes when the tools analyze some complex applications, which block them from wide usage. This study proposes a novel taint analysis approach based on the tainted value graph, which reduces the time cost and improves the efficiency. The tainted value graph is formalized to describe the tainted values and their relationships and the taint analysis and alias analysis are combined together without using the traditional data flow analysis framework. In addition, the taint flows are verified on the control flow graph to improve accuracy. The architecture, modules, and algorithmic details of the proposed tool FastDroid are also described in this paper. The tool is evaluated on three test suites:DroidBench-2.0, MalGenome, and 1517 apps randomly downloaded from Google Play. The experimental results show that, compared with the tool FlowDroid, FastDroid has a higher precision of 93.3% and a higher recall of 85.8% on DroidBench-2.0, and the time cost for analysis is less and more stable on all the test suites.
The taint analysis technology is an effective method to detect the privacy data leakage of Android smart phones. However, the state-of-the-art tools of taint analysis for Android applications mainly focus on the accuracy with few of them addressing the importance of the efficiency and time cost. Actually, the high cost may cause problems such as timeouts or program crashes when the tools analyze some complex applications, which block them from wide usage. This study proposes a novel taint analysis approach based on the tainted value graph, which reduces the time cost and improves the efficiency. The tainted value graph is formalized to describe the tainted values and their relationships and the taint analysis and alias analysis are combined together without using the traditional data flow analysis framework. In addition, the taint flows are verified on the control flow graph to improve accuracy. The architecture, modules, and algorithmic details of the proposed tool FastDroid are also described in this paper. The tool is evaluated on three test suites:DroidBench-2.0, MalGenome, and 1517 apps randomly downloaded from Google Play. The experimental results show that, compared with the tool FlowDroid, FastDroid has a higher precision of 93.3% and a higher recall of 85.8% on DroidBench-2.0, and the time cost for analysis is less and more stable on all the test suites.
2021, 32(6):1717-1732.
DOI: 10.13328/j.cnki.jos.006246
Abstract:
Smart contracts are key software components of blockchain applications. Recently, a great number of bugs and security vulnerabilities have been exposed in smart contracts on the Ethereum blockchain. This resulted in extensive research efforts in the formal verification of smart contracts at the international level. To obtain highly trustworthy verification results, the formalization of programming languages for smart contracts is necessary. This work formalizes Yul-the Ethereum intermediate language. The core of this formalization consists of the first formal definitions of the type system and the small-step operational semantics for Yul. The semantics is executable, and it is validated using a test suite of 120 Yul programs. The proposed formalization is performed in the Isabelle/HOL proof assistant. It lays a solid foundation for the formal verification of the correctness and security of Ethereum smart contracts through theorem proving.
Smart contracts are key software components of blockchain applications. Recently, a great number of bugs and security vulnerabilities have been exposed in smart contracts on the Ethereum blockchain. This resulted in extensive research efforts in the formal verification of smart contracts at the international level. To obtain highly trustworthy verification results, the formalization of programming languages for smart contracts is necessary. This work formalizes Yul-the Ethereum intermediate language. The core of this formalization consists of the first formal definitions of the type system and the small-step operational semantics for Yul. The semantics is executable, and it is validated using a test suite of 120 Yul programs. The proposed formalization is performed in the Isabelle/HOL proof assistant. It lays a solid foundation for the formal verification of the correctness and security of Ethereum smart contracts through theorem proving.
2021, 32(6):1733-1747.
DOI: 10.13328/j.cnki.jos.006247
Abstract:
User feature extraction and identity authentication methods based on interactive behavior are an important method of identity recognition. However, for high-frequency users, the interactive behavior patterns and operating habits are relatively stable, which are easily imitated by fraudsters and making the existing models have a higher misjudgment. The key point to solve the above problems is to make the user's behavior change smoothly and distinguishably. This study proposes a smooth intervention model based on an individual interactive behavior system to handle it. Firstly, according to the user history web behavior log, the change trend of user interaction behavior is obtained from multiple dimensions. Then, combined with the stability and deviation of the behavior, the time-domain drift algorithm (TDDA) is proposed to determine the behavior guidance time of each user. Finally, an intervention model for interactive behavior reconstruction systems is proposed, which superimposes behavior trigger factors on non-critical paths in the system to guide users generating new interactive behavior habits. Experiments prove that the method proposed in this study could guide the user's behavior to change smoothly and produce sufficient distinction to significantly advance the model accuracy in the scenario of behavior camouflage anomaly detection.
User feature extraction and identity authentication methods based on interactive behavior are an important method of identity recognition. However, for high-frequency users, the interactive behavior patterns and operating habits are relatively stable, which are easily imitated by fraudsters and making the existing models have a higher misjudgment. The key point to solve the above problems is to make the user's behavior change smoothly and distinguishably. This study proposes a smooth intervention model based on an individual interactive behavior system to handle it. Firstly, according to the user history web behavior log, the change trend of user interaction behavior is obtained from multiple dimensions. Then, combined with the stability and deviation of the behavior, the time-domain drift algorithm (TDDA) is proposed to determine the behavior guidance time of each user. Finally, an intervention model for interactive behavior reconstruction systems is proposed, which superimposes behavior trigger factors on non-critical paths in the system to guide users generating new interactive behavior habits. Experiments prove that the method proposed in this study could guide the user's behavior to change smoothly and produce sufficient distinction to significantly advance the model accuracy in the scenario of behavior camouflage anomaly detection.
2021, 32(6):1748-1778.
DOI: 10.13328/j.cnki.jos.006248
Abstract:
PolarFS is a distributed file system developed by Alibaba Inc. with ultra-low latency and high availability. It implemented a variant of the Raft consensus protocol, called ParallelRaft. ParallelRaft breaks Raft's strict serialization restrictions in the commitment and execution of log entries and enables state machines to commit and execute log entries in an out-of-order way. However, ParallelRaft is not open-sourced. It has only a brief description, lacking formal specification. Moreover, the correctness of ParallelRaft has not been manually proven or formally checked. The purpose of the study is to provide a precise formal specification for ParallelRaft and to prove its correctness. Specifically, the following main contributions are accomplished. First, to clarify the relationship between Raft and ParallelRaft, ParallelRaft-SE (sequential execution) is proposed, which allows out-of-order commitment but prohibits out-of-order executions. Also, a refinement mapping from ParallelRaft-SE to Multi-Paxos is established. Second, it is discovered that ParallelRaft, according to its brief description in the literature, neglects the so-called "ghost log entries" phenomenon, which may violate the consistency among state machines. Therefore, based on ParallelRaft-SE, ParallelRaft-CE (concurrent execution) is proposed. ParallelRaft-CE avoids the "ghost log entries" phenomenon and ensures the consistency among state machine when executing concurrently by limiting parallelism in the commitment of log entries. The correctness of ParallelRaft-CE is proved manually. Finally, the formal specifications of ParallelRaft-SE and ParallelRaft-CE using TLA+ (TLA stands for temporal logic of actions) are provided, and the refinement mapping from ParallelRaft-SE to Multi-Paxos and the correctness of ParallelRaft-CE are verified using the TLC model checker when the number of participants of the protocols is small.
PolarFS is a distributed file system developed by Alibaba Inc. with ultra-low latency and high availability. It implemented a variant of the Raft consensus protocol, called ParallelRaft. ParallelRaft breaks Raft's strict serialization restrictions in the commitment and execution of log entries and enables state machines to commit and execute log entries in an out-of-order way. However, ParallelRaft is not open-sourced. It has only a brief description, lacking formal specification. Moreover, the correctness of ParallelRaft has not been manually proven or formally checked. The purpose of the study is to provide a precise formal specification for ParallelRaft and to prove its correctness. Specifically, the following main contributions are accomplished. First, to clarify the relationship between Raft and ParallelRaft, ParallelRaft-SE (sequential execution) is proposed, which allows out-of-order commitment but prohibits out-of-order executions. Also, a refinement mapping from ParallelRaft-SE to Multi-Paxos is established. Second, it is discovered that ParallelRaft, according to its brief description in the literature, neglects the so-called "ghost log entries" phenomenon, which may violate the consistency among state machines. Therefore, based on ParallelRaft-SE, ParallelRaft-CE (concurrent execution) is proposed. ParallelRaft-CE avoids the "ghost log entries" phenomenon and ensures the consistency among state machine when executing concurrently by limiting parallelism in the commitment of log entries. The correctness of ParallelRaft-CE is proved manually. Finally, the formal specifications of ParallelRaft-SE and ParallelRaft-CE using TLA+ (TLA stands for temporal logic of actions) are provided, and the refinement mapping from ParallelRaft-SE to Multi-Paxos and the correctness of ParallelRaft-CE are verified using the TLC model checker when the number of participants of the protocols is small.
2021, 32(6):1779-1798.
DOI: 10.13328/j.cnki.jos.006249
Abstract:
With the in-depth research of CPS (cyber physical system), the security problems of CPS are gradually attracted extensive attention. How to verify the security of space and time inconsistency of CPS has become a research hot spot. A hybrid AADL (architecture analysis & design language) modeling and model transformation method for CPS is proposed to solve this problem. Firstly, the time and space description capability of AADL behavior annex is extended, and Hybrid AADL (hybrid architecture analysis & design language) is proposed. Secondly, the differential equation and the position description are introduced into the process algebra. Thirdly, the hybrid AADL is transformed into HP-TCSP. Finally, the effectiveness of the proposed method is verified by an example of aircraft anti-collision system.
With the in-depth research of CPS (cyber physical system), the security problems of CPS are gradually attracted extensive attention. How to verify the security of space and time inconsistency of CPS has become a research hot spot. A hybrid AADL (architecture analysis & design language) modeling and model transformation method for CPS is proposed to solve this problem. Firstly, the time and space description capability of AADL behavior annex is extended, and Hybrid AADL (hybrid architecture analysis & design language) is proposed. Secondly, the differential equation and the position description are introduced into the process algebra. Thirdly, the hybrid AADL is transformed into HP-TCSP. Finally, the effectiveness of the proposed method is verified by an example of aircraft anti-collision system.
2021, 32(6):1799-1817.
DOI: 10.13328/j.cnki.jos.006250
Abstract:
In the field of chip design, the use of model-driven FPGA design methods is currently a safer and more reliable method. However, model-driven FPGA design needs to prove the consistency of the FPGA design model and the generated Verilog/VHDL code. Further, the chip design correctness, performance, reliability, and safety are critical. At present, simulation methods are often used to verify the consistency of models and codes. It is difficult to ensure the reliability and safety of the design, and there are problems such as low verification efficiency and heavy workload. This study proposes a new method to verify the consistency of the design model and the generated code. This method uses the MSVL language to model the system, and propositional projection temporal logic (PPTL) formula to describe the properties of the system, then based on the principle of unified model checking, verifies whether the model meets the validity of the property. Furthermore, a signal light control system is used as a verification example to verify and explain the verification method.
In the field of chip design, the use of model-driven FPGA design methods is currently a safer and more reliable method. However, model-driven FPGA design needs to prove the consistency of the FPGA design model and the generated Verilog/VHDL code. Further, the chip design correctness, performance, reliability, and safety are critical. At present, simulation methods are often used to verify the consistency of models and codes. It is difficult to ensure the reliability and safety of the design, and there are problems such as low verification efficiency and heavy workload. This study proposes a new method to verify the consistency of the design model and the generated code. This method uses the MSVL language to model the system, and propositional projection temporal logic (PPTL) formula to describe the properties of the system, then based on the principle of unified model checking, verifies whether the model meets the validity of the property. Furthermore, a signal light control system is used as a verification example to verify and explain the verification method.
2021, 32(6):1818-1829.
DOI: 10.13328/j.cnki.jos.006251
Abstract:
Robot operating system (ROS) is an open source meta-operating system, which can provide a structured communication layer based on message mechanism on heterogeneous computing clusters. In order to improve the real-time and reliability problems of data distribution in ROS1, ROS2 is proposed with data flow oriented data distribution service mechanism. This study adopts the method of probability model test and analysis, validates real-time and reliability of the ROS2 system. Firstly, a data flow oriented ROS2 data distribution service system of communication formal validation framework is put forward, and the communication system module probabilistic timed automata model is set up. Secondly, probabilistic model detector PRISM is used to verify the real-time and reliability of ROS2 data flow oriented data distribution service through parameter analysis of data loss rate and system response time. Finally, based on retransmission mechanism, quality of service (QoS) strategy analysis, through the set up and adjust service quality parameters, different data requirements and quantitative performance analysis of transmission mode are achieved, providing the reference for application designers based on ROS2 and distributed data distribution service based on the data flow of formal modeling, validation, and quantitative performance analysis.
Robot operating system (ROS) is an open source meta-operating system, which can provide a structured communication layer based on message mechanism on heterogeneous computing clusters. In order to improve the real-time and reliability problems of data distribution in ROS1, ROS2 is proposed with data flow oriented data distribution service mechanism. This study adopts the method of probability model test and analysis, validates real-time and reliability of the ROS2 system. Firstly, a data flow oriented ROS2 data distribution service system of communication formal validation framework is put forward, and the communication system module probabilistic timed automata model is set up. Secondly, probabilistic model detector PRISM is used to verify the real-time and reliability of ROS2 data flow oriented data distribution service through parameter analysis of data loss rate and system response time. Finally, based on retransmission mechanism, quality of service (QoS) strategy analysis, through the set up and adjust service quality parameters, different data requirements and quantitative performance analysis of transmission mode are achieved, providing the reference for application designers based on ROS2 and distributed data distribution service based on the data flow of formal modeling, validation, and quantitative performance analysis.
2021, 32(6):1830-1848.
DOI: 10.13328/j.cnki.jos.006252
Abstract:
Ptolemy is a modeling and simulation toolkit widely used in cyber physical systems, which ensures the correctness of the models through simulation. Formal verification is one of the important methods to guarantee the correctness of systems. This paper presents a model translation based approach to verify the Ptolemy discrete event model. The discrete event model fires according to the timestamp of different events, and the timed automaton can express this feature. Therefore, Uppaal is a suitable verification tool. First, the semantic of discrete event model is defined. And a set of mapping rules are designed to represent the discrete event model with a network of timed automata. Then, a plug-in is implemented in the Ptolemy environment that automatically translated the discrete event model into a network of timed automata, and verifies the network of timed automata by calling the Uppaal validation kernel. Finally, a case of traffic light control system is successfully translated and verified, and the experimental results confirm that the proposed approach is reliable and effective for the verification of Ptolemy discrete event model.
Ptolemy is a modeling and simulation toolkit widely used in cyber physical systems, which ensures the correctness of the models through simulation. Formal verification is one of the important methods to guarantee the correctness of systems. This paper presents a model translation based approach to verify the Ptolemy discrete event model. The discrete event model fires according to the timestamp of different events, and the timed automaton can express this feature. Therefore, Uppaal is a suitable verification tool. First, the semantic of discrete event model is defined. And a set of mapping rules are designed to represent the discrete event model with a network of timed automata. Then, a plug-in is implemented in the Ptolemy environment that automatically translated the discrete event model into a network of timed automata, and verifies the network of timed automata by calling the Uppaal validation kernel. Finally, a case of traffic light control system is successfully translated and verified, and the experimental results confirm that the proposed approach is reliable and effective for the verification of Ptolemy discrete event model.
2021, 32(6):1849-1866.
DOI: 10.13328/j.cnki.jos.006253
Abstract:
Smart contract is a computer protocol running on the blockchain, which is widely used in various fields. However, its security problems continue to emerge. Therefore, it is necessary to audit the security of a smart contract before it is deployed on the blockchain. Traditional testing methods cannot guarantee the high reliability and correctness required by smart contracts. This study shows how to use modeling, simulation, and verification language (MSVL) and propositional projection temporal logic (PPTL) to model and verify smart contracts. First, the theoretical basis of MSVL and PPTL is introduced. Then, by analyzing and comparing the characteristics of solidity and MSVL, an SOL2M converter which can convert a solidity program to an MSVL program is developed and its design idea is introduced in detail. Finally, the execution results of SOL2M converter are given by two examples of a vote smart contract and a bank transfer smart contract. The properties of contracts are described by PPTL on three aspects:function consistency, logic correctness, and contract completeness. And the process of using UMC4M (Unified Model Checker for MSVL) to verify the contract is also given.
Smart contract is a computer protocol running on the blockchain, which is widely used in various fields. However, its security problems continue to emerge. Therefore, it is necessary to audit the security of a smart contract before it is deployed on the blockchain. Traditional testing methods cannot guarantee the high reliability and correctness required by smart contracts. This study shows how to use modeling, simulation, and verification language (MSVL) and propositional projection temporal logic (PPTL) to model and verify smart contracts. First, the theoretical basis of MSVL and PPTL is introduced. Then, by analyzing and comparing the characteristics of solidity and MSVL, an SOL2M converter which can convert a solidity program to an MSVL program is developed and its design idea is introduced in detail. Finally, the execution results of SOL2M converter are given by two examples of a vote smart contract and a bank transfer smart contract. The properties of contracts are described by PPTL on three aspects:function consistency, logic correctness, and contract completeness. And the process of using UMC4M (Unified Model Checker for MSVL) to verify the contract is also given.
2021, 32(6):1867-1881.
DOI: 10.13328/j.cnki.jos.006254
Abstract:
Robot operating system (ROS) is an open source system widely used in Robot development. It can provide developers with hardware abstraction, device driver, library function, visualization, messaging, software package management, and other functions, which has an important and broad application prospect. ROS integrates various software packages that can realize different functions, such as positioning drawing, action planning, perception, simulation, etc. However, some vulnerabilities may damage the overall safety and reliability of robot system directly. In this study, an ROS oriented fuzzing method is proposed to test different versions of ROS packages and find out the vulnerabilities. The proposed approach includes two modules:Test cases generation and differential fuzz testing execution. Firstly, load and process the input file, and generate the test cases file based on the strategy's generation. Secondly, communication among nodes is achieved using topic communication mechanism, and the test case files are used as the inputs to carry out differential fuzz testing on the ROS packages. Then, the inconsistent outputs in the test results are calculated and evaluated, and the seed meet the evaluation indicators are reserved and fed back to the test case generation module to generate test cases, it will improve seed quality and code coverage effectively. Finally, analyze the cause of inconsistent output and find out the vulnerability. This method is applied in the experiment of robot coordinate transformation, testing the packages TF and TF2 that realize coordinate transformation under different reference frames. Final experiment results show that TF is more accurate in function implementation compared with TF2, and there are vulnerabilities in the function of TF2 to realize coordinate rotation transformation.
Robot operating system (ROS) is an open source system widely used in Robot development. It can provide developers with hardware abstraction, device driver, library function, visualization, messaging, software package management, and other functions, which has an important and broad application prospect. ROS integrates various software packages that can realize different functions, such as positioning drawing, action planning, perception, simulation, etc. However, some vulnerabilities may damage the overall safety and reliability of robot system directly. In this study, an ROS oriented fuzzing method is proposed to test different versions of ROS packages and find out the vulnerabilities. The proposed approach includes two modules:Test cases generation and differential fuzz testing execution. Firstly, load and process the input file, and generate the test cases file based on the strategy's generation. Secondly, communication among nodes is achieved using topic communication mechanism, and the test case files are used as the inputs to carry out differential fuzz testing on the ROS packages. Then, the inconsistent outputs in the test results are calculated and evaluated, and the seed meet the evaluation indicators are reserved and fed back to the test case generation module to generate test cases, it will improve seed quality and code coverage effectively. Finally, analyze the cause of inconsistent output and find out the vulnerability. This method is applied in the experiment of robot coordinate transformation, testing the packages TF and TF2 that realize coordinate transformation under different reference frames. Final experiment results show that TF is more accurate in function implementation compared with TF2, and there are vulnerabilities in the function of TF2 to realize coordinate rotation transformation.
2021, 32(6):1882-1909.
DOI: 10.13328/j.cnki.jos.006255
Abstract:
Matrix is a commonly used data structure in the field of engineering. In the field of deep learning, matrix multiplication is one of the key technologies in neural network training. Faced with the problem of operations of large matrices, the block matrix technology can be used to convert large matrix operations into small matrix operations to realize parallel computation, which can greatly reduce matrix operation steps and improve the efficiency of matrix operation. Firstly, this study systematically summarizes the current matrix formalization work in academia and analyzes the main methods of matrix formalization. Secondly, it introduces and improves the matrix formalization method based on Coq record type, which includes putting forward a new definition of matrix equivalence, sorting out and perfecting the previous formalization work and proving a new set of lemmas; then on this basis, the formalization of block matrix operations is further realized, and the difficulties and solutions of this type of inductive proof are discussed. Finally, basic libraries with different types for matrix and block matrix formalization are realized.
Matrix is a commonly used data structure in the field of engineering. In the field of deep learning, matrix multiplication is one of the key technologies in neural network training. Faced with the problem of operations of large matrices, the block matrix technology can be used to convert large matrix operations into small matrix operations to realize parallel computation, which can greatly reduce matrix operation steps and improve the efficiency of matrix operation. Firstly, this study systematically summarizes the current matrix formalization work in academia and analyzes the main methods of matrix formalization. Secondly, it introduces and improves the matrix formalization method based on Coq record type, which includes putting forward a new definition of matrix equivalence, sorting out and perfecting the previous formalization work and proving a new set of lemmas; then on this basis, the formalization of block matrix operations is further realized, and the difficulties and solutions of this type of inductive proof are discussed. Finally, basic libraries with different types for matrix and block matrix formalization are realized.
2021, 32(6):1910-1922.
DOI: 10.13328/j.cnki.jos.006036
Abstract:
It needs supernumerary overhead to prove the correctness of computation results in traditional delegation computing, that cause less efficient and high overhead. This study addresses these problems, proposes a rational delegation computing protocol based on rational trust model by combining the thinking of game theory and rational trust modeling. In order to ensure the reliability of computation results, appropriate utility function incentive calculator is set up to execute protocol honestly. Firstly, construct the rational trust model based on the thinking of rational trust modeling. The lifetime of server is taken as parameter to design the utility function which contented profit of participants of delegation computing; analyze behavior strategy of participants in protocol further, when they take "honest" strategy, they can earn the point of Nash equilibrium. Secondly, design rational delegation computing protocol by combining Pedersen commitment scheme and NTRU public key cryptosystem, with the advantage of high speed, high level security, and ability of resistant to quantum computing attacks. Finally, this protocol is analyzed from three aspects:correctness, security, and performance, and affection of the lifetime on the utility of participants is proven through experiment, the outcome shows reliability of computation results can be ensured effectively by the proposed protocol.
It needs supernumerary overhead to prove the correctness of computation results in traditional delegation computing, that cause less efficient and high overhead. This study addresses these problems, proposes a rational delegation computing protocol based on rational trust model by combining the thinking of game theory and rational trust modeling. In order to ensure the reliability of computation results, appropriate utility function incentive calculator is set up to execute protocol honestly. Firstly, construct the rational trust model based on the thinking of rational trust modeling. The lifetime of server is taken as parameter to design the utility function which contented profit of participants of delegation computing; analyze behavior strategy of participants in protocol further, when they take "honest" strategy, they can earn the point of Nash equilibrium. Secondly, design rational delegation computing protocol by combining Pedersen commitment scheme and NTRU public key cryptosystem, with the advantage of high speed, high level security, and ability of resistant to quantum computing attacks. Finally, this protocol is analyzed from three aspects:correctness, security, and performance, and affection of the lifetime on the utility of participants is proven through experiment, the outcome shows reliability of computation results can be ensured effectively by the proposed protocol.
联系方式
- 《Journal of Software 》
- 主办单位：Institute of Software, CAS, China
- 邮编：100190
- 电话：010-62562563
- 电子邮箱：jos@iscas.ac.cn
- 网址：https://www.jos.org.cn
- 刊号：ISSN 1000-9825
- CN 11-2560/TP
- 国内定价：70元
You are the firstVisitors
Copyright: Institute of Software, Chinese Academy of Sciences Beijing ICP No. 05046678-4
Address：4# South Fourth Street, Zhong Guan Cun, Beijing 100190,Postal Code：100190
Phone：010-62562563 Fax：010-62562533 Email：jos@iscas.ac.cn
Technical Support：Beijing Qinyun Technology Development Co., Ltd.
Copyright: Institute of Software, Chinese Academy of Sciences Beijing ICP No. 05046678-4
Address：4# South Fourth Street, Zhong Guan Cun, Beijing 100190,Postal Code：100190
Phone：010-62562563 Fax：010-62562533 Email：jos@iscas.ac.cn
Technical Support：Beijing Qinyun Technology Development Co., Ltd.
