7月27日，由InForSec主办、复旦大学系统软件与安全实验室、 中国科学院软件研究所可信计算与信息保障实验室、百度安全、奇安信集团、蚂蚁集团、阿里安全协办的“软件供应链安全”的学术交流会在线上成功召开。复旦大学计算机科学与技术学院谈心博士、复旦大学软件学院戴嘉润博士、清华大学（网络研究院）-奇安信联合研究中心谷雅聪、浙江大学&蚂蚁集团潘高宁博士、浙江大学计算机科学与技术学院付丽嫆博士、香港中文大学计算机科学与工程学系李卓华博在会上作了精彩的报告。本次会议由清华大学（网络研究院）-奇安信联合研究中心应凌云主持。北京大学、上海交通大学、中国科学技术大学、浙江大学、北京理工大学、四川大学、华中科技大学、信息工程大学、上海大学、西安邮电大学、中科院软件所、中科院信工所等高校和科研院所以及企业界7900余人在线参与了论坛，并通过视频会议与演讲嘉宾互动。

InForSec将对会议精彩报告进行内容回顾，本文分享的是李卓华博士的报告——《MirChecker：针对 Rust 的静态分析与漏洞检测工具》。

李卓华博士首先介绍了Rust语言的相关背景知识。Rust是一个以其安全性和高效著称的编程语言，它的所有权机制确保了每块内存都只有一个所有者，同时每个变量生命周期结束后都会自动释放内存。该机制有效地避免了一些其他语言中常见的内存泄漏的问题。

然而，尽管有这样的保护机制存在，李博士认为Rust目前依旧面临着两方面的问题。其一是有些代码逻辑是无法在编译时就进行检查的，因此在边运行边检查的过程中，就会出现类似整数溢出这样的异常。另一方面，为了使开发者实现某些特定的需求，Rust有unsafe的关键词，使用该关键词可以规避Rust的安全检查。根据统计，约有25%-30%的Rust包使用了该关键词。

因此，如何自动化发现Rust语言中的这类bug成了一个被关注的问题。为了解决这个问题，李博士团队，提出了名为MirChecker的静态分析与漏洞检测框架。

针对Rust上述的两方面问题，李博士发现第一种问题通常是源自于对于整数值的错误操作；而unsafe关键词则常常会导致Rust的所有权机制崩溃失效。因此，李博士的核心思路是使用静态分析的方法计算整数变量可能的取值范围，从而发现第一种类型的bug；另外，使用符号化执行的方法，对于所有权机制进行跟踪，从而发现第二种类型的bug。

李博士介绍说，MirChecker首先会通过cargo的包管理能力来解析和下载一个Rust软件的所有依赖。紧接着，被解析好的文件会被交给静态分析模块。

静态分析模块使用名叫apron的第三方库来计算整数的域，同时运用预先定义好的符号化执行规则计算对应的方程。该模块会对每个CFG执行fix-point算法，这个算法会不断迭代的读取每一条指令，并提取它们的信息和更新它们的状态，直到所有的状态都不再更新。

随后，上述静态分析结果会被保存下来，并交给bug检测模块。该模块会生成安全约束的公式，并使用SMT Z3求解器求解并输出包含错误类型和问题定位的最终检测结果。

在对模型效果的测试评估中，李博士团队收集了约1000个Rust包，并从其中12个包中发现了33个bug。

同时，对于运行时间和内存使用情况的测试，得出了该方法的开销处于正常范围之内，证明了该框架在实际应用中的价值。