BT

Facilitating the Spread of Knowledge and Innovation in Professional Software Development

Write for InfoQ

Topics

Choose your language

InfoQ Homepage News ZetZ is a Formally Verified Dialect of C

ZetZ is a Formally Verified Dialect of C

This item in japanese

Bookmarks

ZetZ, or ZZ for short, is a Rust-inspired C dialect that is able to formally verify your code by executing it symbolically at compile time in a virtual machine.

The use of ZZ is targeted at software that runs close to the hardware, but it can be also used to build cross-platform, ANSI-C compliant libraries. ZZ functions as a transpiler to C code, which is then fed into any standard C compiler. In contrast to how many modern languages approach safety, ZZ does not preclude or limit features that are deemed "unsafe", such as raw pointer access. Rather, it uses static single assignment form (SSA) to prove your code is undefined behaviour-free at compile time in a SMT prover such as yices2 or z3.

The following snippet shows how ZZ code looks like:

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;
}

To prevent any undefined behaviour from leaking into your code, ZZ requires all memory access to be correct. For example, indexing into an array requires you to tell the compiler the accessed index is valid using the where keyword, which allows you to specify a constraint the caller has to satisfy:

fn bla(int * a)
    where len(a) >= 3
{
    a[2];
}

Analogously, the model keyword allows you to specify a constraints on the behaviour of a function:

fn bla(int a) -> int
    model return == 2 * a
{
    return a * a;           //-- This would fail here
}

To make all of this possible, ZZ includes a number of constraints on C syntax to make it more suitable to formal proving. For example, ZZ enforces east-constness and enables function pointers through function types.

InfoQ has spoken with ZZ creator and maintainer Avid Picciani to learn more about ZZ.

InfoQ: Could you describe your background and your current professional endeavours?

Avid Picciani: My background is in large scale hardware, specifically I worked for Nokia on all of its Linux phones.

Currently, I am the founder of devguard.io. We do cloudless IoT management tools for data sovereignty.

The killer feature that gets developers excited is carrier shell, which allows you to open a remote shell to millions of devices without configuring any network in between. Just with a single ed25519 identity, you can talk to any device behind any physical network, of course peer-to-peer encrypted with us neither seeing nor storing any data.

We shipped about a quarter million devices with Rust on it, but want to expand to lower level embedded stuff that Rust cannot and does not want to target.

InfoQ: Could you tell us how ZZ was born?

Picciani: In order to offer our products for extreme low level hardware (ESP32, an AVR 8 Bit) we needed tools that enable extreme memory efficiency and portability. But coming from the rust language, transitioning back to C felt a little sad. Everyone here really loves Rust and C is full of pitfalls.

At the same time, lots of commercial tools exist for C that we need but are not available in Rust, such as compilers for obscure chips and regulatory approval processes.

ZZ is the result of six months of research into what current computer science can do to make programming better. Specifically it is inspired Microsoft research such as F* and Z3. It just transfers it to a more pragmatic language. We use F* at devguard as well, specifically for cryptography. Also Alloy is worth mentioning, which inspired the idea of counter-example based checking.

InfoQ: What are the main benefits ZZ provides and in which scenarios? Can it be considered a general-purpose language or is it more of a niche language?

Picciani: While Rust has a magic bullet for making programming safer (just don't allow mutable borrow twice), ZZ is really just a layer on top of C. You can do whatever unsafe stuff you want, as long as you also additionally write a formal proof for it. It's a very different way of programming, more like pair programming with a math professor who is constantly throwing corner cases at you under which your code will break.

Formal proofs can get very very boring and long, and as such ZZ isn't really a generic programming language. You totally can write a web service in ZZ, and we in fact do, but it will never ever compete with the quick-to-go nature of the likes of NodeJS. That may change when we integrate alloy directly into the state machine generation, at which point you probably might want to try implementing security critical web applications in ZZ.

InfoQ: How do you deem ZZ current status of maturity?

Picciani: Either way, ZZ is very new and the two big ideas–transpiler for C, and symbolic verification–still have to fleshed out in detail. It already works today and I encourage people to try and build stuff with it, but be prepared for major compiler bugs and big language changes. For commercial code I would encourage people to use ZZ sparingly side by side with Rust, specifically ZZ is good for interfacing with C system code.

My company, devguard.io will ship a new product for cloudless automotive telemetry sometime around April which is mostly built in ZZ on top of the Zephyr OS and a Nordic NRF91, so we're committed to it. The biggest open source code base in ZZ is probably the ZZ branch in devguard carrier. As soon as that is done, I feel like ZZ is ready for production.

To use ZZ, engineers will need to install Rust for bootstrapping and provide a .toml file used by Rust package manager Cargo to compile thier code.

Rate this Article

Adoption
Style

Hello stranger!

You need to Register an InfoQ account or or login to post comments. But there's so much more behind being registered.

Get the most out of the InfoQ experience.

Allowed html: a,b,br,blockquote,i,li,pre,u,ul,p

Community comments

  • Pretty cool idea

    by Cameron Purdy,

    Your message is awaiting moderation. Thank you for participating in the discussion.

    I like the pragmatic (and immediately useful) aspect of what they did with this! It isn't something that I can use, but I'll definitely keep it in mind when other people ask for suggestions in this area.

Allowed html: a,b,br,blockquote,i,li,pre,u,ul,p

Allowed html: a,b,br,blockquote,i,li,pre,u,ul,p

BT