检索结果-南通市图书馆

Tuning parallel symbolic execution engine for better performance

Frontiers of Computer Science 2018年第1期12卷 86-100页

作者： Anil Kumar KARNA Jinbo DU Haihao SHEN Hao ZHONG Jiong GONG Haibo YU Xiangning MA: Jianjun ZHAO Department of Computer Science Shanghai Jiao Tong University Shanghai 200240 China School of Software Shanghai Jiao Tong University Shanghai 200240 China Intel Asia-Pacific Research and Development Ltd. Shanghai 200240 China Department of Advanced Information Technology Kyushu University Fukuoka 819-0395 Japan

symbolic execution is widely used in many code analysis, testing, and verification tools. As symbolic execu- tion exhaustively explores all feasible paths, it is quite time consuming. To handle the problem, researchers have par- alleled existing symbolic execution tools （e.g., KLEE）. In particular, Cloud9 is a widely used paralleled symbolic exe- cution tool, and researchers have used the tool to analyze real code. However, researchers criticize that tools such as Cloud9 still cannot analyze large scale code. In this paper, we con- duct a field study on Cloud9, in which we use KLEE and Cloud9 to analyze benchmarks in C. Our results confirm the criticism. Based on the results, we identify three bottlenecks that hinder the performance of Cloud9： the communication time gap, the job transfer policy, and the cache management of the solved constraints. To handle these problems, we tune the communication time gap with better parameters, modify the job transfer policy, and implement an approach for cache management of solved constraints. We conduct two evalua- tions on our benchmarks and a real application to understand our improvements. Our results show that our tuned Cloud9 reduces the execution time significantly, both on our bench- marks and the real application. Furthermore, our evaluation results show that our tuning techniques improve the effective- ness on all the devices, and the improvement can be achievedupto five times, depending upon a tuning value of our ap- proach and the behaviour of program under test.

关键词： code analysis symbolic execution parallelizingsymbolic execution KLEE Ctoud9

来源：

维普期刊数据库评论

在线全文

维普期刊数据库

学校读者我要写书评

暂无评论

Strategies for scalable symbolic execution-driven test generation for programs

引用

Science China(Information Sciences) 2011年第9期54卷 1797-1812页

作者： KRISHNAMOORTHY Saparya HSIAO Michael S. LINGAPPAN Loganathan Intel Corporation Department of Electrical and Computer Engineering Virginia Polytechnic Institute and State University

With the advent of advanced program analysis and constraint solving techniques,several test generation tools use variants of symbolic *** techniques have been shown to be very effective in path-based test generation;however,they fail to scale to large programs due to the exponential number of paths to be *** this paper,we focus on tackling this path explosion problem and propose search strategies to achieve quick branch coverage under symbolic execution,while exploring only a fraction of paths in the *** present a reachability-guided strategy that makes use of the reachability graph of the program to explore unvisited portions of the program and a conflict-driven backtracking strategy that utilizes conflict analysis to perform nonchronological *** present experimental evidence that these strategies can significantly reduce the search space and improve the speed of test generation for programs.

关键词： test generation software testing symbolic execution path explosion conflict analysis

来源：

同方期刊数据库评论

在线全文

同方期刊数据库

学校读者我要写书评

暂无评论

Modified condition/decision coverage(MC/DC)oriented compiler optimization for symbolic execution

引用

Frontiers of Information Technology & Electronic Engineering 2020年第9期21卷 1267-1284页

作者： Wei-jiang HONG Yi-jun LIU Zhen-bang CHEN Wei DONG Ji WANG College of Computer National University of Defense TechnologyChangsha 410073China State Key Laboratory of High Performance Computing National University of Defense TechnologyChangsha 410073China

symbolic execution is an effective way of systematically exploring the search space of a program,and is often used for automatic software testing and bug *** program to be analyzed is usually compiled into a binary or an intermediate representation,on which symbolic execution is carried *** this process,compiler optimizations influence the effectiveness and efficiency of symbolic ***,to the best of our knowledge,there exists no work on compiler optimization recommendation for symbolic execution with respect to(w.r.t.)modified condition/decision coverage(MC/DC),which is an important testing coverage criterion widely used for mission-critical *** study describes our use of a state-of-the-art symbolic execution tool to carry out extensive experiments to study the impact of compiler optimizations on symbolic execution ***/*** results indicate that instruction combining(IC)optimization is the important and dominant optimization for symbolic execution ***/*** designed and implemented a support vector machine based optimization recommendation method ***(denoted as auto).The experiments on two standard benchmarks(Coreutils and NECLA)showed that auto achieves the best MC/DC on 67.47%of Coreutils programs and 78.26%of NECLA programs.

关键词： Compiler optimization Modified condition/decision coverage(MC/DC) Optimization recommendation symbolic execution

来源：

维普期刊数据库

同方期刊数据库评论

在线全文

学校读者我要写书评

暂无评论

Automatic Buffer Overflow Warning Validation

引用

Journal of Computer Science & Technology 2020年第6期35卷 1406-1427页

作者： Feng-Juan Gao Yu Wang Lin-Zhang Wang Zijiang Yang Xuan-Dong Li State Key Laboratory for Novel Software Technology Nanjing UniversityNanjing 210023China Department of Computer Science and Technology Nanjing UniversityNanjing 210023China Department of Computer Science Western Michigan UniversityKalamazoo 49008-5466U.S.A.

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.

关键词： buffer overflow static analysis warning symbolic execution automatic repair

来源：

维普期刊数据库评论

在线全文

维普期刊数据库

学校读者我要写书评

暂无评论

An empirical study on constraint optimization techniques for test generation

引用

Science China(Information Sciences) 2017年第1期60卷 69-83页

作者： Zhiyi ZHANG Zhenyu CHEN Ruizhi GAO Eric WONG Baowen XU State Key Laboratory for Novel Software Technology Nanjing University Department of Computer Science University of Texas at Dallas

Constraint solving is a frequent, but expensive operation with symbolic execution to generate tests for a program. To improve the efficiency of test generation using constraint solving, four optimization techniques are usually applied to existing constraint solvers, which are constraint independence, constraint set simplification, constraint caching, and expression rewriting. In this paper, we conducted an empirical study, using these four constraint optimization techniques in a well known test generation tool KLEE with 77 GNU Coreutils applications, to systematically investigate how these optimization techniques affect the efficiency of test generation. The experimental results show that these constraint optimization techniques as well as their combinations cannot improve the efficiency of test generation significantly for ALL-SIZED programs. Moreover, we studied the constraint optimization techniques with respect to two static metrics, lines of code(LOC) and cyclomatic complexity(CC), of programs. The experimental results show that the "constraint set simplification" technique can improve the efficiency of test generation significantly for the programs with high LOC and CC values. The"constraint caching" optimization technique can improve the efficiency of test generation significantly for the programs with low LOC and CC values. Finally, we propose four hybrid optimization strategies and practical guidelines based on different static metrics.

关键词： test generation symbolic execution constraint solving constraint optimization static metric

来源：

同方期刊数据库评论

在线全文

同方期刊数据库

学校读者我要写书评

暂无评论

An Empirical Study on Automated Test Generation Tools for Java:Effectiveness and Challenges

引用

Journal of Computer Science & Technology 2024年第3期39卷 715-736页

作者：刘相君余萍马晓星 State Key Laboratory for Novel Software Technology Nanjing UniversityNanjing 210023China Department of Computer Science and Technology Nanjing UniversityNanjing 210023China CCF ACM IEEE

Automated test generation tools enable test automation and further alleviate the low efficiency caused by writing hand-crafted test ***,existing automated tools are not mature enough to be widely used by software testing *** paper conducts an empirical study on the state-of-the-art automated tools for Java,i.e.,EvoSuite,Randoop,JDoop,JTeXpert,T3,and *** design a test workflow to facilitate the process,which can automatically run tools for test generation,collect data,and evaluate various ***,we conduct empirical analysis on these six tools and their related techniques from different aspects,i.e.,code coverage,mutation score,test suite size,readability,and real fault detection *** discuss about the benefits and drawbacks of hybrid techniques based on experimental ***,we introduce our experience in setting up and executing these tools,and summarize their usability and ***,we give some insights into automated tools in terms of test suite readability improvement,meaningful assertion generation,test suite reduction for random testing tools,and symbolic execution integration.

关键词： automated test generation search-based software testing random testing symbolic execution

来源：

维普期刊数据库评论

在线全文

维普期刊数据库

学校读者我要写书评

暂无评论

Evaluation of model checkers by verifying message passing programs

引用

Science China(Information Sciences) 2019年第10期62卷 6-30页

作者： Weijiang HONG Zhenbang CHEN Hengbiao YU Ji WANG College of Computer National University of Defense Technology State Key Laboratory of High Performance Computing National University of Defense Technology

Benchmarks and evaluation are important for the development of techniques and tools. Studies regarding evaluation of model checkers by large-scale benchmarks are few. The lack of such studies is mainly because of the language difference of existing model checkers and the requirement of intensive labor in building models. In this study, we present a large-scale benchmark for evaluating model checkers whose inputs are concurrent models. The benchmark consists of 2318 models that are generated automatically from real-world message passing interface(MPI) programs. The complexities of the models have been inspected to be well distributed and suitable for evaluating model checkers. Based on the benchmark, we have evaluated five state-of-the-art model checkers, i.e., PAT, FDR, Spin, PRISM, and NuSMV, by verifying the deadlock freedom property. The evaluation results demonstrate the ability and performance difference of these model checkers in verifying message passing programs.

关键词： model checker evaluation benchmark MPI symbolic execution

来源：

同方期刊数据库评论

在线全文

同方期刊数据库

学校读者我要写书评

暂无评论

Melton： a practical and precise memory leak detection tool for C programs

引用

Frontiers of Computer Science 2015年第1期9卷 34-54页

作者： Zhenbo XU Jian ZHANG Zhongxing XU Department of Computer Science and Technology University of Science and Technology of China Anhui 230027 China State Key Laboratory of Computer Science Institute of Software Chinese Academy of Sciences Beijing 100190 China

Memory leaks are a common type of defect that is hard to detect manually. Existing memory leak detection tools suffer from lack of precise interprocedural analysis and path-sensitivity. To address this problem, we present a static interprocedural analysis algorithm, that performs fully pathsensitive analysis and captures precise function behaviors, to detect memory leak in C programs. The proposed algorithm uses path-sensitive symbolic execution to track memory actions in different program paths guarded by path conditions. A novel analysis model called memory state transition graph （MSTG） is proposed to describe the tracking process and its results. In order to do interprocedural analysis, the proposed algorithm generates a summary for each procedure from MSTG and applies the summary at the procedure＇s call sites. A prototype tool called Melton is implemented for this procedure. Melton was applied to five open source C programs and 41 leaks were found. More than 90% of these leaks were subsequently confirmed and fixed by their maintainers. For comparison with other tools, Melton was also applied to some programs in standard performance evaluation corporation （SPEC） CPU 2000 benchmark suite and detected more leaks than the state of the art approaches.

关键词： memory leak bug finding static analysis symbolic execution

来源：

维普期刊数据库

同方期刊数据库评论

在线全文

学校读者我要写书评

暂无评论

Binary Program Vulnerability Mining Based on Neural Network

引用

Computers, Materials & Continua 2024年第2期78卷 1861-1879页

作者： Zhenhui Li Shuangping Xing Lin Yu Huiping Li Fan Zhou Guangqiang Yin Xikai Tang Zhiguo Wang School of Information and Software Engineering University of Electronic Science and Technology of ChinaChengdu611731China School of Electrical and Computer Engineering University ofWaterlooWaterlooN2L 3G1Canada

Software security analysts typically only have access to the executable program and cannot directly access the source code of the *** poses significant challenges to security *** it is crucial to identify vulnerabilities in such non-source code programs,there exists a limited set of generalized tools due to the low versatility of current vulnerability mining ***,these tools suffer from some *** terms of targeted fuzzing,the path searching for target points is not streamlined enough,and the completely random testing leads to an excessively large search ***,when it comes to code similarity analysis,there are issues with incomplete code feature extraction,which may result in information *** this paper,we propose a cross-platform and cross-architecture approach to exploit vulnerabilities using neural network obfuscation *** leveraging the Angr framework,a deobfuscation technique is introduced,along with the adoption of a VEX-IR-based intermediate language conversion *** combination allows for the unified handling of binary programs across various architectures,compilers,and compilation ***,binary programs are processed to extract multi-level spatial features using a combination of a skip-gram model with self-attention mechanism and a bidirectional Long Short-Term Memory(LSTM)***,the graph embedding network is utilized to evaluate the similarity of program *** on these similarity scores,a target function is determined,and symbolic execution is applied to solve the target *** solved content serves as the initial seed for targeted *** binary program is processed by using the de-obfuscation technique and intermediate language transformation method,and then the similarity of program functions is evaluated by using a graph embedding network,and symbolic execution is performed based on these similarity *** approach facilitates

关键词： Vulnerability mining de-obfuscation neural network graph embedding network symbolic execution

来源：

维普期刊数据库评论

在线全文

维普期刊数据库

学校读者我要写书评

暂无评论

From proof-of-concept to exploitable

引用

Cybersecurity 2019年第1期2卷 189-213页

作者： Yan Wang WeiWu Chao Zhang Xinyu Xing Xiaorui Gong Wei Zou School of Cyber Security University of Chinese Academy of SciencesBeijingChina Institute for Network Sciences and Cyberspace Tsinghua UniversityBeijingChina College of Information Sciences and Technology Pennsylvania State UniversityUniversity ParkUnited States Institute of Information Engineering Chinese Academy of SciencesBeijingChina Key Laboratory of Network Assessment Technology CASBeijingChina Beijing Key Laboratory of Network Security and Protection Technology BeijingChina

Exploitability assessment of vulnerabilities is important for both defenders and *** ultimate way to assess the exploitability is crafting a working ***,it usually takes tremendous hours and significant manual *** address this issue,automated techniques can be *** solutions usually explore in depth the crashing paths,i.e.,paths taken by proof-of-concept(PoC)inputs triggering vulnerabilities,and assess exploitability by finding exploitable states along the ***,exploitable states do not always exist in crashing ***,existing solutions heavily rely on symbolic execution and are not scalable in path exploration and exploit *** this paper,we propose a novel solution to generate exploit for userspace programs or facilitate the process of crafting a kernel UAF ***,we utilize oriented fuzzing to explore diverging paths from vulnerability *** userspace programs,we adopt a control-flow stitching solution to stitch crashing paths and diverging paths together to generate *** kernel UAF,we leverage a lightweight symbolic execution to identify,analyze and evaluate the system calls valuable and useful for exploiting *** have developed a prototype system and evaluated it on a set of 19 CTF(capture the flag)programs and 15 realworld Linux kernel UAF *** results showed it could generate exploit for most of the userspace test set,and it could also facilitate security mitigation bypassing and exploitability evaluation for kernel test set.

关键词： Exploit Vulnerability Taint analysis Fuzzing symbolic execution

来源：

维普期刊数据库

维普期刊数据库评论

在线全文

学校读者我要写书评

暂无评论

欢迎您,

建议与咨询留下您的常用邮箱和电话号码，以便我们向您反馈解决方案和替代方法

时间限定

文献类型

馆藏选择

核心期刊

语言

文献类型

帮助

文字说明：

检索规则说明：

检索范例：

分类表

所选分类

限定检索结果

文献类型

馆藏范围

日期分布

学科分类号

主题

机构

作者

语言

在线全文

在线全文

在线全文

在线全文

在线全文

在线全文

在线全文

在线全文

在线全文

在线全文

请选择保存的检索档案：

请选择收藏分类：

通借通还

欢迎您,

建议与咨询 留下您的常用邮箱和电话号码，以便我们向您反馈解决方案和替代方法

时间限定

文献类型

馆藏选择

核心期刊

语言

文献类型

帮助

文字说明：

检索规则说明：

检索范例：

分类表

所选分类

限定检索结果

文献类型

馆藏范围

日期分布

学科分类号

主题

机构

作者

语言

在线全文

在线全文

在线全文

在线全文

在线全文

在线全文

在线全文

在线全文

在线全文

在线全文

请选择保存的检索档案： 新增检索档案 确定 取消

请选择收藏分类： 新增自定义分类 确定 取消

通借通还

建议与咨询留下您的常用邮箱和电话号码，以便我们向您反馈解决方案和替代方法

请选择保存的检索档案：

请选择收藏分类：