CCF-华为胡杨林基金形式化专项启动于2021年，今年是第4次发布，本专项主要目标是支持国内形式化方法的提升与竞争力构建，促进学术界与产业界合作、技术成果转化。本年度开放申报的课题分为两类：产业课题和开放课题。

课题背景

元数据如调试信息是编译器在生成可执行文件时附带的信息，它主要包括源代码与生成的机器代码之间的映射关系。具体内容包括源代码行号与对应机器指令的关系、变量的存储位置和作用范围以及函数的入口地址、参数和局部变量等等。这些信息对于调试器（如 GDB）来说至关重要，因为它们能够让调试器将机器码与源代码关联起来，帮助开发者定位和解决程序中的问题。

然而编译器生成的调试信息经常会不准确甚至缺失，主要包括以下几个原因：

• 优化：编译器为了提高代码的执行效率，会对代码进行各种优化（如循环展开、函数内联、常量折叠等），这些优化可能会导致源代码与生成的机器代码之间的映射关系变得复杂，甚至失效。

• 复杂控制流：复杂的控制流结构（如深层嵌套的条件语句、异常处理等）可能使得调试信息难以精确表示。

• 编译器 Bug：编译器本身的缺陷也可能导致调试信息的错误。

• 语言特性：某些高级语言特性（如 C++ 的模板、内联汇编等）可能使得调试信息生成更加困难。

这种调试信息不准会为依赖编译器中间代码或二进制中调试信息的下游工具链的使用造成巨大影响。程序分析工具依赖于准确的调试信息来理解程序的行为和结构。在静态分析工具中，不准确的调试信息会导致这些工具无法正确解析代码，从而影响分析结果的准确性。在动态分析工具（如模糊测试）中，不准确的调试信息会导致这些工具无法正确映射运行时信息到源代码，从而影响问题定位和修复以及覆盖率测量不准确，进而影响测试的有效性评估。

因此，我们希望探索一种可信的、可追溯的编译器中间代码元数据生成技术，能够可靠的将编译器中间代码或二进制的相关信息映射到源代码中，从而赋能所有下游可信测试工程技术，实现可靠的、高质量的软件分析与软件测试，提升可信工具链效能。

项目价值：

高质量的可追溯中间代码元数据将能够赋能所有依赖编译产物的测试与分析技术，提升软件测试与软件分析的可靠性与效能。

研究内容

在本课题中需要对编译器中间代码元数据调试信息生成不准的问题做深入调研，通过定位编译器元数据生成的理论限制和缺陷，探索一种生成可靠的编译器中间代码元数据的生成过程。具体而言，可以从以下两步进行探究：

• 深入研究问题中间代码元数据生成的缺陷，并打造自动化技术测试定位编译器缺陷，帮助开发人员修复编译器的元数据生成可靠性问题，从编译器角度完成可靠元数据生成。

• 通过改进优化编译器流程或利用大模型等进行后置处理，赋能使用中间代码作为输入的测试或分析工具，提高可靠性。

课题提供 

• 产业中的实际中间代码元数据缺失的脱敏实际案例（LLVM IR）

• 开源编译器中的相关问题案例

年度目标

• （必要）针对Clang编译器IR元数据生成的准确性测试数据集

• （必要）针对LLVM IR提供编译器元数据缺陷自动测试工具

• （优选）提供LLVM IR编译器元数据恢复工具，可恢复编译过程中在中间代码生成时缺失和错误的元数据，可以赋能利用中间代码的工具提取精确元数据追溯到源代码行号

• （优选）修复Clang编译器中的元数据的主要生成缺陷或提供对接恢复出的元数据工具

课题背景

为了应对日益增多的混合C与Rust代码的项目，特别是涉及跨语言调用的情况，希望构建一种C-（Unsafe）Rust跨语言场景的内存与并发缺陷分析工具。这个工具将利用静态分析技术，能够在不具体执行程序的情况下，分析混合代码的可能动态行为，从而识别和分析潜在的内存安全和并发问题。

当前已经存在一些静态分析工具，如SVF和MirChecker，它们分别支持C和Unsafe Rust代码的缺陷分析。然而，由于缺乏支持C-Rust跨语言场景的工具，希望填补这一技术空白，并开发一种新的工具来针对混合C-Rust代码进行缺陷分析，帮助开发人员及时发现和调试潜在的问题，提高代码的质量和可靠性。

项目价值：

实现全自动化、低误报与漏报、高效率的静态程序分析，扩展当前面针对C代码的静态分析能力，更好地提升C-Rust代码的自动分析效率与能力，降低分析工具的使用门槛。

研究内容

为了实现C-Rust跨语言静态缺陷分析，需要研究以下问题：

• 跨语言分析能力：工具将能够同时处理C和Rust代码，将他们统一到一个程序IR，并理解它们之间的交互与调用关系，以便全面分析可能存在的内存与并发缺陷。

• 内存安全分析：工具将检查代码中的内存操作，包括指针使用、内存分配与释放、资源管理等，以寻找可能的内存安全问题，如内存使用后释放、缓冲区溢出等。

• 并发缺陷分析：工具将分析代码中的并发访问，包括共享数据的同步与互斥、线程间通信等，以识别潜在的竞态条件、死锁、数据竞争等问题。

课题提供 

• 典型的产业Rust+C内存与并发问题场景；

• 与业务场景中代码功能相似的开源代码；

• 用于评估工具能力的benchmark。

年度目标

• （必要）先进的C+Rust静态分析技术的设计方案以及技术报告或论文，以及原型工具代码；

• （必要）能够检测四种通用并发与内存缺陷，即数据竞争，死锁，内存使用后释放，缓冲区溢出；

• （必要）与原有的纯C静态分析工具SVF比，在效率、准确度、误报率等方面有至少持平；

• （优选）与LLVM框架结合的C+Rust混合代码分析工具，交付的代码有较好的可读性以及可扩展性，如支持用户自定义新的内存与线程管理接口；

课题背景

Rust语言以其内存安全和并发编程特性闻名，通过所有权和生命周期等类型机制有效防止了悬空指针，双层释放等内存问题。然而，即便如此，Rust 代码仍然可能出现内存安全问题：

1.当前编译器类型检测不完善，使得编程通过的Rust代码并不满足所有权和生命周期等类型机制；

2.Rust的safe代码如果类型机制正确可以保障无悬空指针，双层释放等内存问题，但依然可能出现内存越界等其他内存安全问题（由panic机制动态保护）；

3.Rust的unsafe代码与c一样面临所有内存安全问题威胁；

为确保 Rust 代码的完备内存安全，开发一个高效的基于抽象解释的工具来进行静态验证变得尤为重要。传统的静态分析工具在处理 Rust 特有的所有权、生命周期以及复杂控制流和数据流时，往往面临效率和精度上的挑战。

项目价值：

• 实现向Rust的抽象解释内存安全验证工具，填补当前能力空白；

• 发展面向RUST的形式化技术，为Rust代码的可靠性提供形式化保障

研究内容

构建一个面向RUST的抽象解释内存安全验证工具，解决以下问题：

• 抽象域的选择与设计：为了实现高效的抽象解释，选择适当的抽象域至关重要。需要设计能够准确表达Rust代码特性的抽象域，以平衡分析的精度和效率。Rust的所有权和借用机制增加了抽象域设计的复杂性，需要特别考虑这些机制带来的数据流和控制流的复杂性。

• 复杂代码结构的处理：Rust代码中广泛使用的宏、泛型、迭代器等高级语言特性，使得控制流和数据流分析变得更加复杂。需要开发能够准确解析和分析这些复杂结构的技术。

• 低误报与零漏报：在保证分析效率的同时，保持低误报与零漏报是一个重大挑战。误报过多会降低开发者的信任和使用意愿，漏报则可能导致未检测到的潜在问题。需要有一种验证员可干预的方式去提高验证精度，消除验证过程中的误报。

年度目标

构建面向RUST的抽象解释内存安全验证工具， 并可以在千行级的rust代码做到以下3种验证之一：

1.检测safe的RUST代码是否满足Rust所有权和生命周期等类型机制；

2.验证Rust的safe代码是否存在内存越界等panic机制保护的通用内存安全问题；

3.验证Rust的unsafe的代码是否存在通用内存安全问题；

验证工具需要满足以下要求：

1.可以在开源代码（5k左右代码）上有效自动分析；

2.保障验证正确性（无漏报）；

3.可以人为干预分析精度，从而实现半自动精确分析（无误报）；

课题背景

基于二进制验证的常用手段是对待验二进制包进行提升（lifting），即构建待验二进制包等价的IR表示甚至高级语言表示。在完成提升之后，验证工作就可以通过IR层面或高级语言层面的工具完成。

然而，一般意义下的等价提升非常困难，涉及控制流重建等反编译领域的难题，部分工具的可靠性（提升前后程序的等价性）也完全无法得到保障，即使针对小规模程序也可能出现语义不一致的情况，这严重限制了基于提升的二进制验证的应用范围。

另一方面，在进行形式化验证时，完全的“等价性”并不是必要条件。形式化验证只需要提升后的代码能够覆盖原程序的所有行为即可（即“可靠的过近似”）。然而，针对此类需求的提升工作尚相当有限，特别是缺少对ARM指令的支持。

因此，我们希望能够探索一种面向形式化验证场景的二进制提升技术，既能保证提升结果是可靠的（行为覆盖原二进制的行为），也能广泛支持已有的验证器进行二进制验证。

项目价值：

• 使能二进制验证，填补当前能力空白；

• 对接成熟验证器、扩展现有工作流，降低技术迁移成本；

研究内容

• 结构信息重建：在二进制中，高级语言常用的概念（变量类型、结构化控制语句、函数等）并不存在，提升意味着需要通过对二进制中调用模式的分析重建数据流、控制流，从而得到可验证的高层表示。

• 提升可靠性保障：和一般的反编译不同，为了保障可靠性，形式化验证中使用的提升必须保证提升后程序的行为覆盖原程序的行为。这种保障可以通过形式化验证提升规则的可靠性、或者形式化验证提升后重编译的二进制和原二进制的功能等价性获得。

• ARM指令集二进制提升支持：除了X86指令集之外，不同版本的ARM指令集在华为应用场景中也非常常见。提升器需要支持常见的ARM指令二进制。

课题提供 

• 可公开的benchmark二进制（华为内部脱敏后的二进制，或者和华为内部的二进制相似的开源二进制）；

年度目标

一种可靠的二进制提升技术和对应的工具原型实现。提升工具需要满足：

• （必选）在小型服务器上，能够在1小时内完成十万条指令级别的二进制的提升；

• （必选）支持常用X86、ARM指令，能够覆盖提供的benchmark二进制的提升；

• （必选）提升结果可以对接常见验证器（如提升为LLVM IR或C语言子集）；

• （优选）提升规则的可靠性经过形式化验证；

课题背景

ACSL语言是一种常用的规约描述语言，主要在Frama-C验证框架中使用。合适的ACSL规约可以帮助很多Frama-C插件更好地进行程序分析和验证，在WP等演绎推理插件中，详细的ACSL规约甚至是不可或缺的。

然而，实际验证中编写ACSL规约往往需要专家进行长时间的投入，并且待验程序发生改变后ACSL规约往往也要随之改变，带来了极大的初始投入成本和后期维护成本。在待验功能复杂时，ACSL规约长度甚至可以超过原始程序长度。ACSL规约编写已经成为了WP等基于演绎推理的插件在验证应用时的一个主要障碍。

另一方面，在很多时候需要编写的ACSL规约是相对平凡的，可以通过最强后条件、符号执行等技术自动得出。自动生成此类ACSL归于可以大大减少基于Frama-C的演绎推理验证成本，对形式化验证在工业界的推广有重要意义。

项目价值：

降低基于演绎推理的Frama-C验证前期投入成本和后期维护成本，帮助演绎推理验证覆盖更多华为内部的实际代码。

研究内容

在使用WP插件进行程序验证时，需要编写的ACSL规约通常包括：

• 相关函数的前置条件、后置条件(requires、ensures)；

• 循环的循环规约(loop invariant、loop assigns、loop variant)；

• 其他辅助断言(assert、check、admit)；

其中，函数的前后置条件对应函数总结生成问题(function summary synthesis)，循环规约生成对应循环不变量生成(loop invariant synthesis)、循环框架条件生成(loop frame condition synthesis)、循环阶函数生成(loop ranking function synthesis)等问题。

需要注意的是，已有的此类工作往往专注于考虑局部问题（单个函数、循环的相关信息生成）。然而，实用的ACSL规约生成需要根据验证的上下文进行，函数的前置、后置条件和循环不变量的强度需要和实际性质验证需求匹配，这涉及到总体执行流程的分析和验证条件的适当分解。 

课题提供 

• 典型的公司内业务代码或功能相似的开源代码构成的benchmark；

年度目标

ACSL规约自动生成工具，满足：

• （必选）作为LLVM插件，或者Frama-C插件存在，为C代码自动插入可通过Frama-C验证的ACSL规约；

• （必选）生成的ACSL规约足够强，能够自动验证所有给出的benchmark用例；

• （优选）在生成的ACSL规约不合适的时候，支持专家手动调整生成设置、给出生成提示；

课题背景

大模型凭借其强大能力，在工业界逐步应用，在应用过程中使用者也发现大模型的很多问题，比如毒性回答、缺乏领域知识等。大模型的问题易发现、难定位、难修复，目前应用最广的手段就是添加问题对应的训练数据进行微调，但是微调会带来很多不可控的问题，比如遗忘已有知识、影响其他领域表现等。另外对全部参数进行微调代价也比较高。我们缺少精确修复大模型手段，也无法说明修复问题给其他模型能力带来的影响。这使得目前的大模型质量看护方法难以闭环。

项目价值：

支持对大模型进行精确低代价修复，并保障修复不会影响模型在其他方面的能力，与现有的大模型测试方法结合共同提升模型质量

研究内容

• 构建模型问题定位方法，确定在修复模型时需要调整的部分，这些部分可以是模型结构（比如注意力头）、神经元、参数、内部表示、训练数据等，要求能和修复方法结合使用

• 为大型模型开发精确的修复方法，不仅必须提高特定领域的性能，而且还必须提供数学证明，证明修复对其他模型能力影响很小。

• 基于开源模型如llama3，qwen等

• 目标数据集可以使用以下开源仇恨言论或其他问题领域的合理数据集

• Hate speech dataset from a white supremacist forum (WhiteForumHate) .

• Hate speech dataset from Twitter posts (TwitterHate) .

• Hate speech dataset from Gab posts (GabHate)

• Hate speech dataset from Reddit posts (RedditHate) .

• Hate and offensive speech from Twitter and Gab posts (TwitterGabHate) .

• 全面评测数据集可以使用chatbot arena, Mtbench等

年度目标

提供大模型问题定位及修复框架的原型工具及代码、技术报告、实验报告：

• （必选）以相同的训练数据支撑，对比简单使用全量微调或lora，新的修复方法的提升效果要相对高10%；

• （必选）框架能为修复对其他能力的影响提供可证明的理论保障，并对比原模型和修复后模型在chatbot arena, Mtbench等评测数据集上的表现，要求各项指标均符合提供的理论保障的预期；