Page 187 - 《软件学报》2025年第8期

3610 软件学报 2025 年第 36 卷第 8 期

1 let data = 0u32; // 声明一个 u32 整数
2 let data_ref = &data as *const u32; // 将数据的地址转换为不可变原始指针
3 unsafe {// 通过原始指针访问字节
4 let first_byte = *data_ref.offset(200) as u8; // 越界的字节访问
5 println!("First byte: {}", first_byte); // 输出第 1 个字节的值
6 }
图 6 Unsafe 代码的安全隐患

除了原始指针之外, 另一个容易出现安全问题的原因是 unsafe 块中使用 FFI 调用外部函数, 尤其是在涉及指
针、内存管理或外部库函数行为不确定的情况下可能会引入不安全的操作, 如果不小心处理, 可能会导致内存泄
漏、悬空指针、数据竞争或其他未定义行为. 假设从 C 库中调用一个函数返回一个指向动态分配的内存的指针,
该函数期望调用者负责释放这块内存, 如果 Rust 代码未能正确释放内存, 或者在释放后继续使用该指针, 可能会
引发未定义行为.
为了避免上述问题, 程序员有责任确保 unsafe 代码不会表现出未定义行为. 形式化验证可以帮助开发者理解
代码的行为, 并通过验证 unsafe 代码满足特定的规范和属性以提供额外的保证, 确保其不会引入漏洞或安全风险.
此外, 尽管 unsafe 代码在总代码库中所占比例不大, 但它们往往是 Rust 程序中最复杂、最容易出错的部分. 因此,
unsafe 代码也是最迫切需要进行形式化验证的.

2.2.2 Rust 多态性
多态性是面向对象编程语言中的一个核心概念, 它允许编写的代码更加通用和灵活. Rust 语言的多态性主要
通过特质 (traits) 和泛型 (generics) 实现. Rust 中的泛型允许函数、结构体、枚举和 traits 定义可以处理不同类型
的数据, 而无需为每种类型编写单独的代码, 使代码更加通用和可复用. 泛型通过参数化类型来实现多态性, 如图 7
中 largest 函数使用了泛型 T, 使得该函数可以接受任何实现了 PartialOrd 特征的类型的切片. 这样无论是整数列
表还是字符列表, 函数都可以由同一个 largest 函数处理.

1 fn largest<T: PartialOrd>(list: &[T]) -> &T { fn main() {
2 let mut largest = &list[0]; let number_list = vec![34, 50, 25, 100, 65];
3 for item in list { let result = largest(&number_list);
4 if item > largest {largest = item;} let char_list = vec!['y', 'm', 'a', 'q'];
5 } let result = largest(&char_list);
6 largest }
7 }
图 7 Rust 中的泛型实例

Rust 的 trait 类似于其他面向对象语言 (如 Java、C#) 中的接口 (interface), 它定义了一组方法签名, 而具体的
实现则由结构体或枚举来完成. Rust 的 trait 可以在静态和动态两种方式下使用. 静态调度 (static dispatch) 是在编
译时确定实际调用的方法, 编译器在编译时会为每个具体的类型生成相应的代码, 能获得更好的性能, Rust 通过泛
型和 trait bounds 实现静态调度. 在 Java 和 C#中接口的实现通常都是通过动态调度 (dynamic dispatch) 完成的, 方
法调用是在运行时根据对象的实际类型来决定的, Rust 通过特征对象 (trait objects) 使用 dyn Trait 关键字支持动态
调度, 在运行时选择具体的实现, 从而实现接口的封装 (interface encapsulation). Rust 中的关联类型 (associated
types) 是一种在 trait 中定义类型占位符的机制, 这种占位符可以在实现 trait 时被具体类型所替换, 能简化 trait 的
使用, 使代码更加清晰和易于理解. 与泛型相比, 关联类型让 trait 实现更为简洁, 并且在某些情况下, 关联类型比泛
型更适合表达类型间的关系.
接口在 Java、C#等语言中可以支持多继承, 一个类可以实现多个接口, 这样该类就可以被当作多种类型使用,
trait 在 Rust 中也支持多重 trait 实现, Rust 允许一个类型实现多个 trait, 这类似于 Java 或 C#中实现多个接口, 但