NJU Static Analysis - Introduction
2024-04-30 11:21:13 #Static Analysis

NJU Static Analysis - Introduction

程序分析这块还处于宝宝阶段，故做下课堂笔记

感谢李老师和谭老师的开源精神~~ :)

（笔记中的截图来自于两位老师的PPT）

Why？

  • 程序可靠性

    空指针、内存泄露

  • 程序安全性

​ 检测注入攻击路径

  • 编译优化

    死代码优化、代码移动优化

  • 程序理解

    程序调用关系、类型检测

What?

Static Analysis

给定程序P，在不运行P的情况下，使用静态分析程序对其分析，判断P是否满足特性Q

Rice Theorem

=> No Perfect static analysis

Perfect Static Analysis

Sound and Complete => Perfect Static Analysis

What is Sound and Complete

  • Sound：对于程序存在的可能行为不漏报但有错报
  • Truth：既不错报也不漏报
  • Complete：漏报

image-20240320191240299

  • false negatives
  • false positive

image-20240320205907751

Userful Static Analysis

• Compromise soundness (false negatives)

• Compromise completeness (false positives)

image-20240320205957189

image-20240320205948604

Nowdays, Static Analysis’ trends:

​ Sound but not fully-precise static analysis

Necessity of Soundness

Soundness mean more bugs could be found

image-20240320210737920

Example of Soundness

1
2
3
4
if(input)
    x = 1;
else
    x = 0;

Static Analysis Results:

  1. When input is true, x = 1

    When input is false, x = 0

    => sound

  2. x = 1 or x = 0

    => sound

  3. x = 0, 1, 2, 3, 4

    => sound

  4. x = -1, 0

    => unsound

Abstraction

对于变量进行符号抽象

一个形象的例子：

image-20240320211524156

  • 定义符号之后，那么可以对运算进行相应的定义了

image-20240320211649359

sound：

image-20240320211950981

Over-approximation

Control flow (from wiki) :

control flow is the order in which individual statements, instructions or function calls of an imperative program are executed or evaluated

Control flow Statement（控制流语句）

  • 无条件分支或跳转
  • 条件分支
  • 循环判断分支
  • 子例程、协程
  • 无条件停止

程序分析中难免会碰到路径爆炸问题

我们通常采用flow merge

来完成Over-approximation

Prev
2024-04-30 11:21:13 #Static Analysis
Next