%0 Journal Article
%T Full-automatic Detection of Memory Safety Violations for C Programs<br>一种C程序内存访问缺陷自动化检测方法研究
%A YANG Yang
%A ZHANG Huan-guo
%A WANG Hou-zhen
%A <br>杨飏
%A 张焕国
%A 王后珍
%J 计算机科学
%D 2010
%I 
%X Symbolic execution is an effective and automatic bug-finding method. But symbolic execution is limited in practice by the computation cost and path explosion. We presented a tool for full-automatic detection and generating inputs that lead to memory safety violations in C programs, including buffer overflow, buffer overrun and pointer dereference error. In order to reduce the amount of symbol variable, we used the symbol variable to track the length of buffer and C string. The use of symbolic buffer length makes it possible to compactly summarize the behavior of standard buffer manipulation functions. While resolving the problem of path explosion, we introduced the dynamic slicing methods to prune the redundant paths. It's shown by the experiments that our method presented in this paper not only is feasible but also has little cost.
%K Static analysis
%K Symbolic execution
%K Program slicing
%K Constraint solving<br>静态分析
%K 符号执行
%K 程序切片
%K 约束求解
%U http://www.alljournals.cn/get_abstract_url.aspx?pcid=5B3AB970F71A803DEACDC0559115BFCF0A068CD97DD29835&cid=8240383F08CE46C8B05036380D75B607&jid=64A12D73428C8B8DBFB978D04DFEB3C1&aid=26C8AD029B3C76026CA59363F1576328&yid=140ECF96957D60B2&vid=42425781F0B1C26E&iid=B31275AF3241DB2D&sid=7CE3F1F20DE6B307&eid=4C100B7696CE9E24&journal_id=1002-137X&journal_name=计算机科学&referenced_num=0&reference_num=13