Search

Static buffer overflow detection techniques tend to report too many false positives fundamentally due to the lack of software execution information. It is very time consuming to manually inspect all the static warnings. In this paper, we propose BovInspector, a framework for automatically validating static buffer overflow warnings and providing suggestions for automatic repair of true buffer overflow warnings for C programs. Given the program source code and the static buffer overflow warnings, BovInspector first performs warning reachability analysis. Then, BovInspector executes the source code symbolically under the guidance of reachable warnings. Each reachable warning is validated and classified by checking whether all the path conditions and the buffer overflow constraints can be satisfied simultaneously. For each validated true warning, BovInspector provides suggestions to automatically repair it with 11 repair strategies. BovInspector is complementary to prior static buffer overflow discovery schemes. Experimental results on real open source programs show that BovInspector can automatically validate on average 60% of total warnings reported by static tools.

Unlike standalone embedded devices, behaviors of a cyber-physical system (CPS) are highly dynamic. Many parameter values (e.g., those related to nature environment and third party black box functions) are unknown offline. Furthermore, distributed sub-CPSs may exchange data online. In this article, we first propose the concept of parametric hybrid automata (PHA) to describe such complex CPSs. As some PHA parameter values are unknown until runtime, conventional offline model checking is infeasible. Instead, we propose to carry out PHA model checking online, as a fault prediction mechanism. However, this usage is challenged by the high time cost of state reachability verification, which is the conventional focus of model checking. To address this challenge, we propose that the model checking shall focus on online scenario reachability validation instead. Furthermore, we propose a mechanism to compose/decompose scenarios. Our scenario reachability validation can exploit linear programming to achieve polynomial time cost. Evaluations on a state-of-the-art train control system show that our approach can cut online model checking time cost from over 1 h to within 200 ms.

There is more than a decade-long history of using static analysis to find bugs in systems such as Linux. Most of the existing static analyses developed for these systems are simple checkers that find bugs based on pattern matching. Despite the presence of many sophisticated interprocedural analyses, few of them have been employed to improve checkers for systems code due to their complex implementations and poor scalability. In this article, we revisit the scalability problem of interprocedural static analysis from a “Big Data” perspective. That is, we turn sophisticated code analysis into Big Data analytics and leverage novel data processing techniques to solve this traditional programming language problem. We propose Graspan , a disk-based parallel graph system that uses an edge-pair centric computation model to compute dynamic transitive closures on very large program graphs. We develop two backends for Graspan, namely, Graspan-C running on CPUs and Graspan-G on GPUs, and present their designs in the article. Graspan-C can analyze large-scale systems code on any commodity PC, while, if GPUs are available, Graspan-G can be readily used to achieve orders of magnitude speedup by harnessing a GPU’s massive parallelism. We have implemented fully context-sensitive pointer/alias and dataflow analyses on Graspan. An evaluation of these analyses on large codebases written in multiple languages such as Linux and Apache Hadoop demonstrates that their Graspan implementations are language-independent, scale to millions of lines of code, and are much simpler than their original implementations. Moreover, we show that these analyses can be used to uncover many real-world bugs in large-scale systems code.

Missing checks for untrusted inputs used in security-sensitive operations is one of the major causes of various vulnerabilities. Efficiently detecting and repairing missing checks are essential for prognosticating potential vulnerabilities and improving code reliability. We propose a systematic static analysis approach to detect missing checks for manipulable data used in security-sensitive operations of C/C++ programs and recommend repair references. First, customized securitysensitive operations are located by lightweight static analysis. Then, the assailability of sensitive data used in securitysensitive operations is determined via taint analysis. And, the existence and the risk degree of missing checks are assessed. Finally, the repair references for high-risk missing checks are recommended. We implemented the approach into an automated and cross-platform tool named Vanguard based on Clang/LLVM 3.6.0. Large-scale experimental evaluation on open-source projects has shown its effectiveness and efficiency. Furthermore, Vanguard has helped us uncover five known vulnerabilities and 12 new bugs.

Sophisticated static analysis techniques often have complicated implementations, much of which provides logic for tuning and scaling rather than basic analysis functionalities. This tight coupling of basic algorithms with special treatments for scalability makes an analysis implementation hard to (1) make correct, (2) understand/work with, and (3) reuse for other clients. This paper presents Chianina, a graph system we developed for fully context- and flow-sensitive analysis of large C programs. Chianina overcomes these challenges by allowing the developer to provide only the basic algorithm of an analysis and pushing the tuning/scaling work to the underlying system. Key to the success of Chianina is (1) an evolving graph formulation of flow sensitivity and (2) the leverage of out-of-core, disk support to deal with memory blowup resulting from context sensitivity. We implemented three context- and flow-sensitive analyses on top of Chianina and scaled them to large C programs like Linux (17M LoC) on a single commodity PC.

Barrier certificates provide safety guarantees for hybrid systems. In this paper, we propose a novel approach to synthesizing neural networks as barrier certificates. Candidate networks are trained from a special structure: ReLU neural networks consisting of two hidden layers. Then, the problem of identifying real barrier certificates from candidates is transformed into a group of mixed integer linear programming problems and a mixed integer quadratically constrained problem. Taking full advantage of the recent advance in optimization, barrier certificates validation can be performed effectively. We implement the tool SyntheBC and evaluate its performance over 3 hybrid systems and 8 continuous systems up to 12-dimensional state space. The experimental results show that our method is more scalable and effective than the classical polynomial barrier certificate method and the existing neural network based method.

Hybrid systems are widely used in safety-critical areas. Hybrid optimal control synthesis, which aims to generate an optimal sequence of control inputs for a given task, is one of the most important problems in the field. The classical Gradient-based methods are efficient but they require the system under control should be differentiable. Sampling-based methods have no such limitations, but the ability of existing ones to solve complex control missions is restricted. In this paper, we propose a practical and efficient method to solve a general class of hybrid optimal control problems. Basically, we transform the control synthesis problem into a derivative-free optimization (DFO) problem. Then, we adapt a start-of-art classification-based DFO method to solve the optimization problems based on sampled variables efficiently. Furthermore, for complex state space, which is difficult to solve, we present a piecewise control synthesis method to make a tradeoff between optimality and efficiency by generating feasible and piecewise optimal control inputs instead. The empirical results on two complex real-world hybrid systems: a vehicle and a quadcopter drone system, demonstrate that our method outperforms existing methods significantly.

Mobile applications play an important role in our daily life, while it still remains a challenge to guarantee their correctness. Model-based and systematic approaches have been applied to Android GUI testing. However, they do not show significant advantages over random approaches because of limitations such as imprecise models and poor scalability. In this paper, we propose Q-testing, a reinforcement learning based approach which benefits from both random and model-based approaches to automated testing of Android applications. Q-testing explores the Android apps with a curiosity-driven strategy that utilizes a memory set to record part of previously visited states and guides the testing towards unfamiliar functionalities. A state comparison module, which is a neural network trained by plenty of collected samples, is novelly employed to divide different states at the granularity of functional scenarios. It can determine the reinforcement learning reward in Q-testing and help the curiosity-driven strategy explore different functionalities efficiently. We conduct experiments on 50 open-source applications where Q-testing outperforms the state-of-the-art and state-of-practice Android GUI testing tools in terms of code coverage and fault detection. So far, 22 of our reported faults have been confirmed, among which 7 have been fixed.

Barrier certificates generation is widely used in verifying safety properties of hybrid systems because of the relatively low computational complexity it costs. Under sum of squares (SOS) relaxation, the problem of barrier certificate generation is equivalent to that of solving a bilinear matrix inequality (BMI) with a particular type. The paper reveals the special feature of the problem, and adopts it to build a novel computational method. The proposed method introduces a sequential iterative scheme that is able to find analytical solutions, rather than the nonlinear solving procedure to produce numerical solutions used by general BMI solvers and thus is more efficient than them. In addition, different from popular LMI solving based methods, it does not make the verification conditions more conservative, and thus reduces the risk of missing feasible solutions. Benefitting from these two appealing features, it can produce barrier certificates not amenable to existing methods, which is supported by a complexity analysis as well as the experiment on some benchmarks.

By combining communication, computation, and control (3C), Cyber-Physical Systems (CPS)0tightly couple the physical world with the cyber-world, to enable more applications, enhance performance, increase dependability and etc. Among these goals, as CPS are widely used in the safety-critical area, guaranteeing the basic dependability/safety is after all the prerequisite and often the top concern. However, the behavior of CPS is extremely complex. First of all, due to the existence of both discrete control modes transition and continuous real-time behavior in CPS, the behavior of CPS is a complex hybrid state space, which is difficult to understand and handle. Secondly, most CPS applications are working in the open environment and acquiring real-time data from the environment intensively to adjust their own behavior. The dynamic environment makes the behavior space more complex to reason. When a system is too complex to analyze directly, building an abstract model of the system and then conducting analysis on the model to answer questions about the original system is an important and widely-used method. Meanwhile, a reasonable model also plays important roles in the phase of specification, design, development, testing, monitoring and so on. Therefore, it is an important topic of investigating how model-based methods can be applied in the context of CPS to increase the quality and dependability of the system. During the past decade, our research group at Nanjing University has devoted a lot of efforts into this mission. We conducted comprehensive research in a wide spectrum of CPS including model-driven design, verification, control, monitoring, and testing. In this paper, we will make a general review of the progress we made on these directions recently.

In safety verification of hybrid systems, barrier certificates are generated by solving the verification conditions derived from non-negative representations of different types. This paper presents a new computational method, sequential linear programming projection, for directly solving the set of verification conditions represented by the Krivine–Vasilescu–Handelman’s positivstellensatz. The key idea is to decompose it into two successive optimization problems that refine the desired barrier certificate and those undetermined multipliers, respectively, and solve it in an iterative scheme. The most important benefit of the proposed approach lies in that it is much more effective than the LP relaxation method in producing real barrier certificates, and possesses a much lower computational complexity than the popular sum of square relaxation methods, which is demonstrated by the theoretical analysis on complexity and the experiment on a set of examples gathered from the literature.

Recent advances and industry standards in Internet of Things (IoT) have accelerated the real-world adoption of connected devices. To manage this hybrid system of digital real-time devices and analog environments, the industry has pushed several popular home automation IoT (HA-IoT) frameworks, such as If-This-Then-That (IFTTT), Apple HomeKit, and Google Brillo. Typically, users author device interactions by specifying the triggering sensor event and the triggered device command. In this seemingly simple software system, two dominant factors govern the system confidence properties with respect to the physical world. First, IoT users are largely nonexperts who lack the comprehensive consideration regarding potential impact and joint effect with existing rules. Second, while the increasing complexity of IoT devices enables fine-grained control (e.g., heater temperature) of continuous real-time environments, even two simply connected devices can have a huge state space to explore. In fact, bugs that wrongfully control devices and home appliances can have ramifications on system correctness and even user physical safety. It is crucial to help users to make sure the system they created meets their expectation. In this article we introduce how techniques from hybrid automata can be practically applied to assist nonexpert IoT users in the confidence checking of such hybrid HA-IoT systems. We propose an automated framework for end-to-end programming assistance. We build and check the Linear Hybrid Automata (LHA) model of the system automatically. We also present a quantifier elimination-based method to analyze the counterexample found and synthesize fix suggestions. We implemented a platform, MenShen, based on this framework and proposed techniques. We conducted sets of real HA-IoT case studies with up to 46 devices and 65 rules. Empirical results show that MenShen can find violations and generate rule fix suggestions in only 10 seconds.

Fe@AlPO 4 core-shell composites with tunable AlPO 4 content have been successfully prepared through in situ deposition of AlPO 4 on the surface of carbonyl iron. The presence of the AlPO 4 layer improves the anti-oxidative ability of the internal carbonyl iron, so that surface oxidation and magnetic degradation in these composites are significantly suppressed when compared with naked carbonyl iron. It is worth noting that the AlPO 4 layer can affect the electromagnetic parameters of carbonyl iron, resulting in well-matched characteristic impedance. By optimizing the AlPO 4 layer content, the Fe@AlPO 4 composite can display excellent reflection loss characteristics, and qualified absorption in a very broad frequency range (2.4–18.0 GHz over −10 dB) can be achieved. The microwave absorption performance of the Fe@AlPO 4 composite is indeed superior to pure carbonyl iron as well as many previously reported carbonyl iron-based composites. More importantly, the Fe@AlPO 4 composite can maintain good microwave absorption properties after treatment at high temperature for long time periods. These results provide new insight into the fabrication of carbonyl iron-based composites with good microwave absorption and anti-oxidative properties that meet the requirements in practical applications.

Numerical instability is a well-known problem that may cause serious runtime failures. This paper discusses the reason of instability in software development process, and presents a toolchain that not only detects the potential instability in software, but also diagnoses the reason for such instability. We classify the reason of instability into two categories. When it is introduced by software requirements, we call the instability caused by problem . In this case, it cannot be avoided by improving software development, but requires inspecting the requirements, especially the underlying mathematical properties. Otherwise, we call the instability caused by practice . We design our toolchain as four loosely-coupled tools, which combine stochastic arithmetic with infinite-precision testing. Each tool in our toolchain can be configured with different strategies according to the properties of the analyzed software. We evaluate our toolchain on subjects from literature. The results show that it effectively detects and separates the instabilities caused by problems from others. We also conduct an evaluation on the latest version of GNU Scientific Library, and the toolchain finds a few real bugs in the well-maintained and widely deployed numerical library. With the help of our toolchain, we report the details and fixing advices to the GSL buglist.

The problem of probabilistic safety verification of stochastic hybrid systems is to check whether the probability that a given system will reach an unsafe region from certain initial states can be bounded by some given probability threshold. The paper considers stochastic hybrid systems where the behavior is governed by polynomial equalities and inequalities, as for usual hybrid systems, but the initial states follow some stochastic distributions. It proposes a new barrier certificate based method for probabilistic safety verification which guarantees the absolute safety in a infinite time horizon that is beyond the reach of existing techniques using either statistical model checking or probabilistic reachable set computation. It also gives a novel computational approach, by building and solving a constrained optimization problem coming from verification conditions of barrier certificates, to compute the lower bound on safety probabilities which can be compared with the given threshold. Experimental evidence is provided demonstrating the applicability of our approach on several benchmarks.

Software intelligent development has become one of the most important research trends in software engineering. In this paper, we put forward two key concepts — intelligent development environment (IntelliDE) and software knowledge graph — for the first time. IntelliDE is an ecosystem in which software big data are aggregated, mined and analyzed to provide intelligent assistance in the life cycle of software development. We present its architecture and discuss its key research issues and challenges. Software knowledge graph is a software knowledge representation and management framework, which plays an important role in IntelliDE. We study its concept and introduce some concrete details and examples to show how it could be constructed and leveraged.

Rational design on the microstructure of electromagnetic composites offers immense potential for overcoming the challenges related to the microwave absorption performance. In this study, uniform core-shell Co@C microspheres are innovatively fabricated through an in situ transformation from Co 3 O 4 @phenolic resin precursor. Carbon shells restrain the agglomeration of Co particles during high-temperature treatment, which accounts for the survival of uniform core-shell microstructure. Electromagnetic analysis reveals that Co@C microspheres show quite different electromagnetic functions as compared with pure Co derived from Co 3 O 4 microspheres. On one hand, carbon shells can effectively regulate the complex permittivity of Co@C microspheres by reducing conductivity loss and introducing polarization relaxations; on the other hand, carbon shells suppress the skin effect from cross-linked Co networks and make the isolated Co cores produce stronger magnetic loss. The microwave absorption properties are evaluated in the frequency range of 2.0–18.0 GHz, and as expected, core-shell Co@C microspheres exhibits excellent reflection loss characteristics, where strong reflection loss (−68.7 dB at 10.6 GHz), ultra-wide response bandwidth (2.7–18.0 GHz over −10 dB), and thin matched thickness (1.65 mm) can be achieved. A delta-function method and attenuation constant validate that the matched characteristic impedance and improved loss ability in Co@C microspheres account for the significant enhancement.

Preferences, the setting options provided by Android, are an essential part of Android apps. Preferences allow users to change app features and behaviors dynamically, and therefore, need to be thoroughly tested. Unfortunately, the specific preferences used in test cases are typically not explicitly specified, forcing testers to manually set options or blindly try different option combinations. To effectively test the impacts of different preference options, this paper presents PREFEST, as a preference-wise enhanced automatic testing approach, for Android apps. Given a set of test cases, PREFEST can locate the preferences that may affect the test cases with a static and dynamic combined analysis on the app under test, and execute these test cases only under necessary option combinations. The evaluation shows that PREFEST can improve 6.8% code coverage and 12.3% branch coverage and find five more real bugs compared to testing with the original test cases. The test cost is reduced by 99% for both the number of test cases and the testing time, compared to testing under pairwise combination of options.

Existing energy distribution strategies of AFL and its variants have two limitations. (1) They focus on increasing coverage but ignore the fact that some code regions are more likely to be vulnerable. (2) They randomly select mutators and deterministically specify the number to mutator, therefore lack insights regarding which granularity of mutators are more helpful at that particular stage. We improve the two limitations of AFL's fuzzing energy distribution in a principled way. We direct the fuzzer to strengthen fuzzing toward regions that have a higher probability to contain vulnerabilities based on static semantic metrics of the target program. Furthermore, granularity-aware scheduling of mutators is proposed, which dynamically assigns ratios to different mutation operators. We implemented these improvements as an extension to AFL. Large-scale experimental evaluations showed the effectiveness of each improvement and performance of integration. The proposed tool has helped us find 12 new bugs and expose three new CVEs.

Numerical code is often applied in the safety-critical, but resource-limited areas. Hence, it is crucial for it to be correct and efficient, both of which are difficult to ensure. On one hand, accumulated rounding errors in numerical programs can cause system failures. On the other hand, arbitrary/infinite-precision arithmetic, although accurate, is infeasible in practice and especially in resource-limited scenarios because it performs thousands of times slower than floating-point arithmetic. Thus, it has been a significant challenge to obtain high-precision, easy-to-maintain, and efficient numerical code. This paper introduces a novel global optimization framework to tackle this challenge. Using our framework, a developer simply writes the infinite-precision numerical program directly following the problem's mathematical requirement specification. The resulting code is correct and easy-to-maintain, but inefficient. Our framework then optimizes the program in a global fashion (i.e., considering the whole program, rather than individual expressions or statements as in prior work), the key technical difficulty this work solves. To this end, it analyzes the program's numerical value flows across different statements through a symbolic trace extraction algorithm, and generates optimized traces via stochastic algebraic transformations guided by effective rule selection. We first evaluate our technique on numerical benchmarks from the literature; results show that our global optimization achieves significantly higher worst-case accuracy than the state-of-the-art numerical optimization tool. Second, we show that our framework is also effective on benchmarks having complicated program structures, which are challenging for numerical optimization. Finally, we apply our framework on real-world code to successfully detect numerical bugs that have been confirmed by developers.

Static program analysis is widely used in various application areas to solve many practical problems. Although researchers have made significant achievements in static analysis, it is still too challenging to perform sophisticated interprocedural analysis on large-scale modern software. The underlying reason is that interprocedural analysis for large-scale modern software is highly computation-and memory-intensive, leading to poor scalability. We aim to tackle the scalability problem by proposing a novel big data solution for sophisticated static analysis. Specifically, we propose a data-parallel algorithm and a join-process-filter computation model for the CFL-reachability based interprocedural analysis and develop an efficient distributed static analysis engine in the cloud, called BigSpa. Our experiments validated that BigSpa running on a cluster scales greatly to perform precise interprocedural analyses on millions of lines of code, and runs an order of magnitude or more faster than the existing state-of-the-art analysis tools.

Many real-world bugs in large-scale systems are related to object state that is supposed to obey a specified finite state machine (FSM). They are triggered when unexpected events occur on objects in certain states, making these objects transition in a way that violates their specifications. Detecting such FSM-related bugs with static analysis is challenging, especially in distributed systems that have large codebases. This paper presents a single-machine, disk-based graph system, called Grapple, which was designed to conduct precise and scalable checking of finite-state properties for very large codebases. Grapple detects bugs through context-sensitive, path-sensitive alias and dataflow analyses, which are both formulated as dynamic transitive-closure computations and automatically parallelized by the system. We propose a novel path constraint encoding/decoding algorithm to attach a path constraint to a graph edge, allowing the graph engine to efficiently recover a path and compute its constraint during the computation. We have implemented Grapple and conducted a comprehensive evaluation over widely deployed distributed systems. Grapple reported a total of 376 warnings, of which only 17 are false positives. Our results also demonstrate the scalability of Grapple: it took between 51 minutes and 33 hours to finish all the analyses on a low-end desktop with 16G memory and 1T SSD space, while the traditional approaches ran out of memory in all cases.

Stochastic model checking is a recent extension and generalization of the classical model checking, which focuses on quantitatively checking the temporal property of a system model. PCTL* is one of the important quantitative property specification languages, which is strictly more expressive than either PCTL (probabilistic computation tree logic) or LTL (linear temporal logic) with probability bounds. At present, PCTL* stochastic model checking algorithm is very complicated, and cannot provide any relevant explanation of why a formula does or does not hold in a given model. For dealing with this problem, an intuitive and succinct approach for PCTL* stochastic model checking with evidence is put forward in this paper, which includes: presenting the game semantics for PCTL* in release-PNF (release-positive normal form), defining the PCTL* stochastic model checking game, using strategy solving in game to achieve the PCTL* stochastic model checking, and refining winning strategy as the evidence to certify stochastic model checking result. The soundness and the completeness of game-based PCTL* stochastic model checking are proved, and its complexity matches the known lower and upper bounds. The game-based PCTL* stochastic model checking algorithm is implemented in a visual prototype tool, and its feasibility is demonstrated by an illustrative example.

Transition metal carbides with good chemical stability and moderate dielectric constants are becoming popular electromagnetic (EM) absorption materials. In this work, Mo2C/Co/C composites, a ternary loss system (conductivity loss, polarization loss, and magnetic loss) for EM absorption, have been successfully fabricated by rationally regulating the growth of ZIF-67 on the surface of MoO3 nanorods and subsequent pyrolysis process. The chemical compositions of Mo2C/Co/C composites indeed play a dominant role in tailoring their EM functions. It is revealed that conductivity loss, polarization loss, and magnetic loss are together responsible for the attenuation of EM energy. Although the involvement of Mo2C nanoparticles weakens magnetic loss capability to some extent, there will be a positive reinforcement in conductivity loss through the synergistic effects among different components. In addition, Mo2C nanoparticles can further provide considerable dipole orientation polarization and interfacial polarization. Among these ternary composite, MCC-50 with 30.9% of carbon, 53.6% of Mo2C, and 15.5% of Co, exhibits the best EM absorption performance, whose reflection loss intensity and qualified response bandwidth are superior to those of most carbide-based composites in previous studies. These results suggest that the rational integration of components with different loss mechanisms will be an effective pathway to enhance EM absorption.

The last decade has seen a vast proliferation of mobile apps. To improve the reliability of such apps, various techniques have been developed to automatically generate tests for them. While such techniques have been proven to be useful in producing test suites that achieve significant levels of code coverage, there is still enormous demand for techniques that effectively generate tests to exercise more code and detect more bugs of apps. We propose in this paper the Adamant approach to automated Android app testing. Adamant utilizes models that incorporate valuable human knowledge about the behaviours of the app under consideration to guide effective test generation, and the models are encoded in an extended version of the Interaction Flow Modeling Language (IFML). In an experimental evaluation on 10 open source Android apps, Adamant generated over 130 test actions per minute, achieved around 68% code coverage, and exposed 8 real bugs, significantly outperforming other test generation tools like Monkey , AndroidRipper , and Gator in terms of code covered and bugs detected.

Reverse engineering GUI models from Android apps is important for model based techniques. We believe that the UI driven feature of Android makes it necessary to build GUI models with sufficient details in order to adequately capture the apps' behavior.In this work, we make some effort in static extraction of GUI models for Android apps and our focuses include: (i) analyzing container components including Navigation-View, Fragment and RecyclerView; (ii) extracting constraint information, especially those related to window transitions; (iii) representing the analysis result with Interaction Flow Modeling Language (IFML) to visually present GUI elements of Android apps, so as to facilitate human comprehension and manual modification of the models.

Dangling pointers have become an important class of software bugs that can lead to use-after-free and double-free vulnerabilities. So far, only a few approaches have been proposed to protect against dangling pointers, while most of them suffer from high overhead. In this paper, we propose a lightweight approach, named DangDone, to eliminate dangling pointers at compile time. Built upon the root cause of a dangling pointer, i.e., a pointer and its aliases are not nullified but the memory area they point to is deallocated, DangDone realizes the protection by inserting an intermediate pointer between the pointers (i.e., a pointer and its aliases) and the memory area they point to. Hence, nullifying the intermediate pointer will nullify the pointer and its aliases, which mitigates the vulnerabilities caused by dangling pointers. Experimental results have demonstrated that DangDone can protect target programs (i.e., the SPEC CPU benchmarks and the programs with known CVEs) with negligible runtime overhead (i.e., around 1% on average).

It is challenging to have a general solution to precisely detect arbitrary vulnerabilities. Thus security research has focused on detecting specific types of vulnerabilities. Missing checks for untrusted inputs used in security-sensitive operations are one of the major causes of various serious vulnerabilities. Efficiently detecting missing checks is essential for identifying insufficient attack protections and prognosing potential vulnerabilities. This paper proposes a systematic static approach to detect missing checks for manipulable data used in security-sensitive operations in C/C++ programs. We first locate customized security-sensitive operations with lightweight static analysis; then judge assailability of sensitive data used in security-sensitive operations via static taint analysis; finally, assess the existence and risk degree of missing checks using static analysis. We have implemented the approach into an automated and cross-platform tool, named Vanguard, on top of Clang/LLVM 3.6.0. Experimental results on open-source projects have shown its effectiveness and efficiency. Furthermore, Vanguard has led us to uncover five known vulnerabilities and two unknown bugs.

Missing check for untrusted input used in security-sensitive operations is one of the major causes of various serious vulnerabilities. Thus, efficiently detecting missing checks for realistic software is essential for identify insufficient attack protections. We propose a systematic static approach to detect missing checks in C/C++ programs. An automated and cross-platform tool named Vanguard was implemented on top of Clang/LLVM 3.6.0. And experimental results have shown its effectiveness and efficiency.

Context Unpredictability and uncertainty about future evolutions of both the system and its environment may easily compromise the behavior of the system. The subsequent software failures can have serious consequences. When dealing with open environments, run-time monitoring is one of the most promising techniques to detect software failures. Several monitoring approaches have been proposed in the last years; however, they suffer from two main limitations. First, they provide limited information to be exploited at run-time for early detecting and managing situations that most probably will lead to failures. Second, they mainly rely on logic-based specifications, whose intrinsic complexity may hamper the use of these monitoring approaches in industrial contexts. Objective In order to address these two limitations, this paper proposes a novel approach, called PREDIMO ( PREDI ctive MO nitoring). The approach starts from scenario-based specifications, automatically generates predictive monitors called MA s (Multi-valued Automata), which take into account the actual status and also the possible evolution of both system and environment in the near future, and enables the definition of precise strategies to prevent failures. More specifically, the generated monitors evaluate the specified properties and return one of the seven different values representing the degree of controllability of the system and the distance of the potential incoming failure. The translation from scenario-based specifications to MA s preserves the semantics of the starting specification. Method We use the design and creation research methodology to design an innovative approach that fills highlighted gaps of state-of-the-art approaches. The validation of the approach is performed through a large experimentation with OSGi (Open Service Gateway Initiative) applications. Results We present a novel language to specify the properties to be monitored. Then, we present a novel approach to automatically generate predictive monitors from the specified properties. Conclusion The overall approach is tool supported and a large experimentation demonstrates its feasibility and usability.

Mobile applications with complex GUIs are very popular today. However, generating test cases for these applications is often tedious professional work. On the one hand, manually designing and writing elaborate GUI scripts requires expertise. On the other hand, generating GUI scripts with record and playback techniques usually depends on repetitive work that testers need to interact with the application over and over again, because only one path is recorded in an execution. Automatic GUI testing focuses on exploring combinations of GUI events. As the number of combinations is huge, it is still necessary to introduce a test interface for testers to reduce its search space. This paper presents a sketch-guided GUI test generation approach for testing mobile applications, which provides a simple but expressive interface for testers to specify their testing purposes. Testers just need to draw a few simple strokes on the screenshots. Then our approach translates the strokes to a testing model and initiates a model-based automatic GUI testing. We evaluate our sketch-guided approach on a few real-world Android applications collected from the literature. The results show that our approach can achieve higher coverage than existing automatic GUI testing techniques with just 10-minute sketching for an application.

Interrupt-driven programs are widely deployed in safety-critical embedded systems to perform hardware and resource dependent data operation tasks. The frequent use of interrupts in these systems can cause race conditions to occur due to interactions between application tasks and interrupt handlers. Numerous program analysis and testing techniques have been proposed to detect races in multithreaded programs. Little work, however, has addressed race condition problems related to hardware interrupts. In this paper, we present SDRacer, an automated framework that can detect and validate race conditions in interrupt-driven embedded software. It uses a combination of static analysis and symbolic execution to generate input data for exercising the potential races. It then employs virtual platforms to dynamically validate these races by forcing the interrupts to occur at the potential racing points. We evaluate SDRacer on nine real-world embedded programs written in C language. The results show that SDRacer can precisely detect race conditions.

The importance of regression testing in assuring the integrity of a program after changes is well recognized. One major obstacle in practicing regression testing is in maintaining tests that become obsolete due to evolved program behavior or specification. For mobile apps, the problem of maintaining obsolete GUI test scripts for regression testing is even more pressing. Mobile apps rely heavily on the correct functioning of their GUIs to compete on the market and provide good user experiences. But on the one hand, GUI tests break easily when changes happen to the GUI, On the other hand, mobile app developers often need to fight for a tight feedback loop and are left with limited time for test maintenance. In this paper, we propose a novel approach, called ATOM, to automatically maintain GUI test scripts of mobile apps for regression testing. ATOM uses an event sequence model to abstract possible event sequences on a GUI and a delta ESM to abstract the changes made to the GUI. Given both models as input, ATOM automatically updates the test scripts written for a base version app to reflect the changes. In an experiment with 22 versions from 11 production Android apps, ATOM updated all the test scripts affected by the version change, the updated scripts achieve over 80% of the coverage by the original scripts on the base version app, all except one set of updated scripts preserve over 60% of the actions in the original test scripts.

Planar structures for halide perovskite solar cells with the high efficiencies typically use high-temperature processed TiO2 as the electron transporting layers (ETLs). Here, we demonstrate that an in-situ passivation strategy for TiO2 film through the introduction of HI during low-temperature preparation process. HI not only controls hydrolysis of TiO2 precursor but also eliminates defects and suppresses trap states in TiO2 film. Meanwhile, the double-layer architecture is constructed by coating TiO2 with SnO2 layer, the double ETLs can improve the photovoltaic performance of methylamine lead iodide (MAPbI3) perovskite solar cells. The TiO2(HI)/SnO2 ETL can effectively reduce the interfacial charge recombination and facilitate electron transfer. More importantly, the preparation of TiO2 and SnO2 are totally performed at low-temperature (150 °C) and the devices are fabricated in uncontrolled ambient conditions. Our best-performing planar perovskite cell using such a TiO2(HI)/SnO2 ETL has achieved a maximum power conversion efficiency (PCE) of 16.74%, and the devices exhibit good stability which maintaining 85% and 83% of their initial efficiency after heating at 100 °C for 22 h and under illuminating upon 1 sun irradiation for 6 h, respectively. Our results suggest a new approach for further improving the stability of PSCs fabricated in the air condition.

C programming language never performs automatic bounds checking in order to speed up execution. But bounds checking is absolutely necessary in any program. Because if a variable is out-of-bounds, some serious errors may occur during execution, such as endless loop or buffer overflows. When there are arrays used in a program, the index of an array must be within the boundary of the array. But programmers always miss the array bounds checking or do not perform a correct array bounds checking. In this paper, we perform static analysis based on taint analysis and data flow analysis to detect which arrays do not have correct array bounds checking in the program. And we implement an automatic static tool, Carraybound. And the experimental results show that Carraybound can work effectively and efficiently.

Existing CSP model checkers are incapable of verifying multiple properties concurrently in one run of a model checker, and when trying to alleviate state space explosion problem, most of reduction work are usually done after rather than before the complete state space was produced. Thus, A new CSP model checking tool named ACSPChecker was developed based on answer set programming, which is a declarative logic programming paradigm for solving combinational search problems with the feature of completely free of sequential dependencies, to verifying multiple properties concurrently in one run of a model checker. Additionally, It integrated an abstraction method, which could be used to alleviate the state space explosion before the complete state space was produced. Furthermore, a preprocessing technique of properties was proposed to improve the verification efficiency by reducing the expense spending on replicated verification of the same sub formulas. The feasibility and efficiency of ACSPChecker are illustrated by the experiments with a classic concurrency problem - dining philosophers problem.

Symbolic execution is a widely-used program analysis technique. It collects and solves path conditions to guide the program traversing. However, due to the limitation of the current constraint solvers, it is difficult to apply symbolic execution on programs with complex path conditions, like nonlinear constraints and function calls. In this paper, we propose a new symbolic execution tool MLB to handle such problem. Instead of relying on the classical constraint solving, in MLB, the feasibility problems of the path conditions are transformed into optimization problems, by minimizing some dissatisfaction degree. The optimization problems are then handled by the underlying optimization solver through machine learning guided sampling and validation. MLB is implemented on the basis of Symbolic PathFinder and encodes not only the simple linear path conditions, but also nonlinear arithmetic operations, and even black-box function calls of library methods, into symbolic path conditions. Experiment results show that MLB can achieve much better coverage on complex real-world programs.

Buffer overflow is one of the most common types of software vulnerabilities. Various static analysis and dynamic testing techniques have been proposed to detect buffer overflow vulnerabilities. With automatic tool support, static buffer overflow detection technique has been widely used in academia and industry. However, it tends to report too many false positives fundamentally due to the lack of software execution information. Currently, static warnings can only be validated by manual inspection, which significantly limits the practicality of the static analysis. In this paper, we present BovInspector, a tool framework for automatic static buffer overflow warnings inspection and validated bugs repair. Given the program source code and static buffer overflow vulnerability warnings, BovInspector first performs warning reachability analysis. Then, BovInspector executes the source code symbolically under the guidance of reachable warnings. Each reachable warning is validated and classified by checking whether all the path conditions and the buffer overflow constraints can be satisfied simultaneously. For each validated true warning, BovInspector fix it with three predefined strategies. BovInspector is complementary to prior static buffer overflow discovery schemes. Experimental results on real open source programs show that BovInspector can automatically inspect on average of 74.9% of total warnings, and false warnings account for about 25% to 100% (on average of 59.9%) of the total inspected warnings. In addition, the automatically generated patches fix all target vulnerabilities. Further information regarding the implementation and experimental results of BovInspector is available at http://bovinspectortool.github.io/project/. And a short video for demonstrating the capabilities of BovInspector is now available at https://youtu.be/IMdcksROJDg.

Buffer overflow is one of the most common types of software security vulnerabilities. Although researchers have proposed various static and dynamic techniques for buffer overflow detection, buffer overflow attacks against both legacy and newly-deployed software systems are still quite prevalent. Compared with dynamic detection techniques, static techniques are more systematic and scalable. However, there are few studies on the effectiveness of state-of-the-art static buffer overflow detection techniques. In this paper, we perform an in-depth quantitative and qualitative study on static buffer overflow detection. More specifically, we obtain both the buggy and fixed versions of 100 buffer overflow bugs from 63 real-world projects totalling 28 MLoC (Millions of Lines of Code) based on the reports in Common Vulnerabilities and Exposures (CVE). Then, quantitatively, we apply Fortify, Checkmarx, and Splint to all the buggy versions to investigate their false negatives, and also apply them to all the fixed versions to investigate their false positives. We also qualitatively investigate the causes for the false-negatives and false-positives of studied techniques to guide the design and implementation of more advanced buffer overflow detection techniques. Finally, we also categorized the patterns of manual buffer overflow repair actions to guide automated repair techniques for buffer overflow. The experiment data is available at http://bo-study.github.io/Buffer-Overflow-Cases/.

In run-time evolving systems, components may evolve while the system is being operated. Unsafe run-time changes may compromise the correct execution of the entire system. Traditional design-time verification techniques difficultly cope with run-time changes, and run-time monitoring may detect disfunctions only too late, when the failure arises. The desire would be to define advanced monitors with the ability to predict and prevent the potential errors happening in the future. In this direction, this paper proposes CASSANDRA, a new approach that by combining design-time and run-time analysis techniques, can "look ahead" in the near execution future, and predict potential failures. During run-time we on-the-fly construct a model of the future k-step global state space according to design-time specifications and the current execution state. Consequently, we can run-time check whether possible failures might happen in the future.

Multi-robot navigation control in the absence of reference trajectory is rather challenging as it is expected to ensure stability and feasibility while still offer fast computation on control decisions. The intrinsic high complexity of switched linear dynamical robots makes the problem even more challenging. In this paper, we propose a novel HMPC based method to address the navigation problem of multiple robots with switched linear dynamics. We develop a new technique to compute the reachable sets of switched linear systems and use them to enable the parallel computation of control parameters. We present theoretical results on stability, feasibility and complexity of the proposed approach, and demonstrate its empirical advance in performance against other approaches.

International audience; This paper presents an approach to construct a verified virtual prototyping framework of embedded software. The machine code executed on a simulated target architecture can be proven to provide the same results as the real hardware, and the proof is verified with a theorem prover. The method consists in proving each instruction of the instruction set independently, by proving that the execution of the C code simulating an instruction yields an identical result to that obtained by a formal executable model of the processor architecture. This formal model itself is obtained through an automated translation process from the architecture specifications. Each independent proof draws a number of lemmas from a generic lemma library and also uses the automation of inversion tactics in the theorem prover. The paper presents the proof of the ARM architecture version 6 Instruction Set Simulator of the SimSoC open source simulator, with all of the proofs being verified by the Coq proof assistant, using automated tactics to reduce manual proof development.