ZetZ(或简称 ZZ),是一种受 Rust 启发的 C 方言,它能够在虚拟机编译时象征性地执行代码,从而形式化验证代码。
ZZ 针对的是那些在接近底层硬件的位置上运行的软件,但它也可用于构建跨平台、符合 ANSI-C 标准的库。实际上,ZZ 充当了 C 代码的转译器,然后将其输入到任何标准的 C 编译器中。与许多现代语言更强调安全性不同,ZZ 并不排除或限制那些被认为“不安全”的特性,例如原始指针访问。相反,它使用静态单赋值形式( static single assignment form,SSA),在编译时通过诸如yices2或 z3之类的 SMT 定理证明器(SMT prover)来证明我们的代码是没有未定义行为(undefined behavior)的。
下面的代码片段展示了 ZZ 代码的写法:
为了防止任何未定义的行为泄漏到我们的代码中,ZZ 要求所有内存访问都是正确的。例如,数组索引需要使用 where 关键字告诉编译器被访问的索引是有效的,该关键字允许我们指定调用方必须满足的约束:
类似地,可以使用 model 关键字指定对函数行为的约束:
为了做到这些,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
评论 1 条评论