此次分享的是发表在USENIX’22的题为《LinKRID: Vetting Imbalance Reference Counting in Linux kernel with Symbolic Execution 》的论文。
Linux使用reference counter来记录对共享kernel对象的引用数量，以跟踪其生命周期，并防止use-after-free。
但是由于refcount mechanisms不是自动的，因此Linux内核开发人员需要确保所有关于refcount的操作都按照预期执行；换句话说，refcount和相应的引用更改应该是一致的，所以很容易出现错误。
主要错误有：①创建新的reference时没有递增计数器，如果refcount能无限递增，可能导致use-after-free并触发UAF；②移除reference时没有递减计数器，可能导致memory leak。
Figure 1是Linux kernel中的一个UAF示例，这是由于错误处理路径中的重新计数错误造成的。函数join_session_keyring()中，如果找到相应的keyring就会refcount加1（第31行），但如果keyring等于当前的值（第16行），则直接返回，不会将refcount减1。可能产生refcount溢出，从而导致UAF。
Figure 1: A missing refcount decrement bug
internel reference不需要refcount计数，最常见的就是software cache中的指针，例如radix tree/double-linked list/hash map，kernel线程可以查找相应的对象（eg,by name），然后从cache的internel reference中获得一个externel reference，这种internel reference只表示对象存在，并不表示对象被使用，所以不需要refcount计数。在最后一个externel reference释放后，对应的internel reference会自动释放，例如，Figure 2 中，当mgr->kref为0时，kref_put会调用amp_mgr_destroy移除对mgr的internel reference 。internel reference 显然也违反了一致性原则，会带来误报。
Figure 2: An example of internal reference
Linux内核没有定义良好的接口来标记本地引用作用域的开始和结束。我们通过将一个全局引用的生命周期划分为四种常见类型来解决这个问题（Figure 3）。
-
Creation:分配点（kmalloc()）到local reference到global reference（func_1）；
-
Usage:从global reference到local reference到usage（func_2）；
-
Escape:从global reference到local reference到另一个global reference（func_3）；
-
Release:从global reference到local reference到移除global reference（func_4）。
Figure 3: Four types of local reference scopes
DEFINITION 1.在local references scope末尾，refcount change次数（∆refcount)不等于全局可见的reference change次数（∆#(reference) == #escaped – #released)。
LinKRID总体框架如下（Figure 4）：
-
static analysis：识别refcount堆对象（refcounted structures）和操纵refcount的API（refcount wrappers）；识别local reference scope（构造flow chains，即local reference的数据流，从reference创建到不可访问为止），使符号执行在这个范围执行。
-
symbolic analysis：采用约束符号执行，不需要初始化数据结构和环境建模，在local reference scope 中按照Definition 1进行检查。
-
bug detection：筛除internal reference带来的误报（通过总结internal reference类型）。
Figure 4: Four types of local reference scopes
实验数据统计见Table 1:
Table 1: Statistics in experiments
若有理解不当之处，还请批评指正。
原文始发于微信公众号（COMPASS Lab）：论文分享 | LinKRID：使用符号执行审查Linux内核中的不平衡引用计数
