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

  • 发表于:
  • 本文为 InfoQ 中文站特供稿件
  • 首发地址https://www.infoq.cn/article/oacW7eD0hjBLYaD5DbwW
  • 如有侵权,请联系 yunjia_community@tencent.com 删除。

扫码关注云+社区

领取腾讯云代金券