这篇博客将主要包含下面的内容
- 什么是CFA
- Abstracting Abstract Machine(AAM)风格的静态分析
- 使用Racket实现AAM style 0-CFA
AAM style CFA
在开发的过程中 ，相信大家都遇到过一些问题，比如能否在编译期知道一个函数的调用位置， 能不能给推测运行时的指针指向， 能不能预测一个程序可能的运行时间？ 如果上过一些计算理论的课，相信大家都会知道，想要完全精确的知道这些问题的答案是不可能的， 但是没有一种技术能够在某种程度上近似的得到这些问题的答案呢， 其实是有的，CFA （Control Flow Analysis）.
顾名思义，CFA是一种控制流分析的技术，他的目标是获取程序运行的控制流图，并在这基础获取一些信息，比如说值的传递过程。控制流图代表了程序会如何运行， 所以一个比较直接的想法就是通过一个模型去模拟运行这个程序， 在模拟运行的过程中实现某种程度的近似，这样就可以得到程序的控制流图。这里我们就可以使用Abstract Machine来完成操作语义的模拟，特别是之前提到的CEK machine的变种timestamped CESK* machine(假设我们讨论的语言是Call-by-value的)。它的操作语义模型如下所示。
time-stamped CESK* machine
CESK* machine 和CEK 的区别在于把 所有的变量和continuation都放到一个新的Store中， 在environment上只存放一个指针指向store中的值. 使用这个抽象解释器的模型的好处是：
- 在Continuation中，不存在结构化的递归， 每一个continuation 都是使用指针的方式来连到后续的continuation
- time stamp 可以用来提供函数的调用位置信息
- 避免使用meta language自己的栈
- 使用小步语义，方便证明（大步也是可以的可以看Daris的paper但是是真的是Pearl.)
在之前介绍CEK machine的时候， 不难发现，如果我们的一个精确的语义模型，对于
之类的term 是没有办法保证停机的， 或者说我们的分析是不能达到一个不动点（fixpoint）。那么应该如何进行近似才能保证我们能够得到的正确可靠（sound）的分析算法呢？ David Van Horn 和 Matt Might 提出了一种做法, 抽象抽象机（Abstracting Abstract Machine） ,（简称AAM） 在这篇Paper中 ，他们发现，如果使用一些特定的抽象解释器，比如CESK* Machine并对Strore Allocate函数和Timestamp Tick生成函数进行进行抽象，根据CESK* Machine的特点我们可以的证明
- Alloc和Tick通过Galios Connection抽象得到的抽象值域（Abstract Domain）是有限的，那么 之后得到的新的lattice总是有限高度的也就是说我们的分析总能到达一个fixpoint。也就是说 Abstract CESK* machine是decidable的。
-
Abstract CESK* machine 是sound的， 它总是能正确的反映Concrete Machine的运行，只是精度上的丢失。
Abstract CESK* Machine
具体的证明过程在这里就不详细说了。 AAM风格最显而易见的好处就是，它把CFA简化成了只需要实现 和
, 并且能保证有一个有限的Store，也许我们选择的抽象函数不够好，但是我们得到的分析结果总是sound的。
0-CFA
CFA是无法做到完全精确的， 所以根据精度的不同，CFA家族有各种变种，比如k-CFA, m-CFA , pushdown-CFA等等。 其中最常见的是k-CFA种k=0的特例，也就是0-CFA。 0-CFA是CFA家族中最简单的一种CFA，所有的值会被抽象成生成的他们的syntax form.不难发现一种精度丢失比较大的CFA , 0-CFA近似的认为所有长的一样的call都是一样的，而所有和它调用位置相关的信息都会被无视，比如下面的例子
(let* ([id (lambda (x) x)]
[foo (id 5)])
(id 3))
这里id函数被调用了两次，0-CFA就会近似的认为任意的id调用，都会返回到任意的id调用位置。在这里id函数并不知道自己会返回到具体哪一个调用位置，因为0-CFA根本就没有记录调用历史。
0-CFA精度丢失
如果我们采用AAM风格来实现0-CFA，那么首先，因为我们不需要调用位置信息，所以我们不需要time-stamp函数, 我们只需要实现
就可以了。 又因为0-CFA会把所有值都抽象成生成它的syntax form，所以我们可以直接把syntax form当成变量的地址。就这样非常简单的我们就得到了一个0-CFA！
AAM 风格0-CFA的racket实现
在David Van Horn的原文中使用的是Direct-style Lambda Calculus 来描述AAM的。Direct style在实际使用的过程中其实并不是最合适 。一般来说，编译器会把语言先编译成IR再做CFA，常见的FP中的IR 有CPS 和ANF， 再Olin Shiver最本来的k-CFA的表述中就使用的是CPS， 但是这其实是对CFA很不利的，它会导致你的结果完全没有可读性，ANF作为函数式语言的SSA是一种比较好的选择。在后面我应该会单独写一些博客来讲这个问题。。。。
所以在我的实现中将会采用针对ANF的 来实现算法。 同时，在大多数CFA 的论文中间，都只是对最简单的
进行了讨论， 然而实际上加入不同的语法特性可能并不总是一件那么trival的事情。我的实现加入了更加多Core Scheme中的语法，比如数字，布尔值，call/cc, 递归, 多参数函数。
syntax
首先需要environment和store能够支持一个地址对应多个虚拟值，因为根据之前说的0-CFA的函数return我们很容易看到，其实这个Machine是non-deterministic的，同一个变量是很可能对应多个值的。
;; ρ ∈ Env, Environments
(define (env? ρ)
(and (andmap symbol? (hash-keys ρ))
(andmap addr? (hash-values ρ))))
;; σ ∈ Sto, Store
(define (sto? σ)
(and (andmap addr? (hash-keys σ))
(andmap (lambda (vs)
(andmap (or/c kont? value?) (set->list vs)))
(hash-values σ))))
step关系和之前的CEK machine会有巨大的不同， 因为现在一个step可能会导致多个不同的状态。还有一点可以注意到的是，因为我们采用的是ANF，所以在这里面唯一的返回来自于let, 这其实大大减少了状态数量，在ANF中可以极大的简化多参数求值的问题，多参数可以在一步中被原子的完成。在实现其他的语法特性的过程中其实也有一些区别，不赘述了
;; non-deterministic Step relation: Σ → {Σ}
(define (step ς)
(displayln "hasdf")
(pretty-print ς)
(match ς
;; Handle a let: step into `e` while remembering (via the `let`
;; continuation) to go back and bind x within ρ before proceeding
;; to body and continuation k.
[`((let ([,x ,e]) ,body) ,ρ ,σ ,κₐ)
(let ([α (alloc₀ ς)])
(set `(,e ,ρ ,(store-update σ α `(let ,x ,ρ ,body ,κₐ)) ,α)))]
;; letrec, assume e is a curified recursive function do code transfer to
;; Y combinator, and Y combinator here should also in ANF style.
;; (U (λ (y) (λ (f)
;; (f (λ (x) (((y y) f) x)))))
[`((letrec ([,x ,e]) ,body) ,ρ ,σ ,κₐ)
(set `((let ([,x (((lambda (U-x) (U-x U-x))
(lambda (Y-y) (lambda (Y-f)
(Y-f (lambda (Y-x)
(let ([Y-yy (Y-y Y-y)])
(let ([Y-yyf (Y-yy f)])
(Y-yyf Y-x))))))))
,e)]) ,body) ,ρ ,σ ,κₐ))]
;; Handle `if` statement, first step into cond-expr if cond-expr is
;; boolean just return the relate side of branch, if number or lambda
;; throw type err, if var, eval it. Since the code has been ANF-converted
;; there is no complex expr in cond position
[`((if ,(? aexpr? econd) ,(? expr? tbranch) ,(? expr? fbranch)) ,ρ ,σ ,κₐ)
(set-map (aeval econd ρ σ)
(λ (econdᵥ)
(match econdᵥ
[#t `(,tbranch ,ρ ,σ ,κₐ)]
[#f `(,fbranch ,ρ ,σ ,κₐ)])))]
;; TODO: support multi arg continuation
;; call/cc, step into body and make continuation bind to x
;; apply a countinutaion, and it only take one argument
;; it will give up current and jump back to call/cc point
;; [`((,(? kont? k-ap) ,ae) ,ρ ,k)
;; `(,ae ,ρ ,k-ap)]
[`((call/cc (lambda (,x) ,body)) ,ρ ,σ ,κₐ)
(set (let ([α (alloc₀ ς)])
`(,body ,(hash-set ρ x κₐ) ,σ ,κₐ)))]
;; Returns. You should specify how to handle when an atomic
;; expression is in return position. Because this is an A-Normal
;; Form language, the only return position will be the `let`
;; continuation.
[`(,(? aexpr? ae) ,ρ ,σ ,κₐ )
(let ([vs (hash-ref σ κₐ)]
;; step into a state by a value
[step₁ (λ (v)
(match v
[`(let ,x ,ρ-prime ,e ,κₙ)
(let ([α (alloc₀ ς)])
`(,e ,(hash-set ρ-prime x α)
,(store-∪ σ α (aeval ae ρ σ)) ,κₙ))]))])
;; diverge here
(set-map vs step₁)
)]
;; Application. Each is an atomic expression. Assume that ae0 will
;; evaluate to a closure. This means that `(aeval ae0 ρ σ) will
;; evaluate to something that matches something like `(clo (lambda
;; (,xs ...) ,e-body) ,ρ-prime ,σ).
;; if we intro call/cc, (aeval ae0 ρ σ) can also be a continuation
[`((,ae0 ,aes ...) ,ρ ,σ ,κₐ)
(set-map (aeval ae0 ρ σ)
(λ (ae0ᵥ)
(match ae0ᵥ
[(? kont? k-ap)
;; (displayln ae0ᵥ)
;; continuation can only apply to one element
`(,(first aes) ,ρ ,σ ,(hash-ref ρ ae0))]
[`(clo (lambda (,xs ...) ,e-body) ,ρ-prime)
;; eval in one time
(let ([env&stos
(foldl (lambda (x ae e&s)
(match e&s
[`(,env ,sto)
(let ([α (alloc₀ ς)])
`(,(hash-set env x α)
,(store-∪ sto α (aeval ae ρ σ)))
)]))
`(,ρ-prime ,σ) xs aes)])
(match env&stos
[`(,new-ρ ,new-σ) `(,e-body ,new-ρ ,new-σ ,κₐ)]))]
[else (error "LHS value is not a closure can't apply!")]
)))]
))
算法的核心部分 alloc函数，其实这个反而是非常非常简单的，在0-CFA中
;; allocator function this is key of precision in AAM-style CFA
;; allocₖ(ς) : State → Addr
;; bellow is the allocator funtion for 0-CFA
;; in 0-CFA addrs is the syntax form of control string
(define (addr? κₐ) (expr? κₐ))
(define (alloc₀ ς)
(match ς
[`(,e ,ρ ,σ ,κₐ) e]))
CFA算法还有一个和普通的抽象解释器不一样的地方， CFA 是会到达Fixpoint的也就是说，任凭抽象解释器再怎么步进，我们的状态已经不会再增加了， 而状态的增加是单调的， 所以我们如果发现控制流图不再增加，那么就应当结束算法。
;; Is this state at a done configuration?
;; In CFA, if state in state graph doesn't increase
;; which means we have reach fixpoint, we are done
(define (done? state graph prev-graph)
(if (equal? graph prev-graph)
#t
(match state
[`(,(? aexpr?) ,ρ ,σ •) #t]
[else #f])))
接下来只要不停的step直到fixpoint就可以啦！这样就完成了0-CFA算法的实现， 相对还是比较简单的。
加上了生成DOT图的实现完整代码
还要做什么
- 我的实现其实并不完整， 我还需要bypass一些系统库函数进来, 不然加入number和boolean毫无意义。
- 0-CFA比较简单，我们可以增加k-CFA的k值来提升精度，也就是增加调用历史信息。
- 实际上大部分的CFA算法的时间复杂度和空间复杂度还是太大了， 我们需要使用store widening 和 Abstract Gabage collection来提升算法速度。
- 现有的AAM实现都是针对函数式语言的， 我正在做一个针对LLVM IR的。希望能用来实现一些逆向的工具。
网友评论