基于文法和规则描述的程序静态检查器

  • 目前针对 Fortran 语言的静态检查需求来研发
  • 主要思想
    1. 用 SDF 描述程序语言的语法和语法树结构

      SDF 为一种类似 BNF 范式的语法描述语言, 选择这个语言是因为有现成的 Fortran 语言的描述文件. SDF 文件的有现有的 parser generator.

    2. 自动生成分析器源码，该分析器对源程序进行分析，输出 Aterm 格式的抽象语法树

      Aterm 格式是一种通用的数据交换格式, 自动生成的 Parser 把 Fortran 程序编程 ATerm 格式的树. 下面是一个 hello world 程序的 ATerm 格式的树.

           Program(
     no-comments()
   , [ MainProgram(
         ProgramStmt(no-label(), "hello", eos("\n      "))
       , initial-spec-part([], [])
       , SpecAndExecPart(
           [PrintStmt(no-label(), STAR(), comma-list(["\"Hello World!\""]), eos("\n  "))]
         )
       , no-subprogram-part()
       , EndProgramStmt(no-label(), "hello", eos("\n"))
       )
     ]
   )
    3. 将检查规则用自定义的规则描述语言描述. 规则描述语言是对 XPath 的扩展.

      XPath 是树型文件格式 XML 上的路径查询语言. 

          a                xpath:    //c[/d] 
   / \              // 表示在当前节点(根)的所有子孙节点中查找;
  c   c             / 表示在当前节点的孩子中查找 ;   
      |             [/d] 方括号中表示谓词. 选择满足这个条件的节点;  
      d             该表示:    树中所有 以 d 作为孩子的 c 节点. 结果为右边的 c
    4. 基于文法描述的检查器读入 Aterm 格式的语法树和规则描述文件，产生检测结果

Note: 上述框架即 在 AST 查询满足特定结构的 程序片段. 一般无法做多路径敏感的分析.

  • 主要问题
    1. 设计检测规则描述语言：扩展 XPath 语言.
      • 便利性, 使之方便于描述常见的检查.
      • 通用性, 描述不同语言的类型系统.
    2. 对规则描述文件的分析
      • 优化, 化简, 合并
    3. 高效分析器的实现
      • 对于多规则，构造相应的自动机, 用自动机对 AST 进行查询检测.
      • 及时报错

基于符号执行的静态检测工具

clang 静态分析器 是用来找 C, C++ 和 Objective-C 源码中 bug 的源码分析程序, 可以作为一个 独立程序运行, 也可以运行在 Xcode 中. 这个开源软件是 Clang 项目的一部分, 由 C++ 实现.

静态分析意味这个软件使用一系列算法和技术通过分析源码来自动寻找程序中的 bug. 类似于编 译器的警告, 但是能力更强, 能检查出一般需要运行程序才能找到的错误.

对于这个工具的介绍, 可以看官网上的一个视频(slides).

  • 主要思想
    • 探索程序中的所有路径, 执行 path-sensitive context-sensitive 的分析. 相比编译器能进行更深层 次的分析, 找到更多 bug, 比如, use-after-free, 内存泄漏等.
    • CSA 核心在所给程序的控制流图上做符号执行 (symbolic execution). 符号执行类似于一般的程 序执行, 但是会探索程序的所有可能执行路径, 变量的值用符号值来代替.
    • CSA 创建一个程序状态图. ExplodedGraph. 途中的节点为 ExplodedNode . 节点由 Program- Point 和 ProgramState 组成. ProgramPoint 表示在控制流图 CFG 上的位置. ProgramPoint 的 Kind 表示这个节点是在何时, 怎样加入图 (ExplodedGraph) 的. 比如 PreLoadKind, PostLoadKind. Pro- gramState 表示程序的抽象状态. 包括表达式到值的映射 Environment, 地址到值的映射 Store(符号内 存模型), 符号值的约束 GenericDataMap.
    • 在遇到 if 分支语句时, CSA 会跟踪两个分支的执行, 一个分支假定条件为真, 另一个分支假定条件 为假. CSA 在每条执行路径上收集对这些符号值的约束, 用这些约束来判断符号值的可能取值以及一 条路径是否可行. 当收集的约束无法满足时, 说明这一路径不可能到达. 便停止在这条路路上的搜索.
  • CSA 代码分为三部分
    • FrontEnd 作为与 clang 前端的接口
    • Core 核心部分. 符号, 内存模型, 约束求解.
    • Checkers. 在 Core 基础上实现的检查. (Available Checkers)
  • 主要问题
    • 悬空引用的检测（C/C++) 改进

      检查不仅与 checker 的设计有关 还受限于 Core 的能力, 比如 Core 对内存的建模(论文), Core 对循环的检查很差, 没有对位操作和浮点数建模等.

    • 文件未关闭的检测（C/C++） 改进
    • 实现一些 Checkers (potential checkers)
    • other open projects

results matching ""

    No results matching ""