基于模型的应用软件的静态检测方法研究

Research of Static Detection Method Based on Model

该文把静态分析技术与基于模型的演绎验证结合起来提供了一个框架,分析应用源代码,自动生成一个分析器,它能够推断关于给定程序行为的逻辑约束方面的信息。该文引入了一阶逻辑断言来描述API调用语义。这些断言构成分析器使用的模型。通过实验,该方法可被用来识别Java程序中的关于安全的逻辑错误。

This paper introduces a framework, which combines the static analysis technology and the deductive verification basedon model. It is used for analysis of application source code, automatically generating an analyzer, which can give the inferred infor-mation on the logic of a given constraints of program behavior. This paper introduces first-order logic assertions to describe seman-tics of the API calls. These assertions constitute the model used by the analyzer. Through the experiment, this method can be usedto identify the logic errors about the security in Java program.