「如何实现流动式软件发布」线上课堂开课啦,快来报名参与课堂抽奖吧~ 了解详情
写点什么

ZetZ:受 Rust 启发的 C 方言

2020 年 3 月 08 日

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


2020 年 3 月 08 日 09:002086

评论 1 条评论

发布
用户头像
一个小工具?
2020 年 05 月 30 日 21:35
回复
没有更多了
发现更多内容

设计模式的主要原则

编程这件事

dapaul

架构师训练营学习总结——面向对象的设计模式【第三周】

王海

极客大学架构师训练营

SOLID设计原则(第二周+作业)

林毋梦

极客大学架构师训练营

设计原则之依赖倒置和接口隔离

dapaul

【架构】—回归本质(面向对象)

不二架构

面向对象 架构师 极客大学架构师训练营

架构师训练营第二章 总结

尔东雨田

第二周总结

阿布

架构师训练营 - Lesson Week 2

brave heart

极客大学架构师训练营

架构 0 期 -week2- 命题作业

陈俊

极客大学架构师训练营

依赖倒置及 Cache 重构设计

秤须苑

极客大学架构师训练营

架构师训练营 0 期第二周

Blink

架构师如何去进行软件设计(设计原则篇)?

阿飞

极客大学架构师训练营

第二周学习总结

安阳

week02-总结

seki

软件架构的实现设计总结

mh

极客大学架构师训练营 框架设计、设计原则、设计模式 第四课 听课总结

John(易筋)

极客时间 极客大学 极客大学架构师训练营 设计原则 框架设计

【架构课作业 - 第二周】

Nelson

极客大学架构师训练营

架构师训练营-第二周学习总结

极客大学架构师训练营

一笔钱买两次东西?——双花安全问题分析

石君

数字货币 双花攻击 数字货币安全

【Week02】框架设计

Aldaron

架构师训练营 - Task Week 2

brave heart

极客大学架构师训练营

【第二周学习总结】

黑莓

架构训练营第二章作业

mh

第二周作业

Aldaron

架构师培训第2周学习总结

Geek_165f3d

【第二周作业】

黑莓

第二周 作业

尔东雨田

架构师训练营-总结2

进击的炮灰

Mybatis-plus 之 DIP

无心水

极客大学架构师训练营

小师妹学JVM之:JDK14中JVM的性能优化

程序那些事

JVM 「Java 25周年」 小师妹 JIT JDK14

ZetZ:受Rust启发的C方言-InfoQ