0%

Soundiness

Soundiness是五年前的概念,学者们发现程序分析用于实际的现代语言中仍存在各种问题,这些问题是难以分析的语言特性导致的,因此提出Soundiness,说明如何处理这些难解的问题。

Hard features

Hard-to-analyze features: an aggressively conservative treatment to these features will likely make the analysis too imprecise to scale,rendering the analysis useless.

阅读全文 »

Feasible and Realizable Paths

(In)Feasible Paths

Infeasible Paths: Paths in CFG that do not correspond to actual executions.

程序在CFG中会存在不被执行到路径,这些路径会污染分析结果,给静态分析带来不利影响。

阅读全文 »

先前的分析算法虽然展示了分析细节,但是过于复杂难以实现,本课将介绍一种一种声明式语言(Datalog)以数据驱动推导的方式做指针分析和污点分析

Motivation

Imperative vs Declarative

Imperative(命令式)语言主要有Java、C/C++等,展示了详细的实现细节;

阅读全文 »

在软件安全中,最常见的漏洞有注入类漏洞(Injection)和信息泄露(Information Leak),而本节课将介绍的Information Flow 分析方法可以有效处理以上漏洞,具体来说,就是我们常用的污点分析技术。

Information Flow Security

阅读全文 »

Introduction

Problem of Context-Insensitive (C.I.)

  • 每次函数调用时,调用的上下文不一样;
  • 在不同的调用上下文里,函数内的变量会指向不同;
  • 在上下文不敏感的指针分析中,函数内的对象指向的内容是不同上下文混合起来的(如上例中 $n$ 指向 $o_1$ 和 $o_2$),而这些内容会后向传播,造成更多不准确的结果。
阅读全文 »

Motivation

CHA 只看定义类型,会得到很多实际不被调用的子类方法,如下图所示,CHA的常量分析时只能得到NAC

而指针分析会得到更精确的对象类型:

image-20200818213708639

Introduction to Pointer Analysis

A fundamental static analysis, computes which memory locations a pointer can point to.

For object-oriented programs, computes which objects a pointer (variable or field) can point to.

阅读全文 »

Iterative Algorithm

  • 对于一个含 $k$ 个节点的CFG,每个迭代算法对于每个node $n$ 更新$\mathrm{OUT}[n]$。

  • 假设迭代算法的研究对象(domain)是$V$,定义一个k元组$V^k=\left(\mathrm{OUT}\left[\mathrm{n}_{1}\right], \mathrm{OUT}\left[\mathrm{n}_{2}\right], \ldots, \mathrm{OUT}\left[\mathrm{n}_{\mathrm{k}}\right]\right)$,$V^k\in(V_1 \times V_2 \times \dots \times V_k)$,$V^k$ 即一次迭代产生的输出,每次迭代会更新$V^k$,可以将每次迭代经过transfer functions和control-flow handing的过程抽象为$F: V^k\rightarrow {V^{k}}’$

  • 当$V^k\rightarrow {V^{k}}’$时,即$X=F(X)$ ,称$F(x)$在$X$处到达了不动点,$X$为$F(x)$的不动点,

阅读全文 »

母校计算机院的李樾、谭添老师讲的课,听了第一节课就哭了,决定做一下笔记,课程网站 https://pascal-group.bitbucket.io/teaching.html。

PL知识体系

image-20200802113608162

如上图所示,主要分三大块,理论部分包含语言设计、类型系统、语义和逻辑检查;环境部分包含编译器和运行时设计等;应用部分包含程序分析、程序验证和程序生成等,本课程主要关注于应用方面的程序分析。

阅读全文 »