架构组成

Frama-C 是一个用于分析 C 语言的平台。在这个平台之上,用户可以侧重不同的分析目标(数值,结构,内存等等),自己开发 C 语言分析软件,这些软件在 Frama-C 上,是作为插件的形式存在的。目前,已经有很多分析 C 语言的插件。

Frama-C架构

(图片来自Frama-C手册

在上面的架构图中,Frama-C 本身提供了内核服务,比如 lexer 分析器,抽象语法树 AST 生成器,抽象解释框架等等。Frama-C 还提供了标准库 stdlib,这个标准库扩展了 OCaml 自带的标准库。最底层的是内部内核,对于只涉及插件层面的用户来说,kernel Internal 模块就不需要了,如果要扩展被分析语言的语法,比如扩展C的特性,就需要在 kernel Internal 做改动。

性质描述语言 ACSL

Frama—C 也提供了性质描述语言 ACSL(ANSI/ISO C Specification Langage),它的设计参考了JAVA的建模语言 JML(Java Modeling Language)。ACSL能够描述很多功能性性质(functional properties)和函数 contract。(ps:一个函数的 contract 相当于对这个函数能够干什么的描述,通常有前置条件和后置条件)。ACSL描述的范围可以是低层次的,例如某个变量是一个合法的指向int类型的指针,也可以是高层次的,例如某个函数返回一个非空的链表。类似的功能描述语言,还有微软提供的用于描述并发程序的VCC,已经验证指针的Verifast。关于ACSL的更多细节,可以阅读官方给的手册

部分插件列表

nama 特性 技术
Evoled Value analysis(EVA) 数值分析,比如溢出、除0等等 抽象解释
Wp 计算最弱前置条件(weakest precondition),生成证明义务(proof obligations),然后可以输入相应的SMT中求解,比如Alt-Ergo, Z3 C程序中的性质用ACSL描述,基于 Hoare-style weakest precondition computation
Jessie 结构跟WP类似,生成VC C + ACSL + Hoare-style weakest precondition computation
Slicing 程序切片基于用户给的标准
Aoraï 验证 LTL 公式 LTL
PathCrawler 自动找到测试用例入口,以满足覆盖目标 单元测试
WP例子

下列程序中,函数 swap 的前置条件要求,参数指针 a 和 b 都应该是合法的,后置条件要求 a 和 b 的内容经过了交换。

1
2
3
4
5
6
7
8
9
10
11
12
// File swap.c:
/*@ requires \valid(a) && \valid(b);
@ ensures A: *a == \old(*b) ;
@ ensures B: *b == \old(*a) ;
@ assigns *a,*b ;
@*/
void swap(int *a,int *b) {
int tmp = *a ;
*a = *b ;
*b = tmp ;
return ;
}

通过 WP 生成证明义务,并且直接输入到 Alt-Ergo证明器中,我们直接得以下的结果。WP 生成了 9 个证明目标。

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
# frama-c -wp -wp-rte -wp-proof alt-ergo swap.c
...
[wp] Running WP plugin...
[wp] Loading driver 'share/wp.driver'
[wp] Collecting axiomatic usage
[rte] annotating function swap
[wp] 9 goals scheduled
[wp] [Alt-Ergo] Goal typed_swap_post_A : Valid
[wp] [Qed] Goal typed_swap_post_B : Valid
[wp] [Alt-Ergo] Goal typed_swap_assert_rte_mem_access : Valid
[wp] [Qed] Goal typed_swap_assert_rte_mem_access_2 : Valid
[wp] [Alt-Ergo] Goal typed_swap_assert_rte_mem_access_3 : Valid
[wp] [Qed] Goal typed_swap_assert_rte_mem_access_4 : Valid
[wp] [Qed] Goal typed_swap_assign_part1 : Valid
[wp] [Qed] Goal typed_swap_assign_part2 : Valid
[wp] [Qed] Goal typed_swap_assign_part3 : Valid
[wp] Proved goals: 9 / 9
Qed: 6
Alt-Ergo: 3
----------------------------------------------------------
Functions WP Alt-Ergo Total Success
swap 6 3 (17) 9 100%
----------------------------------------------------------

开发插件

用户可以根据自己的需要,在 Frama-C 开发插件,新插件可以注册在 Frama-C 的平台上。Frama-C 是完全用 OCaml 语言开发的,安装可以用 Opam 来安装。在安装好 Frama-C 的情况下,运行以下命令,就能看到插件列表了。开发插件可以参考手册

1
~ frama-c -plugins