ZetZ：受 Rust 启发的 C 方言

ZetZ（或简称 ZZ），是一种受 Rust 启发的 C 方言，它能够在虚拟机编译时象征性地执行代码，从而形式化验证代码。

ZZ 针对的是那些在接近底层硬件的位置上运行的软件，但它也可用于构建跨平台、符合 ANSI-C 标准的库。实际上，ZZ 充当了 C 代码的转译器，然后将其输入到任何标准的 C 编译器中。与许多现代语言更强调安全性不同，ZZ 并不排除或限制那些被认为“不安全”的特性，例如原始指针访问。相反，它使用静态单赋值形式（ static single assignment form，SSA），在编译时通过诸如yices2或 z3之类的 SMT 定理证明器（SMT prover）来证明我们的代码是没有未定义行为（undefined behavior）的。

下面的代码片段展示了 ZZ 代码的写法：

using <stdio.h>::{printf}
export fn main() -> int {    let r = Random{        num: 42,    };    printf("your lucky number: %u\n", r.gen());    return 0;}
struct Random {    u32 num;}
fn gen(Random *self) -> u32 {    return self->num;}

为了防止任何未定义的行为泄漏到我们的代码中，ZZ 要求所有内存访问都是正确的。例如，数组索引需要使用 where 关键字告诉编译器被访问的索引是有效的，该关键字允许我们指定调用方必须满足的约束：

fn bla(int * a)    where len(a) >= 3{    a[2];}

类似地，可以使用 model 关键字指定对函数行为的约束：

fn bla(int a) -> int    model return == 2 * a{    return a * a;           //-- This would fail here}

为了做到这些，ZZ 在 C 语法上添加了许多约束，使其更适合形式化检查。例如，ZZ 强制执行 east-constness ，并通过函数类型启用函数指针。

InfoQ 采访了 ZZ 的创建者和维护者 Avid Picciani，以进一步了解更多关于 ZZ 的信息。

InfoQ：您能描述一下您的背景和目前从事的专业工作吗？

Picciani：我的背景是大众硬件领域，具体来说，我参与过诺基亚的所有 Linux 手机项目。

目前，我是devguard.io的创始人。我们提供了云下的物联网管理工具以实现数据主权。

让开发人员兴奋不已的杀手级特性是 carrier shell，它允许我们在不配置任何网络的情况下，向数百万台设备打开一个远程 shell。只需一个 ed25519 标识，我们就可以与任何物理网络背后的任何设备通信，当然也有对等加密，我们也不会看到或存储任何数据。

我们发布了大约 25 万台 Rust 设备，但是我们想要扩展到更低层次的嵌入式设备中，Rust 不能也不想将这些设备作为目标。

InfoQ：您能介绍下 ZZ 是怎么诞生的吗？

Picciani：为了向更低级别的硬件（ESP32，一个 AVR 8 位）提供我们的产品，我们需要能够实现极高存储效率和可移植性的工具。但是放弃 Rust 语言，转回 C 语言让我感到有点难过。这里的每个人都很喜欢 Rust， 而且 C 充满了陷阱。

与此同时，存在许多我们需要但在 Rust 中无法使用的 C 语言商业工具，比如用于模糊芯片的编译器和监管审批流程。

ZZ 是一个为期 6 个月研究的成果，我们努力从现在的计算机科学领域中探索编程的改进途径。具体来说，它的灵感来自于微软研究（比如 F* 和 Z3）。它只是将其转换成为一种更实用的语言。我们在 devguard 上也使用了 F*，特别是用于加密用途。同样值得一提的是 Alloy，它激发了我们基于反例（counter-example）检查的想法。

InfoQ：ZZ 的主要优势是什么？可用于什么场景？可以将其视为通用语言还是利基语言？

Picciani：虽然 Rust 有一种使编程更安全的魔法弹（只是不允许可变借入两次），但 ZZ 实际上只是 C 之上的一层。我们可以做任何我们想做的不安全的事情，只要我们另外为它编写一个形式化验证即可。这是一种非常独特的编程方式，更像是与一位数学教授进行结对编程，他不断地向外抛出极端情况，在这些情况下，我们的代码将会崩溃。

形式化验证可能会非常枯燥和冗长，因此 ZZ 并不是一种真正的通用编程语言。我们完全可以用 ZZ 编写一个 web 服务，事实上我们也这样做了，但它永远无法与 NodeJS 这样的快速开发特性相匹敌。但当我们将 alloy 直接集成到状态机生成器中时，这种情况可能会改变，这时我们可能希望尝试在 ZZ 中实现安全性至关重要的 Web 应用程序。

InfoQ：您如何看待 ZZ 目前的成熟状态？

Picciani：不管怎样，ZZ 是一个非常新的概念，它的两大功能（C 语言转换器和符号验证）仍然需要在细节上进一步充实。今天它已经可以使用，我鼓励人们尝试用它来构建东西，但是要做好面对许多编译器关键错误和重大语言变更的准备。对于商业代码，我建议大家谨慎地将 ZZ 和 Rust 一起使用，特别是 ZZ 非常适合与 C 系统代码交互。

我的公司devguard.io将在 4 月左右发布一款用于无云汽车遥测的新产品，该产品主要是在 Zephyr OS 和 Nordic NRF91 的基础上基于 ZZ 构建的，因此我们在全力投入其中。ZZ 中最大的开源代码库可能是devguard carrier中的 ZZ 分支。完成之后，我觉得 ZZ 就可以投入生产了。

要使用 ZZ，需要安装 Rust 以进行引导，并提供一个.toml 文件，Rust 包管理器 Cargo 使用该文件来编译代码。

原文链接：

ZetZ is a Formally Verified Dialect of C