2011, 22(3):353-365. DOI: 10.3724/SP.J.1001.2011.03867 CSTR:
Abstract:In this paper, the fast continuous weak Hash (FCWH) in strings is proposed and its theoretic and practical applications are investigated. First, FCWH is conceptualized and a uniform construction framework for FCWH is formulized from an algebraic viewpoint. Secondly, the theoretical and experimental collision probabilities of FCWH are analyzed, and the related work by Michael O. Rabin is generalized and strengthened. Finally, by generalizing the Karp-Rabin algorithm for string-matching problem, FCWH is applied to solve the problem of sequential extraction of common substrings (SECS), and, based on SECS, the express synchronization (X-Sync) protocol is designed to address the issue of real-time backup and the retrieval of multiple versions of a given document in the current environment of broadband communication network and cloud computing.
2011, 22(3):366-380. DOI: 10.3724/SP.J.1001.2011.03918 CSTR:
Abstract:To verify the properties of concurrent and reactive systems based on the theorem proving approach, a complete axiomatization is formulized over finite domains for first order projection temporal logic (PTL) with finite time. First, the syntax, semantics and the axiomatization of PTL are presented; next, a normal form (NF) and a normal form graph (NFG) of PTL formulas are defined respectively; further, the algorithm for constructing the NFG is formalized upon the NF; moreover, the decision theorem for PTL formulas and the completeness of the axiomatic system have been proven to be based on the property that the NFG can-describe the models of PTL formulas; finally, an example is given to illustrate how to do system verification based on PTL and its axiomatic system, and the results indicate that the PTL based theorem proving approach can be conveniently applied to modeling and verification of concurrent systems.
MA Yu-Tao , HE Ke-Qing , LI Bing , LIU Jing
2011, 22(3):381-407. DOI: 10.3724/SP.J.1001.2011.03934 CSTR:
Abstract:The popularity of the Internet and the boom of the World Wide Web foster innovative changes in software technology that give birth to a new form of software—networked software, which delivers diversified and personalized on-demand services to the public. With the ever-increasing expansion of applications and users, the scale and complexity of networked software are growing beyond the information processing capability of human beings, which brings software engineers a series of challenges to face. In order to come to a scientific understanding of this kind of ultra-large-scale artificial complex systems, a survey research on the infrastructure, application services, and social interactions of networked software is conducted from a three-dimensional perspective of cyberization, servicesation, and socialization. Interestingly enough, most of them have been found to share the same global characteristics of complex networks such as “Small World” and “Scale Free”. Next, the impact of the empirical study on software engineering research and practice and its implications for further investigations are systematically set forth. The convergence of software engineering and other disciplines will put forth new ideas and thoughts that will breed a new way of thinking and input new methodologies for the study of networked software. This convergence is also expected to achieve the innovations of theories, methods, and key technologies of software engineering to promote the rapid development of software service industry in China.
ZHONG Hao , ZHANG Lu , MEI Hong
2011, 22(3):408-416. DOI: 10.3724/SP.J.1001.2011.03931 CSTR:
Abstract:Invocation Specifications of an API library are types of specifications that are able to describe the legal invocation sequences of methods. Client code should follow descriptions of invocation specifications to call upon methods provided by API libraries. If this procedure is not followed, defects can be introduced into client code, and reduce its integrity. Because invocation specifications define the properties that are trustworthy for a software system, they play a central role in the research of trustworthy software and model checking; however, due to the great efforts to write invocation specifications, most API libraries do not provide such specifications. To address the problem, researchers have proposed various approaches to mine invocation specifications automatically. In this paper update-to-date research of mining specifications is surveyed, and the potential direction of further research is discussed.
SONG Wei , MA Xiao-Xing , HU Hao , Lü Jian
2011, 22(3):417-438. DOI: 10.3724/SP.J.1001.2011.03962 CSTR:
Abstract:Supporting the evolution of process model at run-time stage and propagating the changes of process model to the active process instances are fundamental requirements for any flexible process-aware information systems (PAIS). Instance migration is regarded as the mainstream technique that deals with the dynamic evolution of process-aware information systems. By using this technique, active process instances are migrated to the modified process model, so that they can benefit from the optimization process. The challenges are 1) to guarantee that the process instances can be correctly migrated to the modified process model; 2) to efficiently check whether the process instances can be migrated. From this view, this paper surveys the state-of-the-art dynamic evolution of processes in PAIS. Finally, some potential research directions on evolution of processes are proposed for future references.
XU Gao-Chao , LIU Xin-Zhong , HU Liang , FU Xiao-Dong , DONG Yu-Shuang
2011, 22(3):439-450. DOI: 10.3724/SP.J.1001.2011.03739 CSTR:
Abstract:Mostly, defect correlation is caused by the defect detected capability masked by other defects. Defect correlation affects the result of the test and makes the results in accurate and distorts the estimated results of software reliability assessment models. From the standpoint of defects themselves, this paper makes a detailed analysis of defect correlation and gives the reasons of the software testing and reliability assessment out of action. By applying the generalized correlation to improve the existing reliability assessment models, this paper puts forward the P-NHPP (phase-nonhomogeneous poisson process) reliability model to make the reliability assessment parameters more coordinated with the actual defect number. Experimental results show that P-NHPP is better and has a fairly accurate prediction capability.
LI Qiao-Qin , LIU Ming , YANG Mei , CHEN Gui-Hai
2011, 22(3):451-465. DOI: 10.3724/SP.J.1001.2011.03944 CSTR:
Abstract:In a multi-hop wireless sensor network (WSN), sensor nodes closer to the sink have to take a heavier traffic load, and thus, these sensor nodes tend to deplete their energy faster. This uneven energy depletion leads to what is called an energy hole around the sink. If this happens, no more data can be delivered to the sink, and a considerable amount of energy is wasted. This paper investigates the energy hole problem in WSNs. Based on the analysis of traffic load distribution in the continuous space of the network, a load-similar node distribution strategy is proposed to balance energy consumption and solve the energy hole problem. Sensor nodes are deployed according to the load distribution. Most nodes will be deployed in the range where the average load is higher. The impact of idle listening is also investigated. Simulation results demonstrate that the load-similar node distribution strategy prolongs a longer network lifetime than existing nonuniform node distribution and uniform node distribution strategies that do not take in consideration idle listening. When idle listening is considered, the energy consumed on idle listening plays an important part in the overall energy consumption and impacts the network lifetime. The load-similar node distribution improves the network lifetime, although the improvement is not as prominent as without considering idle listening. The analysis model and the proposed load-similar node distribution strategy have the potential to be applied to other multi-hop WSN structures.
SONG Chao , LIU Ming , GONG Hai-Gang , CHEN Gui-Hai , WANG Xiao-Min
2011, 22(3):466-480. DOI: 10.3724/SP.J.1001.2011.03808 CSTR:
Abstract:This paper proposes a Distributed Real-time Information based Routing Protocol in vehicular ad-hoc networks (DRIP). Based on the proposed Distributed Real-time Delay Evaluation Scheme (DRES), vehicles obtain the real-time information for the network status of each road, and according to the delay evaluation of each road, vehicles use DRIP for an effective data delivery. Compared with existing protocols, DRIP has the characters of being effective and having a low resource consumption rate. The simulation results indicate that DRIP performs well.
HU Ning , ZHU Pei-Dong , ZOU Peng
2011, 22(3):481-494. DOI: 10.3724/SP.J.1001.2011.03734 CSTR:
Abstract:The cooperative routing monitoring constructs a more complete global information view by information sharing among autonomous systems (ASes), which can eliminate the negative impact of the autonomous inter-domain routing system characteristic and improve the route monitoring ability of AS. This paper designs an information sharing mechanism called CoISM that is based on self-organization for the information sharing, which is the essential issue of cooperative route monitoring. CoISM leverages the localization caused by BGP policy to reduce and control the transmit range of information. It also uses information reflection to implement the information active push and builds AS profit on its altruistic information sharing behavior. This mechanism leads to information aggregation, as needed in self-organization, and facilitates cooperation among AS by its incentive. CoISM adopts a distributed architecture and has good expansibility and a lower communication overhead. In addition, it does not modify the BGP protocol, but supports an incremental deployment and can be used in many cross-domain cooperative management applications such as inter-domain routing monitoring, cooperative routing failure analysis, cooperative intrusion detection, and so on.
ZHANG Yong , TAN Xiao-Bin , CUI Xiao-Lin , XI Hong-Sheng
2011, 22(3):495-508. DOI: 10.3724/SP.J.1001.2011.03751 CSTR:
Abstract:To analyze the influence of propagation on a network system and accurately evaluate system security, this paper proposes an approach to improve the awareness of network security, based on the Markov Game Model (MGM). This approach gains a standard data of assets, threats, and vulnerabilities via fusing a variety of system security data collected by multi-sensors. For every threat, it analyzes the rule of propagation and builds a threat propagation network (TPN). By using the Game Theory to analyze the behaviors of threats, administrators, and ordinary users, it establishes a three player MGM. In order to make the evaluation process a real-time operation, it optimizes the related algorithm. The MGM can dynamically evaluate system security situation and provide the best reinforcement schema for the administrator. The evaluation of a specific network indicates that the approach is suitable for a real network environment, and the evaluation result is precise and efficient. The reinforcement schema can effectively curb the propagation of threats.
CHEN Ming , WU Kai-Gui , WU Chang-Ze , XU Jie , WU Zhong-Fu
2011, 22(3):509-521. DOI: 10.3724/SP.J.1001.2011.03945 CSTR:
Abstract:The fairness and punctuality of optimistic fair exchange protocols are difficult to analyze by using belief logic. Based on the studies of existing formal models and security attributes in fair exchange, a formal model for logic reasoning and fair exchange protocols is proposed. In the model, the channel errors are transferred to the attacker’s behaviors, the participants are divided into honest and dishonest ones, and the threats are attributed to two types of intruders. Based on the idea of model checking, the protocols are defined as an evolved system that has the Kripke structure, and the parties are considered as processes in an asynchronous environment. The new logic stimulates the time operators to control the transfers among the participants’ behaviors and is simple and easy to use. Through typical optimistic fair exchange protocols, the article demonstrates the course of protocol analysis. Two flaws of the protocol are discovered and improved. The case study shows that the new logic can be used to analyze the fairness and timeliness of fair exchange protocols.
KONG De-Guang , TAN Xiao-Bin , XI Hong-Sheng , GONG Tao , SHUAI Jian-Mei
2011, 22(3):522-533. DOI: 10.3724/SP.J.1001.2011.03727 CSTR:
Abstract:To cope with the problem of the low accuracy in detecting obfuscated malware, an algorithm to detect obfuscated malware based on boosting multi-level features is presented. After a disassembly analysis and static analysis for the obfuscated malware, the algorithm extracts features from three dimensions: opcode distribution, a function call graph, and a system call graph, which combines the statistic and semantic features to reflect the behavior characteristic of the malware, and then gives out the decision result based on weighted voting for a different feature analysis. It has been proven by experiment that the algorithms have a much higher accuracy on the testing dataset.
LEI Xin-Feng , LIU Jun , XIAO Jun-Mo
2011, 22(3):534-557. DOI: 10.3724/SP.J.1001.2011.03732 CSTR:
Abstract:In cryptographic protocols, the agent’s epistemic and doxastic states are changeable over time. To model these dynamics, a time-dependent cryptographic protocol logic is proposed. Our logic is based on the predicate modal logic and the time factor can be expressed in it by invoking a time variable as a parameter of predicates and modal operators. This makes it possible to model every agent’s actions, knowledges and beliefs at different time points. We also give the formal semantics of our logic to avoid the ambiguity of its language and make the logic sound. The semantics is based on the kripke structure and the possible world in it is built both on the local world of agent and the specific world of time. This makes every possible world can give a global view of each point of the protocol. Our logic provides a flexible method for analyzing the cryptographic protocols, especially the time-dependent cryptographic protocols, and increases the power of the logical method for analyzing protocols.
PU Bao-Xing , YANG Lu-Ming , WANG Wei-Ping
2011, 22(3):558-571. DOI: 10.3724/SP.J.1001.2011.03737 CSTR:
Abstract:Aiming at a single-source multicast network, this paper studies the intrinsic mechanism of linear network coding and proposes a technique of generation and extension between two coding schemes at different multicast rates. The coding scheme is a generation of some coding schemes at higher multicast rate, and it is also an extension of some coding schemes at lower multicast rates. Furthermore, the determinate relationship among channels’ global encoding vectors under two generation-extension coding schemes is discovered. By adopting random network coding, several important properties are derived, which are some of the application values and are helpful in implementing a single-source multicast connection with linear network coding. Several related applications are listed. In particular, this paper highlight a way to improve the throughput of single-source multicast network in dynamic environment and presents a random network coding approach based on retransmission and variable multicast rate, under the condition that each sink node has a feedback path to the source node. Compared with random network coding, this approach is a better way of improving the throughput of network. Simulation experiments of the listed applications have been done, and the results validate the conclusions derived from theoretical analyses.
ZHAO Xin-Jie , WANG Tao , GUO Shi-Ze , ZHENG Yuan-Yuan
2011, 22(3):572-591. DOI: 10.3724/SP.J.1001.2011.03802 CSTR:
Abstract:Firstly, this paper displays an access driven Cache timing attack model, proposes non-elimination and elimination two general methods to analyze Cache information leakage during AES encryption, and builds the Cache information leakage model. Next, it uses quantitative analysis to attack a sample with the above elimination analysis method, and provides some solutions for the potential problems of a real attack. Finally, this paper describes 12 local and remote attacks on AES in OpenSSL v.0.9.8a, v.0.9.8j. Experiment results demonstrate that: the access driven Cache timing attack has strong applicability in both local and remote environments; the AES lookup table and Cache structure decide that AES is vulnerable to this type of attack, the least sample size required to recover a full AES key is about 13; the last round AES implementation in OpenSSL v.0.9.8j, which abandoned the T4 lookup table, cannot secure itself from the access driven Cache timing attack; the attack results strongly verify the correctness of the quantitative Cache information leakage theory and key analysis methods above.