Detection of infeasible paths is required in many areas including test coverage analysis, test case generation, security vulnerability analysis, etc. Existing approaches typically use static analysis coupled with symbolic evaluation, heuristics, or path-pattern analysis. This paper is related to these approaches but with a different objective. It is to analyze code of real systems to build patterns of unsatisfiable constraints in infeasible paths. The resulting patterns can be used to detect infeasible paths without the use of constraint solver and evaluation of function calls involved, thus improving scalability. The patterns can be built gradually. Evaluation of the proposed approach shows promising results.

Buffer overflow vulnerability is one of the commonly found significant security vulnerabilities. This vulnerability may occur if a program does not sufficiently prevent input from exceeding intended size and accessing unintended memory locations. Researchers have put effort in different directions to address this vulnerability. How, authorized reports and data showed that as more sophisticated attack vectors are being discovered, efforts on a single direction are not sufficient to resolve this critical issue well. In this paper, we characterize buffer overflow vulnerability in four patterns and propose ABOR, a framework to remove buffer overflow vulnerabilities from source code automatically. It only patches identified code segments, which means it is an optimized solution that eliminates buffer overflows at the maximum while adds runtime overhead at the minimum. We have implemented the proposed approach and evaluated ABOR over a set of real world C/C++ applications. The results prove ABOR’s effectiveness in practice.

Buffer overflow vulnerability is one of the commonly found significant security vulnerabilities. This vulnerability may occur if a program does not sufficiently prevent input from exceeding intended size or accessing unintended memory locations. Researchers have put effort in different directions to address this vulnerability, including creating a run-time defence mechanism, proposing effective detection methods or automatically modifying the original program to remove the vulnerabilities. These techniques share many commonalities and also have differences. In this paper, we characterize buffer overflow vulnerability in the form of four patterns and propose ABOR--a framework that integrates, extends and generalizes existing techniques to remove buffer overflow vulnerability more effectively and accurately. ABOR only patches identified code segments; thus it is an optimized solution that can eliminate buffer overflows while keeping a minimum runtime overhead. We have implemented the proposed approach and evaluated it through experiments on a set of benchmarks and three industrial C/C++ applications. The experiment result proves ABORâ s effectiveness in practice.

In Android-based mobile computing, since the original Java source code is irretrievable from Dalvik bytecode, intermediate representations (IRs) were developed to represent Dalvik bytecode in readable form. To date, SMALI, JASMIN, and JIMPLE are all used as Android application IRs by mobile developers, testers and researchers. Here, we compare these three IRs via randomized event-based testing (Monkey testing) to determine that which most accurately preserves the original program behaviors in terms of the number of successfully injected events. As such program behaviors are critical to mobile security, the choice of IR is crucial during software security testing. In our experiment, we developed an event-based comparative scheme, and conducted a comprehensive empirical study. Statistical comparison of the three IRs’ program behaviors shows that SMALI behaves closest to the original applications and hence is the most suitable for software security testing as the most accurate alternative to the original Java source code (which is usually not publicly available). Keywords-intermediate representation; program behaviors; event-based testing; Android computing; SMALI; JASMIN; JIMPLE

Software often crashes despite tremendous effort on software quality assurance. Once developers receive a crash report, they need to reproduce the crash in order to understand the problem and locate the fault. However, limited information from crash reports often makes crash reproduction difficult. Many "capture-and-replay" techniques have been proposed to automatically capture program execution data from the failing code, and help developers replay the crash scenarios based on the captured data. However, such techniques often suffer from heavy overhead and introduce privacy concerns. Recently, methods such as BugRedux were proposed to generate test input that leads to crash through symbolic execution. However, such methods have inherent limitations because they rely on conventional symbolic execution techniques. In this paper, we propose a dynamic symbolic execution method called SymCon, which addresses the limitation of conventional symbolic execution by selecting functions that are hard to be resolved by a constraint solver and using their concrete runtime values to replace the symbols. We then propose SymCrash, a selective recording approach that only instruments and monitors the hard-to-solve functions. SymCrash can generate test input for crashes through SymCon. We have applied our approach to successfully reproduce 13 failures of 6 real-world programs. Our results confirm that the proposed approach is suitable for reproducing crashes, in terms of effectiveness, overhead, and privacy. It also outperforms the related methods.

Infeasible branches are program branches that can never be exercised regardless of the inputs of the program. Detecting infeasible branches is important to many software engineering tasks such as test case generation and test coverage measurement. Applying full-scale symbolic evaluation to infeasible branch detection could be very costly, especially for a large software system. In this work, we propose a code pattern based method for detecting infeasible branches. We first introduce two general patterns that can characterize the source code containing infeasible branches. We then develop a tool, called Pattern-based method for Infeasible branch Detection (PIND), to detect infeasible branches based on the discovered code patterns. PIND only performs symbolic evaluation for the branches that exhibit the identified code patterns, therefore significantly reduce the number of symbolic evaluations required. We evaluate PIND from two aspects: accuracy and efficiency. The experimental results show that PIND can effectively and efficiently detect infeasible branches in real-world Java and Android programs. We also explore the application of PIND in measuring test case coverage,

Software often crashes despite tremendous effort on software quality assurance. Once developers receive a crash report, they need to reproduce the crash in order to understand the problem and locate the fault. However, limited information from crash reports often makes crash reproduction difficult. Many "capture-and-replay" techniques have been proposed to automatically capture program execution data from the failing code, and help developers replay the crash scenarios based on the captured data. However, such techniques often suffer from heavy overhead and introduce privacy concerns. Recently, methods such as BugRedux were proposed to generate test input that leads to crash through symbolic execution. However, such methods have inherent limitations because they rely on conventional symbolic execution techniques. In this paper, we propose a dynamic symbolic execution method called SymCon, which addresses the limitation of conventional symbolic execution by selecting functions that are hard to be resolved by a constraint solver and using their concrete runtime values to replace the symbols. We then propose SymCrash, a selective recording approach that only instruments and monitors the hard-to-solve functions. SymCrash can generate test input for crashes through SymCon. We have applied our approach to successfully reproduce 13 failures of 6 real-world programs. Our results confirm that the proposed approach is suitable for reproducing crashes, in terms of effectiveness, overhead, and privacy. It also outperforms the related methods.

Input manipulation vulnerabilities such as SQL Injection, Cross-site scripting, Buffer Overflow vulnerabilities are highly prevalent and pose critical security risks. As a result, many methods have been proposed to apply static analysis, dynamic analysis or a combination of them, to detect such security vulnerabilities. Most of the existing methods classify vulnerabilities into safe and unsafe. They have both false-positive and false-negative cases. In general, security vulnerability can be classified into three cases: (1) provable safe, (2) provable unsafe, (3) unsure. In this paper, we propose a hybrid framework-Detecting Input Manipulation Vulnerabilities (DIMV), to verify the adequacy of security vulnerability defenses for input manipulation vulnerabilities by integrating formal verification with vulnerability prediction in a seamless way. The verification part takes into account sink predicates and effect of domain and custom specifications for detecting input manipulation vulnerabilities. Proving from specification is used as far as possible. Cases that cannot be proved are then predicted from the signatures mined. Our evaluation shows the practicality of the proposed framework.

Each execution of the program follows one path through its control flow graph. In general, a program has a large number of such paths. Most of the programs have an infinite number of these paths. Regardless of the quality of the program and the programming language used to develop it, in general, a sizable number of these paths are infeasible that is no input can exercise them. Detection of these infeasible paths has a key impact in many software engineering activities including code optimization, testing and even software security. This paper reviews the approaches for detecting infeasible paths, discusses the challenges and proposes to revisit this important problem by considering also empirical aspect in conjunction to formal program analysis.

Buffer overflow vulnerability is one of the major security threats for applications written in C/C++. Among the existing approaches for detecting buffer overflow vulnerability, though flow sensitive based approaches offer higher precision but they are limited by heavy overhead and the fact that many constraints are unsolvable. We propose a novel method to efficiently detect vulnerable buffer overflows in any given control flow graph through recognizing two patterns. The proposed approach first uses syntax analysis to filter away those branches that cannot possibly comply with any of the two patterns before applying a limited symbolic evaluation for a precise matching against the patterns. The proposed approach only needs to evaluate a limited set of selected branch predicates according to the patterns and avoids the need to deal with a large number of general branch predicates. This significantly improves the scalability while not sacrificing the detection precision. Our experiments demonstrate the scalability and efficiency of the proposed method, which demonstrates its applicability.

A program has many and usually an infinite number of logic paths from its entry point to its exit point. Each execution of the program follows one of its logic paths. Regardless of the quality of the program and the programming language used to develop it, in general, a sizable number of these paths are infeasible — that is no input can exercise them. Detection of these infeasible paths has a key impact in many software engineering activities including code optimization, testing and even software security. This article reviews methods for detecting infeasible paths and proposes to revisit this important problem by considering also empirical aspect in conjunction to program analysis.

A large proportion of software systems are database applications. Functionalities provided in these applications are very much associated with their databases. Hence, a lot of designs for these applications can be inferred from their databases. However, most of the design and verification techniques do not take advantage from these important and fundamental characteristics that are generally applied across database applications. Based on these characteristics, this paper proposes a design verification approach for database applications. The proposed verification is grounded on the fact that all data maintained in a database must be inserted, used and removed. These data may also require to be modified. Our evaluation finds that the proposed design verification is useful and effective in detecting essential functionalities that are not provided originally.

3D visualisation plays an important role in understanding abstract and complex concepts. In this paper, we move one step further by proposing a 3D multiuser collaborative virtual environment (CVE) system for e-learning. It provides an engaging learning environment, where the students and lecturers can collaboratively interact with the 3D e-learning contents, which will response based on law of physics or simulation rules. This would be particularly useful for those subjects that require multiuser collaboration. It also bridges the gap between lecturers and students by providing virtual real-time interactions, thus overcoming the limitations resulted from the distance issue in the Distance Learning.

The Web3D technologies make it possible to create Collaborative Virtual Environment (CVE) in the popular Internet, thus promoting the popularity of CVE scientific applications to broader areas and making it easily accessible to more online users. However, the scalability of a Large-scale CVE (LCVE) is still limited by the constraints in processing power and network speed of each participating host. In this paper, we propose an Intelligent Mobile Agent Framework for LCVE in heterogeneous internet environment. In our approach, the system functions are decomposed into independent and fine grained tasks. The tasks are modeled as intelligent mobile agents which are not bound to any fixed nodes as the traditional CVE architectures do. As the intelligent mobile agents can autonomously migrate or clone at any suitable participating host dynamically at run-time, the system workloads can be distributed more pervasively to avoid potential bottleneck. This improves the scalability of LCVE. Our experiments results have demonstrated the scalability of our proposed approach.