Volume 21,Issue 2,2010 Table of Contents
2010, 21(2):179-193.
Abstract:
This paper presents an automatic testing method, DAIDT (dynamic automatic integer-overflow detection and testing), for finding integer overflow fatal bugs in binary code. DAIDT can thoroughly test the binary code and automatically find unknown integer overflow bugs without necessarily knowing their symbol tables. It is formally proved in this paper that DAIDT can theoretically detect all the high-risk integer overflow bugs with no false positives and no false negatives. In additional, any bugs find by DAIDT can be replayed. To demonstrate the effectiveness of this theory, IntHunter has been implemented. It has found 4 new high risk integer overflow bugs in the latest releases of three high-trusted applications (two Microsoft WINS services in Windows 2000 and 2003 Server, Baidu Hi Instant Messager) by testing each for 24 hours. Three of these bugs allow arbitrary code execution and have received confirmed vulnerabilities numbers, CVE-2009-1923, CVE-2009-1924 from Microsoft Security Response Center and CVE-2008-6444 from Baidu.
This paper presents an automatic testing method, DAIDT (dynamic automatic integer-overflow detection and testing), for finding integer overflow fatal bugs in binary code. DAIDT can thoroughly test the binary code and automatically find unknown integer overflow bugs without necessarily knowing their symbol tables. It is formally proved in this paper that DAIDT can theoretically detect all the high-risk integer overflow bugs with no false positives and no false negatives. In additional, any bugs find by DAIDT can be replayed. To demonstrate the effectiveness of this theory, IntHunter has been implemented. It has found 4 new high risk integer overflow bugs in the latest releases of three high-trusted applications (two Microsoft WINS services in Windows 2000 and 2003 Server, Baidu Hi Instant Messager) by testing each for 24 hours. Three of these bugs allow arbitrary code execution and have received confirmed vulnerabilities numbers, CVE-2009-1923, CVE-2009-1924 from Microsoft Security Response Center and CVE-2008-6444 from Baidu.
2010, 21(2):194-208.
Abstract:
This paper proposes a resource-aware performance diagnostic method. For transactions in Web applications, the proposed method constructs performance profile chains based on the resource service time, which is stable for different workload characteristics. According to the anomaly of resource service time at application runtime, the proposed method provides an efficient solution to performance anomaly detection, location and diagnosis. Experimental results show that this method can effectively detect performance anomalies caused by different resource bottlenecks with changing workload characteristics.
This paper proposes a resource-aware performance diagnostic method. For transactions in Web applications, the proposed method constructs performance profile chains based on the resource service time, which is stable for different workload characteristics. According to the anomaly of resource service time at application runtime, the proposed method provides an efficient solution to performance anomaly detection, location and diagnosis. Experimental results show that this method can effectively detect performance anomalies caused by different resource bottlenecks with changing workload characteristics.
2010, 21(2):209-217.
Abstract:
This paper presents a new path sensitive algorithm for static defect detecting running in polynomial time. In this method, property state conditions are represented by abstract domain of variables, and infeasible paths can be identified when some variables’ abstract value range is empty. This method avoids the combination explosion of full path analysis by merging the conditions of identical property state at join points in the CFG (control flow graph). This algorithm has been implemented as part of a defect testing tool called DTS (defect testing system). Practical test results show that this method can reduce false positive.
This paper presents a new path sensitive algorithm for static defect detecting running in polynomial time. In this method, property state conditions are represented by abstract domain of variables, and infeasible paths can be identified when some variables’ abstract value range is empty. This method avoids the combination explosion of full path analysis by merging the conditions of identical property state at join points in the CFG (control flow graph). This algorithm has been implemented as part of a defect testing tool called DTS (defect testing system). Practical test results show that this method can reduce false positive.
2010, 21(2):218-230.
Abstract:
In this paper, a time-based multi-cycle checkpointing approach, allowing each process to take checkpoints with its own checkpoint cycle, is proposed. To ensure the advancement of consistent global checkpoint, checkpoint cycles can be adjusted according to a “P-pattern”. In the proposed approach, processes will be divided into zones, so that dependency tracking required for checkpoint cycle adjustment can be restricted in the zone scope. It makes the time-based multi-cycle checkpointing more scalable.
In this paper, a time-based multi-cycle checkpointing approach, allowing each process to take checkpoints with its own checkpoint cycle, is proposed. To ensure the advancement of consistent global checkpoint, checkpoint cycles can be adjusted according to a “P-pattern”. In the proposed approach, processes will be divided into zones, so that dependency tracking required for checkpoint cycle adjustment can be restricted in the zone scope. It makes the time-based multi-cycle checkpointing more scalable.
2010, 21(2):231-247.
Abstract:
In this paper, a framework is proposed for handling fault of service composition through analyzing fault requirements. Petri nets are used in the framework for fault detecting and its handling, which focuses on targeting the failure of available services, component failure and network failure. The corresponding fault models are given. Based on the model, the correctness criterion of fault handling is given to analyze fault handling model, and its correctness is proven. Finally, CTL (computational tree logic) is used to specify the related properties and enforcement algorithm of fault analysis. The simulation results show that this method can ensure the reliability and consistency of service composition.
In this paper, a framework is proposed for handling fault of service composition through analyzing fault requirements. Petri nets are used in the framework for fault detecting and its handling, which focuses on targeting the failure of available services, component failure and network failure. The corresponding fault models are given. Based on the model, the correctness criterion of fault handling is given to analyze fault handling model, and its correctness is proven. Finally, CTL (computational tree logic) is used to specify the related properties and enforcement algorithm of fault analysis. The simulation results show that this method can ensure the reliability and consistency of service composition.
2010, 21(2):248-260.
Abstract:
This paper proposes a way to analyze diagnosed systems using dynamic description logic. Syntax and semantics of dynamic description logic are suitable to describe both the normal and the failed behavior of the system. Then, it gives algorithms to test diagnosability of discrete-event systems by using dynamic description logic satisfiability-checking and for the construction of a diagnoser, which performs diagnostics using on-line observations of the system behavior. Throughout the paper, examples are given for illustration.
This paper proposes a way to analyze diagnosed systems using dynamic description logic. Syntax and semantics of dynamic description logic are suitable to describe both the normal and the failed behavior of the system. Then, it gives algorithms to test diagnosability of discrete-event systems by using dynamic description logic satisfiability-checking and for the construction of a diagnoser, which performs diagnostics using on-line observations of the system behavior. Throughout the paper, examples are given for illustration.
2010, 21(2):261-276.
Abstract:
This paper is concerned with trustworthy software constructed through service composition and is especially emphasizes guaranteeing the trustworthiness of networked software through dynamic evolution of composite services. First of all, a set of evolution operations preserving soundness of composite services is proposed so as to avoid the complex verification process. Second, a composite service evolution method with availability guarantee is provided, the main idea of which is to create redundant execution path to improve the availability of a composite service. Third, to deal with runtime instances after dynamic composite service evolution, a live instance migration algorithm is designed to support the correct evolution enforcement. Finally, a composite service execution engine supporting dynamic evolution is developed and the effectiveness of the proposed method is showed through a set of experiments.
This paper is concerned with trustworthy software constructed through service composition and is especially emphasizes guaranteeing the trustworthiness of networked software through dynamic evolution of composite services. First of all, a set of evolution operations preserving soundness of composite services is proposed so as to avoid the complex verification process. Second, a composite service evolution method with availability guarantee is provided, the main idea of which is to create redundant execution path to improve the availability of a composite service. Third, to deal with runtime instances after dynamic composite service evolution, a live instance migration algorithm is designed to support the correct evolution enforcement. Finally, a composite service execution engine supporting dynamic evolution is developed and the effectiveness of the proposed method is showed through a set of experiments.
2010, 21(2):277-286.
Abstract:
This paper proposes an efficient algorithm LD/RPath (lowest delay/reliability path) for service-oriented reliable multimedia delivery in a pervasive environment. LD/RPath estimates the dynamic data volume on service nodes and links through reasonable data volume approximation. And the data splitting technique is imported to convert the node delay into the edge delay. In the mean time, the reliability of nodes is considered as a coefficient of delay, so that the multimedia delivery problem is transformed into a conventional shortest path problem. Simulation results prove that LD/RPath achieves good path selection performance while imposing low overhead to the system.
This paper proposes an efficient algorithm LD/RPath (lowest delay/reliability path) for service-oriented reliable multimedia delivery in a pervasive environment. LD/RPath estimates the dynamic data volume on service nodes and links through reasonable data volume approximation. And the data splitting technique is imported to convert the node delay into the edge delay. In the mean time, the reliability of nodes is considered as a coefficient of delay, so that the multimedia delivery problem is transformed into a conventional shortest path problem. Simulation results prove that LD/RPath achieves good path selection performance while imposing low overhead to the system.
2010, 21(2):287-304.
Abstract:
In the context of component-based software development, this paper proposes an approach to transforming UML diagrams of software architecture to Markov chain for the quantitative evaluation of reliability. Based on the component-based software architecture, it utilizes four types of UML diagrams: use case, sequence, activity and component diagrams, extending them and annotating them with reliability related attributes. Then, the diagrams are transformed into a Markov chain based analysis model by constructing an intermediate model called Component Transition Graph (CTG). Result of this transformation can be directly used in the existing analysis methods to predict software reliability, which facilitates the analysis task of software designer.
In the context of component-based software development, this paper proposes an approach to transforming UML diagrams of software architecture to Markov chain for the quantitative evaluation of reliability. Based on the component-based software architecture, it utilizes four types of UML diagrams: use case, sequence, activity and component diagrams, extending them and annotating them with reliability related attributes. Then, the diagrams are transformed into a Markov chain based analysis model by constructing an intermediate model called Component Transition Graph (CTG). Result of this transformation can be directly used in the existing analysis methods to predict software reliability, which facilitates the analysis task of software designer.
2010, 21(2):305-317.
Abstract:
This paper presents a method to build and verify bytecode virtual machine. The formal definition and the operational semantics of a bytecode virtual machine (BVM) are given. CertVM (certified virtual machine) is implemented with X86 assembly code. It is proved in this paper that the CertVM is satisfied with the formal definition of the bytecode machine with simulation relation. The virtual machine implementation program is certified in the Coq proof assistant. The proof is machine checkable. This method guarantees that a certified bytecode program will run on the certified virtual machine without stuck unless hardware faults. This work does not only provide a solid theoretical foundation for reasoning about virtual machine, but also makes an important advance toward building the trustworthy software.
This paper presents a method to build and verify bytecode virtual machine. The formal definition and the operational semantics of a bytecode virtual machine (BVM) are given. CertVM (certified virtual machine) is implemented with X86 assembly code. It is proved in this paper that the CertVM is satisfied with the formal definition of the bytecode machine with simulation relation. The virtual machine implementation program is certified in the Coq proof assistant. The proof is machine checkable. This method guarantees that a certified bytecode program will run on the certified virtual machine without stuck unless hardware faults. This work does not only provide a solid theoretical foundation for reasoning about virtual machine, but also makes an important advance toward building the trustworthy software.
2010, 21(2):318-333.
Abstract:
This paper presents a method of constructing anticipatory monitors for PALTL (parameterized LTL (linear temporal logic)) based on automata theory. This paper on one hand investigates into the important concepts about the syntax, anticipatory semantics, valuation generation and binding of PALTL. It is assured that the binding and using are correct in syntax level. Then the concept of parameterized anticipatory monitor is presented consisting of the static part and the dynamic part. The static part is presented as parameterized Büchi automata, and the dynamic part is composed of the valuations of variables in the current state. While the system running, based on the static parameterized Büchi automata, the valuations of variables are dynamically generated and bound from the current state in an on-the-fly fashion, and the anticipatory monitor incrementally checks whether the current running system is satisfied with the given parameterized property. In this process, the parameterized monitor can precisely identify the minimal good/bad prefix of the monitored property.
This paper presents a method of constructing anticipatory monitors for PALTL (parameterized LTL (linear temporal logic)) based on automata theory. This paper on one hand investigates into the important concepts about the syntax, anticipatory semantics, valuation generation and binding of PALTL. It is assured that the binding and using are correct in syntax level. Then the concept of parameterized anticipatory monitor is presented consisting of the static part and the dynamic part. The static part is presented as parameterized Büchi automata, and the dynamic part is composed of the valuations of variables in the current state. While the system running, based on the static parameterized Büchi automata, the valuations of variables are dynamically generated and bound from the current state in an on-the-fly fashion, and the anticipatory monitor incrementally checks whether the current running system is satisfied with the given parameterized property. In this process, the parameterized monitor can precisely identify the minimal good/bad prefix of the monitored property.
2010, 21(2):334-343.
Abstract:
A pointer logic is designed for a C-like programming language PointerC. The pointer logic is an extension of Hoare logic, and it uses the idea of precise alias analysis in pointer program verification to support safety verification of programs in which equality of pointers is well-regulated. This paper presents an extension to the pointer logic by introducing a set of uncertain-equality pointer access path sets, so as to reason in the extended pointer logic about properties of programs which manipulate data structures like directed graph in which equality of pointers is uncertain.
A pointer logic is designed for a C-like programming language PointerC. The pointer logic is an extension of Hoare logic, and it uses the idea of precise alias analysis in pointer program verification to support safety verification of programs in which equality of pointers is well-regulated. This paper presents an extension to the pointer logic by introducing a set of uncertain-equality pointer access path sets, so as to reason in the extended pointer logic about properties of programs which manipulate data structures like directed graph in which equality of pointers is uncertain.
2010, 21(2):344-358.
Abstract:
In this paper, the existing intrusion tolerance and self-destruction technology are integrated into autonomic computing in order to construct an autonomic dependability model based on SM-PEPA (semi-Markov performance evaluation process algebra) which is capable of formal analysis and verification. It can hierarchically anticipate Threats to dependability (TtD) at different levels in a self-management manner to satisfy the special requirements for dependability of mission-critical systems. Based on this model, a quantification approach is proposed on the view of steady-state probability to evaluate autonomic dependability. Finally, this paper analyzes the impacts of parameters of the model on autonomic dependability in a case study, and the experimental results demonstrate that improving the detection rate of TtD as well as the successful rate of self-healing will greatly increase the autonomic dependability.
In this paper, the existing intrusion tolerance and self-destruction technology are integrated into autonomic computing in order to construct an autonomic dependability model based on SM-PEPA (semi-Markov performance evaluation process algebra) which is capable of formal analysis and verification. It can hierarchically anticipate Threats to dependability (TtD) at different levels in a self-management manner to satisfy the special requirements for dependability of mission-critical systems. Based on this model, a quantification approach is proposed on the view of steady-state probability to evaluate autonomic dependability. Finally, this paper analyzes the impacts of parameters of the model on autonomic dependability in a case study, and the experimental results demonstrate that improving the detection rate of TtD as well as the successful rate of self-healing will greatly increase the autonomic dependability.
2010, 21(2):359-372.
Abstract:
This paper proposes a framework supporting software assets evaluation on trustworthiness, analyzes the technologies included in this framework, such as evidence collection, trust management for evidence, trustworthiness evaluation and so on. Furthermore, this paper presents the design decisions and solutions of this framework in software asset library of Peking University. A detailed case study is also given
This paper proposes a framework supporting software assets evaluation on trustworthiness, analyzes the technologies included in this framework, such as evidence collection, trust management for evidence, trustworthiness evaluation and so on. Furthermore, this paper presents the design decisions and solutions of this framework in software asset library of Peking University. A detailed case study is also given
2010, 21(2):373-387.
Abstract:
This paper extends the software trustworthiness evidence framework to include the runtime software trustworthiness evidence. To collect software trustworthiness evidence in an objective, genuine and comprehensive way, it proposes a runtime software trustworthiness evidence collection mechanism based on trusted computing technology. Based on the features provided by TPM (trusted platform module), as well as the late launch technology, a trusted evidence collection agent is introduced in an operating system kernel. The agent can securely monitor executing programs and collect their trustworthiness evidence accordingly. The agent also provides some trusted services for programs to collect application specific evidences and guarantees the trustworthiness of these evidences. This mechanism has good scalability to support various applications and software trustworthiness evaluation models. This paper also implements a prototype for the agent based on Linux security model in Linux. Based on the prototype, it studies the trustworthiness evaluation for executing a client program in a distributed computing environment. In this application, the performance of prototype is studied, and the feasibility of this approach is demonstrated.
This paper extends the software trustworthiness evidence framework to include the runtime software trustworthiness evidence. To collect software trustworthiness evidence in an objective, genuine and comprehensive way, it proposes a runtime software trustworthiness evidence collection mechanism based on trusted computing technology. Based on the features provided by TPM (trusted platform module), as well as the late launch technology, a trusted evidence collection agent is introduced in an operating system kernel. The agent can securely monitor executing programs and collect their trustworthiness evidence accordingly. The agent also provides some trusted services for programs to collect application specific evidences and guarantees the trustworthiness of these evidences. This mechanism has good scalability to support various applications and software trustworthiness evaluation models. This paper also implements a prototype for the agent based on Linux security model in Linux. Based on the prototype, it studies the trustworthiness evaluation for executing a client program in a distributed computing environment. In this application, the performance of prototype is studied, and the feasibility of this approach is demonstrated.
2010, 21(2):388-400.
Abstract:
Since online system evolution requires efficient service selection to meet with the high dynamics demand of open system, this paper proposes a reputation-based recommender discovery approach. It qualifies trust relationships in different recommendation contexts via a relative factor, divides the Web of trust into personalized trust networks by applying a segment algorithm and finally locates recommenders with high reputation through trust opinion iteration among users. Simulation results show that the suggested approach in this paper helps to reduce the cost in information collection as well as improve the efficiency and precision of service selection results.
Since online system evolution requires efficient service selection to meet with the high dynamics demand of open system, this paper proposes a reputation-based recommender discovery approach. It qualifies trust relationships in different recommendation contexts via a relative factor, divides the Web of trust into personalized trust networks by applying a segment algorithm and finally locates recommenders with high reputation through trust opinion iteration among users. Simulation results show that the suggested approach in this paper helps to reduce the cost in information collection as well as improve the efficiency and precision of service selection results.
联系方式
- 《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.
