Narrow Results

We present a generic aproach to the static analysis of concurrent programs with procedures. We model programs as communicating pushdown systems. It is known that typical dataflow problems for this model are undecidable, because the emptiness problem for the intersection of context-free languages, which is undecidable, can be reduced to them. In this paper we propose an algebraic framework for defining abstractions (upper approximations) of context-free languages. We consider two classes of abstractions: finite-chain abstractions, which are abstractions whose domains do not contain any infinite chains, and commutative abstractions corresponding to classes of languages that contain a word if and only if they contain all its permutations. We show how to compute such approximations by combining automata theoretic techniques with algorithms for solving systems of polynomial inequations in Kleene algebras.

Dynamic networks of Pushdown Systems (DNPS in short) have been introduced to perform static analysis of concurrent programs that may spawn threads dynamically. In this model the set of successors of a regular set of configurations can be non-regular, making forward analysis of these models difficult. We refine the model by adding the associative-commutative properties of parallel composition, and we define Presburger weighted tree automata, an extension of weighted automata and tree automata, that accept the set of successors of a regular set of configurations. This yields decidability of the forward analysis of DNPS. Finally, we extend this result to the model where configurations are sets of threads running in parallel.

We investigate the decidability of the feasibility problem for imperative programs with bounded loops. A program is called feasible if all values it computes are polynomially bounded in terms of the input. The feasibility problem is representative of a group of related properties, like that of polynomial time complexity. It is well known that such properties are undecidable for a Turing-complete programming language. They may be decidable, however, for languages that are not Turing-complete. But if these languages are expressive enough, they do pose a challenge for analysis. We are interested in tracing the edge of decidability for the feasibility problem and similar problems.

In previous work, we proved that such problems are decidable for a language where loops are bounded but indefinite (that is, the loops may exit before completing the given iteration count). In this paper, we consider definite loops. A second language feature that we vary, is the kind of assignment statements. With ordinary assignment, we prove undecidability of a very tiny language fragment. We also prove undecidability with lossy assignment (that is, assignments where the modified variable may receive any value bounded by the given expression, even zero). But we prove decidability with max assignments (that is, assignments where the modified variable never decreases its value).

In this work we present an algorithm for solving the reachability problem in finite systems that are modelled with process algebras. Our method is based on Static Analysis, in particular, Data Flow Analysis, of the syntax of a process algebraic system with multi-way synchronisation. The results of the Data Flow Analysis are used in order to build a set of Horn clauses whose least model corresponds to an overapproximation of the reachable states. The computed model can be refined after each transition, and the algorithm runs until either a state whose reachability should be checked is encountered or it is not in the least model for all constructed states and thus is definitely unreachable. The advantages of the algorithm are that in many cases only a part of the Labelled Transition System will be built which leads to lower time and memory consumption. Also, it is not necessary to save all the encountered states which leads to further reduction of the memory requirements of the algorithm.

Auto-scoping in OpenMP has been proposed as a means for relieving the programmer from the non-trivial effort of identifying the data sharing attributes of variables used within code regions that produce concurrency, such as parallel and task constructs. In this work we reconsider autoscoping on parallel constructs, including combined parallel-worksharing constructs. We first show that the current implementations do not always scope variables correctly in the presence of nested parallel constructs. We then proceed to extend the set of rules that guide the autoscoping decisions so as to handle nested constructs successfully. We also discuss how this functionality is implemented in the OMPi source-to-source OpenMP compiler.

The design complexity and outsourcing trend of modern integrated circuits (ICs) have increased the chance for adversaries to implant hardware Trojans (HTs) in the development process. To effectively defend against this hardware-based security threat, many solutions have been reported in the literature, including dynamic and static techniques. However, there is still a lack of methods that can simultaneously detect and diagnose HT circuits with high accuracy and low time complexity. Therefore, to overcome these limitations, this paper presents an HT detection and diagnosis method for gate-level netlists (GLNs) based on different machine learning (ML) algorithms. Given a GLN, the proposed method first partitions it into several circuit cones and extracts seven HT-related features from each cone. Then, we repeat this process for the sample GLN to construct a dataset for the next step. After that, we use K-Nearest Neighbor (KNN), Decision Tree (DT) and Naive Bayes (NB) to classify all circuit cones of the target GLN. Finally, we determine whether each circuit cone is HT-implanted through the label, completing the HT detection and diagnosis for target GLN. We have applied our method to 11 GLNs from ISCAS’85 and ISCAS’89 benchmark suites. As shown in experimental results of the three ML algorithms used in our method: (1) NB costs shortest time and achieves the highest average true positive rate (ATPR) of 100%; (2) DT costs longest time but achieve the highest average true negative rate (ATNR) of 98.61%; (3) Compared to NB and DT, KNN costs a slightly longer time than NB but the ATPR and ATNR values are approximately close to DT. Moreover, it can also report the possible implantation location of a Trojan instance according to the detecting results.

The Model-Driven Development (MDD) approach shifts the focus on code to models in the software development process. In MDD, model transformations are elements that play an important role. MDD-based projects evolve along their lifecycle in a way that changes in their transformations are frequent. Before applying changes it is important to measure their impacts within the transformation. However, currently no technique helps practitioners in this direction. We propose an approach to measure the change impact in ATL model transformations. Based on static analysis, it detects the elements impacted by a change and calculates the change impact value through three metrics we defined. By using our approach, practitioners can (i) save effort and development time since the elements impacted with the change are automatically detected and (ii) better schedule and prioritize changes according to the impact value. To empirically evaluate our approach we conducted a case study.

Libraries offer reusable functionality through Application Programming Interfaces (APIs) with usage constraints such as call conditions or orders. Constraint violations, i.e. API misuses, commonly lead to bugs and security issues. Although researchers have developed various API misuse detectors in the past few decades, recent studies show that API misuse is prevalent in real-world projects, especially for secure socket layer (SSL) certificate validation, which is completely broken in many security-critical applications and libraries. In this paper, we introduce SSLDoc to effectively detect API misuse bugs, specifically for SSL API libraries. The key insight behind SSLDoc is a constraint-directed static analysis technique powered by a domain-specific language (DSL) for specifying API usage constraints. Through studying real-world API misuse bugs, we propose ISpec DSL, which covers majority types of API usage constraints and enables simple but precise specification. Furthermore, we design and implement SSLDoc to automatically parse ISpec into checking targets and employ a static analysis engine to identify potential API misuses and prune false positives with rich semantics. We have instantiated SSLDoc for OpenSSL APIs and applied it to large-scale open-source programs. SSLDoc found 45 previously unknown security-sensitive bugs in OpenSSL implementation and applications in Ubuntu. Up to now, 35 have been confirmed by the corresponding development communities and 27 have been fixed in master branch.

As the use of smartphones increases, Android, as a Linux-based open source mobile operating system (OS), has become the most popular mobile OS in time. Due to the widespread use of Android, malware developers mostly target Android devices and users. Malware detection systems to be developed for Android devices are important for this reason. Machine learning methods are being increasingly used for detection and analysis of Android malware. This study presents a method for detecting Android malware using feature selection with genetic algorithm (GA). Three different classifier methods with different feature subsets that were selected using GA were implemented for detecting and analyzing Android malware comparatively. A combination of Support Vector Machines and a GA yielded the best accuracy result of 98.45% with the 16 selected permissions using the dataset of 1740 samples consisting of 1119 malwares and 621 benign samples.

Besides the applications aimed at increasing the efficiency of the Android mobile devices, also many malicious applications, millions of Android malware according to various security company reports, are being developed and uploaded into the application stores. In order to detect those applications, a malicious Android application detection system based on permission and permission groups namely, AppPerm Analyzer has been developed. The AppPerm Analyzer software extracts the manifest and code permissions of analyzed applications, creates duple and triple permission groups from them, calculates risk scores of these permissions and permission groups according to their usage rates in malicious and benign applications and calculates the total risk score of the analyzed application. After training the software with 7776 applications in total, it is tested with 1664 benign and 1664 malicious applications. In the tests, AppPerm Analyzer detected malicious applications with an accuracy of 96.19% at most. At this point, sensitivity (true-positive ratio) is 95.50% and specificity (true-negative ratio) is 96.88%. If a false-positive ratio up to 10% is accepted, the sensitivity increases to 99.04%.

Mobile and web applications must operate and be displayed correctly on many different devices and browsers. The visual testing of web or mobile applications is usually a manual process that requires a significant amount of testing time, meaning that applications are tested only on a few devices. It is then assumed that the applications will be displayed correctly on other compatible or similar devices. This paper presents an automated visual testing method for user interfaces. The main contributions of this paper are a classification scheme for visual defects of user interfaces and the definition of an automatic visual testing method that tests applications on many different devices with varying hardware and software parameters. The method is based on an automated search for defects using heuristic and expected state prediction algorithms, which involves analyzing the resources used by applications and screenshots. The testing method works by executing applications on a full set of devices, taking a screenshot at every execution step, and analyzing each of these screenshots. The manual as well as automated testing approaches were validated on 781 of Android applications. The experimental results show that the proposed method has advantages over manual testing.

The software security issue is being paid great attention from the software development community as security violations have emerged variously. Developers often use access control techniques to restrict some security breaches to software systems’ resources. The addition of authorization constraints to the role-based access control model increases the ability to express access rules in real-world problems. However, the complexity of combining components, libraries and programming languages during the implementation stage of web systems’ access control policies may arise potential flaws that make applications’ access control policies inconsistent with their specifications. In this paper, we introduce an approach to review the implementation of these models in web applications written by Java EE according to the MVC architecture under the support of the Spring Security framework. The approach can help developers in detecting flaws in the assignment implementation process of the models. First, the approach focuses on extracting the information about users and roles from the database of the web application. We then analyze policy configuration files to establish the access analysis tree of the application. Next, algorithms are introduced to validate the correctness of the implemented user-role and role-permission assignments in the application system. Lastly, we developed a tool called VeRA, to automatically support the verification process. The tool is also experimented with a number of access violation scenarios in the medical record management system.

Software security vulnerabilities and leakages of private information are two of the main issues in modern software systems. Several different approaches, ranging from design techniques to run-time monitoring, have been applied to prevent, detect and isolate such vulnerabilities. Static taint analysis has been particularly successful in detecting injection vulnerabilities at compile time. However, its extension to detect leakages of sensitive data has been only partially investigated. In this paper, we introduce BackFlow, a backward flow reconstructor that, starting from the results of a generic taint analysis engine, reconstructs the flow of tainted data. If successful, BackFlow provides full information about the flow that such data (e.g. private information or user input) traversed inside the program before reaching a sensitive point (e.g. Internet communication or execution of an SQL query). Such information is needed to extend taint analysis to privacy analyses, since in such a scenario it is important to know which exact type of sensitive data flows to what type of communication channels. BackFlow has been implemented in Julia (an industrial static analyzer for Java, Android and .NET programs), and applied to WebGoat and different benchmarks to detect both injections and privacy issues. The experimental results prove that BackFlow is able to reconstruct the flow of tainted data for most of the true positives, it scales up to industrial applications, and it can be effectively applied to privacy analysis, such as the detection of sensitive data leaks or compliance with a data regulation.

As more mobile applications become available to a broader user base, the need to localize applications to various languages and cultures grows. The need for localization demands localization testing. In this paper, the user interface localization problems are identified and categorized. The automated testing method containing automated localization defects detection algorithms using applications’ screenshots analysis is presented. The proposed method was validated experimentally by comparing automated testing and manual review. The experiment contained an automated and manual review of 781 Android applications. The manual review results were compared with the proposed automated testing method results. The comparison shows that automated methods can save localization testing time and discover more defects. However, the proposed method does not fully substitute manual testing but can act as a helper.

Cybercriminals motivated by malign purpose and financial gain are rapidly developing new variants of sophisticated malware using automated tools, and most of these malware target Windows operating systems. This serious threat demands efficient techniques to analyze and detect zero-day, polymorphic and metamorphic malware. This paper introduces two frameworks for Windows malware detection using random forest algorithms. The first scheme uses features obtained from static and dynamic analysis for training, and the second scheme uses features obtained from static, dynamic, malware image analysis, location-sensitive hashing and file format inspections. We carried out an extensive experiment on two feature sets, and the proposed schemes are evaluated using seven standard evaluation metrics. The experiment results demonstrate that the second scheme recognizes unseen malware better than the first scheme and three state-of-the-art works. The findings show that the second scheme’s multi-view feature set contributes to its 99.58% accuracy and lowers false positive rate of 0.54%.

Call graphs facilitate various tasks in software engineering. However, for the dynamic language Python, the complex language features and external library dependencies pose enormous challenges for building the call graphs of real projects. Some program analysis techniques used for call graph construction in other languages are impractical for Python. In this paper, we present STAR, a practical technique for the construction of Python static call graphs. We reformulate call graph construction as an entity identification task. STAR leverages inter-module summary and cross-project dependencies to construct a fine-grained entity knowledge base to identify the possible nodes and edges of the call graph in the code, and then construct the call graph. Our evaluation of three benchmarks shows that (1) STAR improves recall in three benchmarks compared to three baseline tools. Especially, STAR improves the recall of reachable nodes and reachable edges compared with the state-of-the-art tool by 11.3% and 9.8%, respectively; (2) STAR achieves comparable performance as three baseline tools in execution time and memory usage and is more efficient in large projects; (3) STAR can be effectively used for the task of detecting vulnerability propagation with real-world cases. We expect our results will attract more exploration of practical methods and improve the application of Python call graphs.

Identifying key classes of a software system can help developers understand the system quickly, reduce the time for system maintenance, and prevent security risks caused by defects in key classes. So far, many approaches have been proposed to identify key classes from software systems. However, some approaches select too many key class candidates, making it inconvenient and difficult for developers to start understanding the system from these classes. For the other approaches, although the number of key class candidates is not large, their effectiveness needs to be further improved. To this end, in this paper, we propose a new model, named SAVM, to detect key classes by combining static analysis and a voting mechanism. First, we extract structural information from the source codes of a software system and construct a class coupling network (CCN) using this information. Then, we present the VRWD method that iteratively identifies important nodes in CCN based on a voting mechanism. Specifically, in each iteration, a node votes for its outgoing neighbors and in the meantime receives votes from its incoming neighbors. Afterward, the node that attains the highest voting score is elected as the important node in this turn. Finally, the corresponding classes of the selected important nodes are the key class candidates. The effectiveness of the proposed model and eight other baselines is evaluated in eight open-source Java projects. The experimental results show that although no method performs the best in all projects, according to the average ranking of the Friedman test, our method overall performs better compared to the baselines. In addition, this paper also proves through experiments that our approach can be applied to large-scale software projects. These indicate that our approach is a valuable technique for developers.

Maintaining high code quality is a crucial concern in software development. Existing studies demonstrated that developers frequently face recurrent bugs and adopt similar fix measures, known as code change patterns. As an essential static analysis technique, code pattern mining supports various tasks, including code refactoring, automated program repair, and defect prediction, thus significantly improving software development processes. A prevalent approach to identifying code patterns involves translating code changes to edit actions into a Bag-of-Words (BoW) model. However, when applied to open-source projects, this method exhibits several limitations. For instance, it overlooks function call information and disregards feature word order. This study introduces MIFA, a novel technique for mining code change patterns using multiple feature analysis. MIFA extends existing BoW methods by incorporating analysis of function calls and overall changes in the Abstract Syntax Tree (AST) structure. We selected 20 popular Python projects and evaluated MIFA in both intra-project and cross-project scenarios. The experimental results indicate that: (1) MIFA achieved higher silhouette coefficients and F1 scores compared to other state-of-the-art methods, demonstrating a superior accuracy; (2) MIFA can assist developers in detecting unique change patterns more earlier, with an efficiency improvement of over 40% compared to random sampling. Additionally, we discussed critical parameters for measuring the similarity of code changes, guiding users to apply our method effectively.

Mode analysis in logic programs has been used mainly for code optimization. The mode analysis in this paper supports the program construction process. It is applied to partially complete logic programs. The program construction process is based on schema refinements and refinements by data type operations. Refinements by data type operations are at the end of the refinement process. This mode analysis supports the proper application of refinements by data type operations. In addition, it checks that the declared modes as defined by the Data Type (DT) operations are consistent with the inferred runtime modes. We have implemented an algorithm for mode analysis based on minimal function graphs. An overview of our logic program development method and the denotational semantics of the analysis framework are presented in this paper.

Presented herein is a new method for the analysis of plates with clamped edges. The solutions for the natural frequencies of the plates are found using static analysis. The starting are the equations of motion of an isotropic rectangular plate supported on Winkler elastic foundation, with a positive or negative value. In either case, one can solve the displacements of such a plate under a given concentrated load. This deflection will be infinite if the plate losses its stiffness, or in other words, the generalized foundation is causing the plate to be unstable. The solution for the vibration frequencies of the plate is equivalent to finding the values of the negative elastic foundation that will yield infinite deflection under a point load on the plate. The solution for a clamped plate is decomposed as the sum of three cases of plates resting on elastic foundation: simply supported plate with a concentrated load, and two cases of distributed moments along opposite edges. The solution for simply supported plates with elastic foundation is found using Navier's method. For zero force, the vibration frequencies are found up to the desired accuracy by careful calculations at the neighborhood of the roots.