李未教授提出了R-演算系统,它是形式理论的修正演算系统,是OPEN过程模式和GUINA过程模式的基础.R-演算在这2种过程模式中的核心作用是,当一个形式理论与事实产生矛盾时,找出矛盾的必要前提,从而获得一个协调的子理论.通过3种不同的方法细致刻画R-演算的基本概念“必要前提”,第1种方法来自R-演算,第2种方法基于极大协调子集与极小非协调子集的,最后一种方法是对于R-必要前提的归纳定义.通过比较这3种方法,指出各自的优缺点,并从第3种方法推演出一个可靠并且相对完全的系统.在比较这3种方法的同时,还细致地探讨了R-终止式的上下界以及极大协调子集的不可枚举性.其中极大协调的不可枚举性在一定程度上表明了不存在一种同时满足可靠并且完全的系统.%With the Internet advances further, people pay more and more attention to information security. Particularly, buffer overflow has become one of the best-known software security vulnerabilities. In terms of source code, software security vulnerabilities can be caused in two ways, data-copy-related and format-control-string-related function calls. This paper summarizes the common functions which are prone to risk buffer overflows, and introduces an algorithm of how to compute the length of formatted string variables when calling the formatted input/output functions. It also proposes a method of buffer overflow detection based on static code analysis. The detection method models the source code firstly by creating its syntax tree, symbol table, control flow graph and function call graph. Based on these models, the value range of variables and expressions in each program point is computed by interval calculation, and when encountering a function call, the function's summary is applied as a stand-in for the function. This method is scalable by allowing user to add functions under test in configure files. Experiments on open source project show that it would detect buffer overflow efficiently, and its output has both a lower false positive rate and a lower false negative rate than another testing tool, Klocwork K8.
展开▼
