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使用该文件来编译代码。
原文链接：
- 发表于:
- 本文为 InfoQ 中文站特供稿件
- 首发地址：https://www.infoq.cn/article/oacW7eD0hjBLYaD5DbwW
- 如有侵权，请联系 cloudcommunity@tencent.com 删除。
相关快讯
扫码
添加站长 进交流群
领取专属 10元无门槛券
私享最新 技术干货
腾讯云开发者
