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

创作场景

ZetZ：受 Rust 启发的 C 方言