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 so...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.展开更多
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 warning...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.展开更多
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 pot...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.展开更多
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 quan...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.展开更多
Fuzzing is known to be one of the most effective techniques to uncover security vulnerabilities of large-scale software systems.During fuzzing,it is crucial to distribute the fuzzing resource appropriately so as to ac...Fuzzing is known to be one of the most effective techniques to uncover security vulnerabilities of large-scale software systems.During fuzzing,it is crucial to distribute the fuzzing resource appropriately so as to achieve the best fuzzing performance under a limited budget.Existing distribution strategies of American Fuzzy Lop(AFL)based greybox fuzzing focus on increasing coverage blindly without considering the metrics of code regions,thus lacking the insight regarding which region is more likely to be vulnerable and deserves more fuzzing resources.We tackle the above drawback by proposing a vulnerable region-aware greybox fuzzing approach.Specifically,we distribute more fuzzing resources towards regions that are more likely to be vulnerable based on four kinds of code metrics.We implemented the approach as an extension to AFL named RegionFuzz.Large-scale experimental evaluations validate the effectiveness and efficiency of RegionFuzz-11 new bugs including three new CVEs are successfully uncovered by RegionFuzz.展开更多
文摘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.
基金This work was supported by the National Natural Science Foundation of China under Grant No.62032010partially by the Postgraduate Research and Practice Innovation Program of Jiangsu Province of China.
文摘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.
基金supported by the National Key Research and Development Program of China under Grant No. 2017YFA0700604the National Natural Science Foundation of China under Grant Nos. 61632015 and 61690204partially supported by the Collaborative Innovation Center of Novel Software Technology and Industrialization, and Nanjing University Innovation and Creative Program for Ph.D. Candidate under Grant No. 2016014.
文摘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.
基金The work was supported by the National Natural Science Foundation of China under Grant Nos. 61303022 and 61472179, the China Postdoctoral Science Foundation under Grant No. 2013M531328, the Natural Science Foundation of Shandong Province of China under Grant No. ZR2012FQ013, the Project of Shandong Province Higher Educational Science and Technology Program under Grant No. J13LN10, and the Science and Technology Program of Taian of China under Grant No. 201330629. This work was partially supported by Jiangsu Collaborative Innovation Center of Novel Software Technology and Industrialization of China.
文摘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.
基金(partially)supported by the National Key Research and Development Program of China under Grant No.2017YFA0700604the National Natural Science Foundation of China under Grant Nos.62032010 and 61802168+1 种基金the Leading-Edge Technology Program of Jiangsu Natural Science Foundation under Grant No.BK20202001the 2021 Double Entrepreneurship Big Data and Theoretical Research Project of Nanjing University.
文摘Fuzzing is known to be one of the most effective techniques to uncover security vulnerabilities of large-scale software systems.During fuzzing,it is crucial to distribute the fuzzing resource appropriately so as to achieve the best fuzzing performance under a limited budget.Existing distribution strategies of American Fuzzy Lop(AFL)based greybox fuzzing focus on increasing coverage blindly without considering the metrics of code regions,thus lacking the insight regarding which region is more likely to be vulnerable and deserves more fuzzing resources.We tackle the above drawback by proposing a vulnerable region-aware greybox fuzzing approach.Specifically,we distribute more fuzzing resources towards regions that are more likely to be vulnerable based on four kinds of code metrics.We implemented the approach as an extension to AFL named RegionFuzz.Large-scale experimental evaluations validate the effectiveness and efficiency of RegionFuzz-11 new bugs including three new CVEs are successfully uncovered by RegionFuzz.