DEV Community: Santiago Palladino

A beginner's intro to coding zero-knowledge proofs

Santiago Palladino — Thu, 09 Feb 2023 15:11:03 +0000

Zero-knowledge proofs are becoming increasingly popular, but it can be a hard space to navigate and find the resources to get started as a developer. After spending some time studying the topic, I'm compiling here what I learned in hope it helps others. Note from the title that this is a beginner's guide, as in its author (me!) being a beginner on ZKP programming, so please reach out if you find anything off in this article!

This article will cover what a zero-knowledge proof is, how it is used from a developer's perspective, and go through a few languages for writing them. It will not go through the underlying math: we'll treat ZKPs as a cryptographic black box.

What is a zero-knowledge proof?

A zero-knowledge proof (ZKP for short) is a cryptographic proof about a fact that does not reveal any info about said fact.

A classic example to introduce ZKPs is that I (the prover) can prove to you (the verifier) that I know a valid coloring for a graph without revealing it. To do it, we play a game where I color the graph using a random set of colors, then cover it, and you choose an edge at random. If my coloring was valid, then both nodes connected by that edge must have different colors. Then we repeat, with a different set of colors each time, until you are satisfied. Since I re-paint the graph before every round, you don't learn anything about the coloring, but you can verify that it was valid every time.

Another well-known example of what could be considered a ZKP is a digital signature: I can produce a proof that I hold a secret string (my private key) that corresponds to a public one (my public key) by signing a message, and that signature does not reveal any bits from my private key.

What is a zkSNARK?

SNARK stands for Succinct Non-interactive ARgument of Knowledge. The important bits here are the first two words: succinct and non-interactive.

A proof is succinct if it's, well, small. This means that, regardless of the complexity of the fact that we are proving, we can keep proofs small and quick to verify. This is what makes ZKPs attractive for building rollups: you can generate a succinct proof that all operations that occurred on the L2 chain were valid, succinct enough that you can verify it in a contract on L1. Protocols like Mina take this to the extreme with recursive proofs, which allow them to prove the validity of the entire history of the chain with a constant-size proof.

As for non-interactivity, just think how cumbersome it would be to deal with signatures if you needed the signer to be online every single time someone needed to verify it. In the examples above, the graph coloring proof was interactive, requiring an online game between the prover and the verifier. Fortunately, zkSNARKs do not have this requirement.

ZKPs flavors

Turns out that zkSNARKs are not the only kind of interesting ZKPs. There are also STARKs (pioneered by Starkware and used to power Starknet) and Bulletproofs (used in Monero). These differ in the running time for generating and verifying a proof, as well as the resulting proof size, or in the need for trusted setups (more on this in the next section). MatterLabs has a great comparison between them here.

Even within SNARKs, you'll find that there are multiple flavors. Groth16 is one of the most popular. The PLONK family, which includes TurboPLONK and UltraPLONK, can remove the need for a circuit-specific trusted setup at the expense of proof generation and verification time, or add support for new types of operations.

Furthermore, there are different elliptic curves to pick from, or different polynomial commitment schemes that can be used. Consensys Gnark provides a great explainer on SNARK proving schemes and curves here.

Usually, picking a ZKP language to work with will determine which ZK backend you end up using, though there are some like Circom or Gnark that support more than a single proving system.

Trusted setup

Some flavors of proving systems require what's called a trusted setup. A trusted setup is a one-time ceremony, run by multiple participants, which produces a set of random values that power the ZK proving system.

These ceremonies are critical because if all of its participants collude they can break the proving system. Here, breaking the proving system means being able to generate a proof for an invalid claim that gets accepted by the verifier. Fortunately, having just one honest participant does the trick: that's why you'll find calls for as many community members as possible to participate in such a ceremony.

Certain flavors, like Groth16, require a trusted setup for each circuit: this means that, for every program you code, you need to run a new ceremony. Others, like PLONK, need just one universal trusted setup that can be reused on any program built with that flavor. And others, like STARKs, don't need any trusted setup at all.

Constraints

The main thing you need to know about ZKPs internals is that the proof operates on a mathematical constraint system. In other words, prover engines do not deal with code like x := y * z, but with constraints of the form x - y * z = 0. Depending on the language you're working with and the prover backend, these may impact how you structure your code.

For instance, Circom only allows you to write quadratic expressions on your variables, whereas Halo2 lets you write polynomial constraints of any degree. As we'll see later, one of the outputs of compiling a program in a ZKP language will be the set of constraints.

This has the implication that certain operations are easier to represent in a ZKP than others: addition can be represented in a single constraint, whereas bit manipulation may require hundreds, as every bit may need to be represented as a separate variable. This is the reason why specific cryptographic primitives are typically chosen when working on ZKPs. As an example, Pedersen hashes are hash functions that can be represented in an arithmetic circuit much more efficiently than keccak, so they are frequently found in ZKPs.

Finite fields

Another important bit you need to know is that constraints operate in a finite field of a size determined by the underlying elliptic curve. What this means is that all arithmetic operations are computed modulo a certain value, meaning they will wrap-around that value. Don't worry though, this value is usually large enough. For instance, in Circom it is:

21888242871839275222246405745257275088548364400416034343698204186575808495617

This also means that, if you want to define specific thresholds for your integer variables, you'll need to add extra constraints for it. Some languages like Noir will do it for you, whereas others will require you to do it manually.

Why all the buzz?

ZKPs have drawn a lot of attention lately. The main reason is that they can be used as a means to cheaply verify any computation, effectively becoming a general-purpose cryptographic building block.

Gubsheep describes ZKPs as programmable cryptography, in the sense that you can use them to program cryptographic proofs for general problems. For instance, you could prove set membership using ring signatures which are specifically built to tackle that problem, or just coding a zkSNARK circuit for it.

In the Devcon6 panel on Zero Knowledge, there's a great point made about their power in enabling interoperability across different systems: once you have a system that can verify a ZKP, then you can verify that any other system with any computational environment behaved as expected, as long as you can express its computation as a ZKP. This is what powers zk-rollups: if you can write the rules of your chain as a ZKP, then you can push that proof to Ethereum and verify it on the EVM - even if your rollup doesn't use the EVM as an execution environment!

What does a circuit look like?

Let's now look into how all this works. The first step is to write a program in your ZK language or framework of choice, such as Circom, Halo2, or Noir. These programs are often referred to as circuits, which express constraints among your set of variables, or signals.

For example, we can build a circuit in Circom that lets us prove that we know two numbers, a and b, such that c = (a*b)^2, without revealing them:

template MultiplierSq() {
  signal input a;
  signal input b;
  signal ab;
  signal output c;
  ab <== a * b;
  c <== ab * ab;
}

Here we are defining two private input signals, an intermediate variable, and an output value. Note that, since Circom does not allow us to write anything more complex than quadratic constraints, we cannot directly write c <== (a*b)^2, that's why we need the intermediate ab signal.

Creating and verifying a proof

The workflow for using a ZKP circuit is not the same as a regular program, since we have two different agents: the prover and the verifier. And even within the prover, there are multiple steps involved to generate the proof. Let's go through them:

We first write and compile the circuit. This outputs several artifacts, such as the set of constraints defined by the circuit, and a script or binary to be used in the step below.
Depending on the SNARK flavor being used, it may be necessary to run a trusted setup ceremony to generate the proving and verifying keys, which are cryptographic material required for the proving and verifying process, as their names imply.
When interacting with our zk-app, the user enters the private and public inputs for the circuit. The first step is to "execute" the circuit as if it were a program, using the script or binary generated during compilation. This calculates the values for all intermediate and output variables, given the input. In the example above, given a = 2 and b = 3, it will calculate that ab = 6 and c = 36. This assignment of every signal to its concrete value is called a witness or trace.
Given the trace from step 3 and the proving key from step 2, the prover can now generate a zero-knowledge proof that all the constraints defined in the circuit hold, and only reveals the output value c. This proof can now be sent to the verifier.
The verifier, using the submitted proof and the verifying key, can now verify that the proof is correct for its public output. In our examples, the verifier can cryptographically check that the prover knows three values (a, b, ab) such that a * b = ab and ab * ab = c, where c = 36.

Keep in mind that the verification step is cheap, so the verifier can be run as an EVM smart contract. This allows to trustlessly verify any off-chain computation that can be expressed as a ZKP.

If you want to try out the workflow above yourself, I strongly reccomend Circom's getting started guide that will take you through the necessary steps. In Circom, compiling a circuit will output a WASM or a C++ program that computes the witness, as well as a R1CS representation that, together with the trusted setup ceremony, outputs the proving and verifying keys. Then, in order to generate the proof, you supply the calculated witness and the proving key. To verify it, just use the generated proof along with the verifying key. You can also autogenerate a Solidity contract for running the verification on-chain.

Execution vs constraints

In the workflow above, you may have noted that the circuit is used twice by the prover: first to generate the witness, and then to derive the constraints that are covered by the proof. These two runs are completely different beasts, and understanding their difference is one of the keys to understanding how ZKPs work.

Let's go back to our Circom example from before, where we had two instructions:

ab <== a * b;
c <== ab * ab;

In Circom, a fat arrow is just syntax sugar for two different instructions, assignment and constrain, so the above can be expanded to:

ab <-- a*b
ab === a*b
c <-- ab * ab
c === ab * ab

The a <-- a*b instructions means during the execution phase, assign a*b to ab, and gets ignored when compiling the constraints. On the other hand, ab === a*b means add a constraint that forces ab to be equal to a*b, which gets ignored during execution. In other words, when writing a circuit you're writing two different programs, that belong to two different programming paradigms, in a single one.

While you will usually write assignments and constraints that are equivalent, sometimes you need to split them up. A good example of this is the IsZero circuit.

The `IsZero` circuit

Writing a circuit that outputs 1 if an input signal is zero and 0 otherwise is surprisingly difficult when you are constrained (pun intended) to just quadratic expressions. If you are thinking of using an expression like x === 0, note that that will not return a boolean on whether x is zero or not, but instead it will constrain the signal x to be zero in this circuit.

Fortunately, Circom has a library of useful building blocks that includes an IsZero circuit that returns 0 or 1 depending on whether the input is zero, and looks like this:

template IsZero() {
  signal input in;
  signal output out;
  signal inv;

  inv <-- in!=0 ? 1/in : 0;
  out <-- -in*inv +1;
  out === -in*inv +1;
  in*out === 0;
}

This is a good example of decoupling execution and constraints in a circuit. Let's begin analyzing the constraints. The constraint in * out = 0 tells us that in or out is zero. If in is zero, then out = -in * inv + 1 = 1, so we're good. And if out is zero, then it follows that in * inv = 1, which means that in cannot be zero. Great!

But note that the actual value of inv never popped up in our reasoning, since we did not need it. This is valid for writing constraints, but when it comes to populating the trace, it falls short. We need to tell Circom how to calculate the value for inv in the witness generation phase: that's where the inv <-- in!=0 ? 1/in : 0 expression comes in. Cairo appropriately calls this sort of expressions hints.

Note that we're using operations much more complex than a quadratic expression here: we have a conditional, a comparison, and a division. This is because the execution phase is unrelated to the constraints, and as such, is not bound by the restrictions of generating a ZKP. So we are back to pretty much usual programming when working in the execution phase, having access to additional operators, control flow statements, or even auxiliary functions.

Underconstrained computation bugs

However, this difference between execution and constraint generation phases can open the door to a very nasty kind of bugs. Going back to the IsZero example, what would have happened if we forgot to write one of the constraints, say the in*out = 0 one?

Let's follow the workflow we know, assuming in=3 as input:

The circuit would have compiled fine, since there are no errors.
Witness generation would have followed the execution instructions, and correctly calculated the values inv=3^-1, out=0.
The prover would have generated a proof based on the witness and the public output, since the constraint out = -in*inv +1 holds.
The verifier would have accepted it as valid, trusting that the prover has a private non-zero value.

So far so good. But what happens if a malicious prover wants to convince us that they have a zero value, when they actually have in=3? Remember we don't have the in*out = 0 in this thought experiment.

The malicious user can manually craft a witness where in=3, inv=0, out=1.
Since the witness satisfies the constraint out = -in*inv +1, the prover can generate a proof for it.
The verifier happily accepts it, and believes that the user has a zero value when they actually don't.

This kind of issues, dubbed under-constrained computation, are particularly hard to catch. Any unit test that treats the circuit as a black box would never trigger them, as they use the circuit's execution logic to build the witness, which will pass the constraints. The only way to reproduce them is to manually assemble a witness with custom logic, which requires that you exactly know the attack you are looking for.

Alternatively, there are efforts for verifying the soundness of a circuit you've written with regard to the function you want to encode, such as Ecne, whcih I still have to try out.

The bottom line here is that you should be particularly careful when you write execution code separate from your constraint generation code, since it opens the door to underconstrained ZK programs.

A real-world example

Tornado Cash is a great learning resource on how to build a real-world zk-app with Circom circuits. I strongly recommend going through the 3-page-long white paper, as well as Gubsheep's breaking down Tornado Cash session from the 0xparc course, plus Porter's overview of the white paper.

The gist of Tornado, in case you are not familiar with it, is that you can deposit ETH in discrete amounts (there are notes of 0.1, 1, 10, and 100 ETH) into a contract, and later anonymously withdraw each note into other addresses. This has the effect of mixing your notes with those from other people, granting anonimity as long as there is enough usage.

How does it work?

For the sake of the explanation, we'll go through a slightly simplified version of the protocol, and follow Gubsheep's version instead of the one actually implemented.

Whenever a user wants to deposit a note, they generate a secret value s, and submit their 1 ETH note along with a hash of the secret H(s) to the contract. The contract collects all submitted secret hashes into a merkle tree, and stores its root R.

Now, when a user wants to withdraw their note, they need to prove that they have the secret that corresponds to H(s). To do this, the user submits a ZKP that shows that they know a private value s such that H(s) is in the merkle tree of root R. It is not revealed which of all the leaves of the tree is the user' s H(s), as the ZKP only public output is R, so this preserves anonimity. The merkle proof is checked by a circuit in the ZKP.

We also need a way to ensure that a user cannot withdraw the same note twice. Here is where the concept of nullifier comes in. A nullifier is a value, deterministically generated from the original secret, that is tracked to prevent double-spends.

So, in addition to proving membership to the merkle tree of root R, the ZKP also outputs a value G(s) to be used as a nullifier, where G is another hash function different to H. Then, whenever a note is withdrawn, its nullifier is added to a nullifier set in the smart contract, and the withdrawal is rejeted if it already exists. Note that G needs to be different to H, otherwise the ZKP would reveal H(s), which can be traced back to the original deposit and break anonimity.

In other words, whenever a user wants to withdraw, they submit a ZKP that states that they know a secret value that's in a merkle tree of root R, and exposes the nullifier of that secret value. Then the contract can check that the merkle root matches and the nullifier hasn't been used it.

If you went through Tornado's white paper, you'll note that the nullifier concept is where their implementation diverges from what we described here. Tornado actually uses two different secret values, called randomness r and nullifier k, and the public value they store is called the nullifier hash. Tornado also uses a single hash function (Pedersen hashes) instead of two different ones, and they compute the merkle tree leaf as H(r || k) and the nullifier hash as H(k). The important thing is that the nullifier cannot be linked back to the merkle tree leaf, and that it is deterministically generated from the secret. You can check out Tornado's full circuits in Circom here.

Languages for ZKPs

There are multiple languages and frameworks that you can choose from for writing ZK circuits, either general purpose (like Circom) or specific to a certain platform (like Cairo). I have tried out three different languages, Circom, Halo2, and Noir, and implemented the same circuit to compare them. The circuit proves that the user knows the results of a private set of rock-paper-scissors matches, such that the total score matches a public output. The score is calculated as specified in the definition of advent of code 2022 day 2, which I used for inspiration for the problem.

Your total score is the sum of your scores for each round. The score for a single round is the score for the shape you selected (1 for Rock, 2 for Paper, and 3 for Scissors) plus the score for the outcome of the round (0 if you lost, 3 if the round was a draw, and 6 if you won).

What follows is an overview of each language, my personal impression of it, and how the rock-paper-scissors circuit looks like in it. Keep in mind I'm a beginner in all of them, so there may be errors. Please reach out if you find any so I can fix this article.

Other languages and frameworks I still have to try out are Zokrates, Cairo, SnarkyJS, Gnark, and Leo. I hope to update this post as I go through them!

Circom

I found Circom to be the best language to start learning ZKPs, as suggested by CyberPorter. To me, Circom has the ideal level of abstraction for learning: not too high level that it abstracts away some of the quirks of ZKP, and not too low level that you get bogged down in annoying details. It also has been around for quite some time (modulo how new everything ZK is!), so you can find more documentation and samples, as well as the awesome Circom workshops from 0xparc. Last but not least, there is circomlib, a library of common building blocks for Circom.

Circom ships with a rust-based compiler CLI, plus an npm package for trusted setups and proof generation and verification. The benefit of having an npm package is that you can generate proofs in the browser, opening the door to building zk-apps. You can also autogenerate Solidity contracts for verifying proofs on-chain. Circom also lets you to choose your proving engine between Groth16 and PLONK.

As mentioned before, in Circom you work assembling circuits, where each circuit has a set of input, internal, and output signals. Circuits are defined as templates, which can be parameterized with values known at compile-time, which are similar to C++ function templates. Circom also has the concept of functions as a reusable building block in the execution phase.

The main challenges are Circom is understanding when you are writing constraint-generation code, and when you are writing witness-generation code, and tracking what values are known at compile-time versus only known at runtime. Many language constructs are only available for witness generation, like boolean or comparison operators, or can only depend on values known at compile-time, such as control flow statements. Also, keeping in mind the difference between constraint and witness generation times can guard you against underconstrained computation bugs.

Rock-paper-scissors in Circom

The circuits for the rock-paper-scissors problem were fun to write in Circom. Since it's not possible to write conditional expressions in constraints, you need to resort to math-based tricks. As a simple example, the first circuit, which validates the input of a play by checking that it is 0, 1, or 2, looks like this:

template AssertIsRPS() {
  signal input x;
  signal isRP <== (x-0) * (x-1);
  isRP * (x-2) === 0;
}

The code for calculating the score of a single round uses similar constructs, along with the IsEqual circuit from CircomLib:

// Returns the score for a single round, given the plays by x and y
template Round() {
  signal input x, y;
  signal output out;

  // ensure that each input is within 0,1,2
  AssertIsRPS()(x);
  AssertIsRPS()(y);

  // check if match was a draw
  signal isDraw <== IsEqual()([x, y]);

  signal diffYX <== (y+3)-x;

  // y wins if y-x = 1 mod 3
  signal yWins1 <== (diffYX-1) * (diffYX-4);
  signal yWins <== IsZero()(yWins1);

  // x wins if y-x = 2 mod 3
  signal xWins1 <== (diffYX-2) * (diffYX-5);
  signal xWins <== IsZero()(xWins1);

  // check that exactly one of xWins, yWins, isDraw is true
  // we probably can do without these constraints
  signal xOrYWins <== (xWins - 1) * (yWins - 1);
  xOrYWins * (isDraw - 1) === 0;
  xWins + yWins + isDraw === 1;

  // score is 6 if y wins, 3 if draw, 0 if x wins
  // plus 1, 2, 3 depending on the choice of RPS
  out <== yWins * 6 + isDraw * 3 + y + 1;
}

Finally, the outermost circuit loops through a parameterizable number of rounds n, and aggregates all scores. Note that a loop can be used here since it depends on n, which is a template parameter known at compile-time.

template Game(n) {
  signal input xs[n];
  signal input ys[n];
  signal scores[n];
  signal output out;

  var score = 0;
  for (var i = 0; i < n; i++) {
    scores[i] <== Round()(xs[i], ys[i]);
    score += scores[i];
  }

  out <== score;
}

Halo2

Halo2 is not a language but a Rust-based framework, maintained by the ZCash team. Halo2 is specific to PLONKish, giving you very direct control of how circuits are represented in the arithmetization. This makes Halo2 very low-level, but ideal for writing highly optimized circuits.

To me, Halo2 had the steepest learning curve by far. Not just because of having to understand how PLONKish arithmetization works to build the circuits, but mostly because I found Halo2's API quite complex and its documentation hard to find. There are also few resources for learning Halo2: the best I found were the 0xparc course which provides a few really valuable code samples, as well as the examples in the main repo. You may also want to check out awesome-halo2 for updated resources.

When starting with Halo2, keep in mind that there are two flavors of the framework out there: the vanilla one maintained by ZCash, and the fork by Ethereum's Privacy and Scaling Explorations team which uses a different polynomial commitment (KZG instead of IPA) that's more friendly for Ethereum.

PLONKish arithmetization

The key to building circuits in Halo2 is to begin by designing how the underlying PLONKish matrix will look like. In PLONKish, circuits are defined over a matrix that you directly define. This matrix is composed by multiple columns, where a column may represent a public output (called instance), a private witness value (called advice), a constant value (called fixed), a flag on whether a constraint is enabled (called selector, more on this below), or a lookup value (used for lookup tables, an advanced feature).

Once you have the matrix set up, it's time to define the polynomial constraints using gates. A gate in Halo2 defines one or more constraints to be applied over a set of cells in the matrix. Each gate is controlled via a selector column: if the selector is enabled at a row, then the constraints imposed by the gate relative to that row will be enforced.

A gate can define constraints across multiple rows. For example, here's an example of an L-shaped multiplication gate straight out of the Halo2 book:

meta.create_gate("mul", |meta| {
    // To implement multiplication, we need three advice cells and a selector
    // cell. We arrange them like so:
    //
    // | a0  | a1  | s_mul |
    // |-----|-----|-------|
    // | lhs | rhs | s_mul |
    // | out |     |       |
    //
    // Gates may refer to any relative offsets we want, but each distinct
    // offset adds a cost to the proof. The most common offsets are 0 (the
    // current row), 1 (the next row), and -1 (the previous row), for which
    // `Rotation` has specific constructors.
    let lhs = meta.query_advice(advice[0], Rotation::cur());
    let rhs = meta.query_advice(advice[1], Rotation::cur());
    let out = meta.query_advice(advice[0], Rotation::next());
    let s_mul = meta.query_selector(s_mul);

    // Finally, we return the polynomial expressions that constrain this gate.
    // For our multiplication gate, we only need a single polynomial constraint.
    //
    // The polynomial expressions returned from `create_gate` will be
    // constrained by the proving system to equal zero. Our expression
    // has the following properties:
    // - When s_mul = 0, any value is allowed in lhs, rhs, and out.
    // - When s_mul != 0, this constrains lhs * rhs = out.
    vec![s_mul * (lhs * rhs - out)]
});

In the code sample above, a0 and a1 are advice columns, and s_mul is the selector that defines whether the mul multiplication gate will be enforced. If it is, then the value for a0 in the next row will be constrained to be equal to the product of a0 and a1 on the current row.

In addition, Halo2 allows you to define equality constraints, where you require that a specific cell in your matrix must be equal to another. This is useful for "copying" values across your matrix, or for constraining a public instance cell to equal a specific private advice cell in order to expose a value.

As another example, you could define a circuit for proving the N-th Fibonacci number, where row i of the matrix has the values x[i-2], x[i-1], x[i]. This means you'd need three advice columns to begin with, let's call them a, b, c. Then, you'd constrain c to be equal to a + b in the same row using a gate, which requires adding a selector column for controlling it. And you'd have to set up equality constraints so that a and b are equal to b and c from the previous row. Last, in order to expose the N-th number as a public value, you'd need an instance column, constrained to equal the value of c at the last row.

Chips, gadgets, and regions

The main building blocks for circuits in Halo2 are gadgets and chips. Chips are the lowest level unit. A chip will typically expose a method for configuring its gates, as well as multiple methods for assigning values to its cells during synthesis (more on this phase below). You can also build chips composed out of other chips. Gadgets, on the other hand, operate at a higher level of abstraction, hiding the underlying chips' implementation details, though you can build your circuits directly out of chips and skip gadgets altogether.

To promote reusability, you'll notice that chips always operate over relative offsets. This allows multiple chips to be grouped into regions in a circuit. Once all regions and their shapes have been defined, it is the responsibility of a floor planner to arrange these regions on the matrix, so you don't need to directly define where each chip is actually placed. However, depending on how you structure your circuits, it is perfectly possible to pack everything into a single region and not delegate placement to the planner.

Halo2 Rust API

In Halo2, similar to Circom, the main thing to keep in mind is that your code will be invoked multiple times in different circumstances: whether it is to configure the matrix, generate the constraints, create a proof, or calculate a witness.

Your circuits need to implement a specific Circuit trait that defines methods that will be called throughout this lifecycle, either with concrete or unknown Values:

pub trait Circuit<F: Field> {
    type Config: Clone;
    type FloorPlanner: FloorPlanner;

    fn without_witnesses(&self) -> Self;
    fn configure(meta: &mut ConstraintSystem<F>) -> Self::Config;
    fn synthesize(
        &self, 
        config: Self::Config, 
        layouter: impl Layouter<F>
    ) -> Result<(), Error>;
}

The important bits here are configure and synthesize. The TLDR is that configure will set up the matrix shape and its gates, and synthesize will calculte the witness and populate the matrix with the corresponding values. However, synthesize may also be invoked with unknown values during other stages, so you need to always work with wrapped Values. For instance, and while it may seem anti-intuitive, polynomial constraints in gates are defined during configuration, but equality constraints are set up at synthesis.

The example in the Halo2 book has a good step by step on how to implement a simple circuit with a single chip in case you need a scaffold to follow.

Rock-paper-scissors in Halo2

The RPS implementation in Halo2 is much more verbose than in Circom, so we'll only reproduce some parts here. To begin with, the matrix is set up with the following columns:

An advice column for each of the two players, xs and ys, where the value in row i represents what move the player chose in round i.
A third advice column accum that tracks the accumulated total score, so row i contains the sum of the scores of all rounds up to i.
A public instance column, where the last cell is constrained to be equal to the value of accum, so only the total score is revealed and not the intermediate ones.
A selector for enabling the single gate that validates inputs and calculates the score of each round.

The main chip defines a custom gate that packs all constraints for each round: validating that inputs are in range, and calculating the score for the round and adding it to the accumulated total score. This chip uses the values of xs, ys, and accum in a row as "inputs", and "outputs" the new score in the accum column at the next row.

meta.create_gate("round", |meta| {
    let s = meta.query_selector(selector);

    let x = meta.query_advice(col_x, Rotation::cur());
    let y = meta.query_advice(col_y, Rotation::cur());
    let accum = meta.query_advice(col_accum, Rotation::cur());

    // We store the output in the accum column in the next row
    let out = meta.query_advice(col_accum, Rotation::next());

    // Constraints for each round
    vec![
        // out = y_wins * 6 + is_draw * 3 + y + 1 + accum
        s.clone() * (out - (y_wins.expr() * F::from(6) + is_draw.expr() * F::from(3) + y.clone() + const_val(1) + accum)),
        // x in (0,1,2)
        s.clone() * x.clone() * (x.clone() - const_val(1)) * (x.clone() - const_val(2)),
        // y in (0,1,2)
        s.clone() * y.clone() * (y.clone() - const_val(1)) * (y.clone() - const_val(2)),
    ]
});

The y_wins and is_draw above are IsZero chips defined like the following. Note that we can reuse the same selector column for all constraints, since there is no row in which we would want to enable some but disable others.

// yWins <==> (y+2-x) * (y-1-x) == 0;
let y_wins = IsZeroChip::configure(
    meta,
    |meta| meta.query_selector(selector), 
    |meta| {
        let x = meta.query_advice(col_x, Rotation::cur());
        let y = meta.query_advice(col_y, Rotation::cur());
        (y.clone() + const_val(2) - x.clone()) * (y - const_val(1) - x)
    }
);

When synthesizing the circuit, we loop over the inputs for each round, calculate the accumulated score, and assign the calculated values to our matrix. Note that, for the "execution" mode, we can directly use conditional expressions to calculate the score.

// Assign one row per round
for row in 0..N {
  let [x, y] = [xs[row], ys[row]]; 

  // Enable the selector for the round gate
  self.config.selector.enable(&mut region, row)?;

  // This is requiring us to add a constant column to the chip config just with zeros
  if row == 0 {
      region.assign_advice_from_constant(|| "zero", col_accum, 0, F::ZERO)?;
  }

  // Set x and y advice columns to the input values
  region.assign_advice(|| format!("x[{}]", row),col_x,row,|| x)?;
  region.assign_advice(|| format!("y[{}]", row),col_y,row,|| y)?;

  // Assign the is_zero chips to the same expressions defined in the gates
  // yWins <==> (y+2-x) * (y-1-x) == 0;
  let y_wins_chip = IsZeroChip::construct(y_wins.clone());
  let y_wins_value = (y + Value::known(F::from(2)) - x) * (y - Value::known(F::ONE) - x);
  let y_wins = y_wins_chip.assign(&mut region, row, y_wins_value)?;

  // isDraw <==> y-x == 0;
  let is_draw_chip = IsZeroChip::construct(is_draw.clone());
  let is_draw_value = y - x;
  let is_draw = is_draw_chip.assign(&mut region, row, is_draw_value)?;

  // Calculate the score of this round
  let round_score = y_wins.zip(is_draw).and_then(|(y_wins, is_draw)| {
      let partial_score = if y_wins { 6 } else if is_draw { 3 } else { 0 };
      Value::known(F::from(partial_score)) + y + Value::known(F::ONE)
  });

  // Assign the col_accum *in the next row* to the new score
  accum_value = accum_value + round_score;
  out_cell = region.assign_advice(
      || format!("out[{}]", row),
      col_accum,
      row + 1,
      || accum_value
  );
};

The last bit is exposing the total score as a public output of the circuit, by constraining the instance column to match the accum one in the last row of the matrix:

layouter.constrain_instance(out_cell.cell(), self.config.instance, N-1)

Noir

Noir, built by Aztec, is the newest language of the pack and is under active development. It is distributed as nargo, a rust-based CLI, and as a set of npm packages. The npm packages releases seem to lag slightly behind the crate, which has the bleeding edge features and only got its first stable release a few days ago (early February). Both the rust crate and the npm package can be used to compile Noir programs, generate and verify proofs, and create a verifier Solidity contract.

Noir is heavily inspired in Rust, as in it shares almost the same syntax. It supports integer, booleans, tuples, structs, and arrays, as well as a basic field type which represents an element in the native field of the proving backend (think an unsigned int capped to a big prime of about 254 bits), and is more performant than regular integers.

Unlike Circom, Noir does not allow you to define code used only for witness generation (aka hints). Noir supports control flow statements and operators out of the box, and converts them to equivalent constraints as needed. This helps prevent any unconstrained computation bugs, at the expense of performance. That said, you can define constraints unrelated to witness generation, using the special constrain keyword.

Rock-paper-scissors in Noir

Noir feels a bit like cheating compared to the other languages, since it abstracts away most complexities related to ZKPs, and feels like writing regular Rust code. The entirety of the program fits in 30 lines, and reads like a regular program:

global N: Field = 3;

#[builtin(arraylen)]
fn len<T>(_input : [T]) -> comptime Field {}

fn round(x: Field, y: Field) -> Field {
    constrain (x as u8) <= 2;
    constrain (y as u8) <= 2;

    let mut score = 0;
    let diffYX = (y + 3 - x);

    if x == y {
        score = 3;
    }    
    if (diffYX == 4) | (diffYX == 1) {
        score = 6;
    }

    score + y + 1
}

fn main(xs: [Field; N], ys: [Field; N]) -> pub Field {
    let mut result = 0;

    for i in 0..len(xs) {
        result = result + round(xs[i], ys[i]);
    }
    result
}

It's worth mentioning that I didn't run any analysis regarding the number of constraints generated by each language, but it is expected that Noir, given its higher abstraction level, produces a higher number of constraints, which impact proving time. Nevertheless, as the compiler matures, more optimizations should be added that get automatically incorporated to Noir-written programs.

Resources

If you got to this point and want to keep learning, here are some of the resources I used for getting up to speed with ZKPs. I encourage you to go through them if you want to learn directly from the masters!

CyberPorter produced a set of 6 classes that provide a great overview of ZKPs, including the motivation, a mapping of the space and who's working on it, a deep dive on TornadoCash, an overview of Circom, Cairo, SnarkyJS, and Noir, and a walkthrough of the math behind Groth16.
0xPARC has two full courses online, one on Circom and another on Halo2. I strongly recommend starting with the Circom one, led mostly by the great Gubsheep, the guy behind the Dark Forest game. These courses include hands-on workshops that take you step by step on how to build several circuits. If you want to take a stab at Halo2, I'd say they are a must-see, since there are not many other resoruces on it.
Vitalik has multiple blog posts on pretty much every cryptographic concept you need for understanding SNARKs and STARKs, as well as interesting uses for the tech. If you want to go deeper into the workings of ZKPs, search on his blog first.
The Scroll team, who are building a ZK-EVM, run an excellent educational blog when it comes to ZKPs. In particular, the article on proof generation provides a great step-by-step on the whole workflow involved when creating a ZKP.
Awesome lists are awesome, and Matter Labs, the team behind zkSync, keeps an awesome-zero-knowledge-proofs with links to all kind of resources.

A look into formal verification of smart contracts using Certora

Santiago Palladino — Fri, 02 Dec 2022 18:27:40 +0000

This is an overview of how smart contract formal verification works using Certora. It is definitely not an in-depth review of either Certora or formal verification techniques, of which I'm not an expert. Special thanks to Shelly Grossman and Nurit Dor from Certora for reviewing this article.

In software, we rely on automated tests for checking if our code matches our expectations. Testing helps guide development and uncover bugs, but a green test run only means that our tests haven't stumbled upon any issues for the scenario we chose. It certainly does not mean that our code is correct.

Formal verification is a more powerful method that can mathematically prove that our code adheres to a specification. As described in "Formal verification of smart contracts" on ethereum.org:

Formal verification refers to the process of evaluating the correctness of a system with respect to a formal specification. In simpler terms, formal verification allows us to check if the behavior of a system satisfies some requirements (i.e., it does what we want).

When implemented in smart contracts, formal verification can prove that a contract's business logic meets a predefined specification. Compared to other methods for assessing the correctness of contract code, such as testing, formal verification gives stronger guarantees that a smart contract is functionally correct.

Given how critical blockchain applications can be, smart contracts are fertile ground for formal verification. The deterministic and bounded execution in the EVM also make formal methods easier to apply.

Certora is one of the players in this field, offering a platform for formal verification using a proprietary spec language, Certora Verification Language or CVL. These specifications are uploaded, along with the smart contract code, to a proprietary cloud-based platform for verification. Given how resource-intensive formal proofs can be, these are not suited for running locally.

Under the hood, Certora generates a set of constraints out of decompiled EVM bytecode and the CVL specs, which are then passed through an SMT solver. But this is out of scope for this article: refer to their whitepaper for an in-depth explanation of how it works. So let's jump directly onto the formal specs.

What does a spec look like in CVL?

The main building block of CVL is a rule. Rules are structured as Hoare triples:

A precondition defines the current state of the contract
An operation is executed on the contract
A postcondition asserts properties on the resulting state

As an example, taken from Certora's tutorials (most examples in this article will be copied or adapted from it), let's say we have a Bank contract that receives and stores deposits from users. We want to verify that, after every deposit, the total funds deposited are greater than every individual user balance.

rule totalFundsAfterDeposit(env e, uint256 amount) {
  uint256 userFundsBefore = getFunds(e, e.msg.sender);
  uint256 totalBefore = getTotalFunds(e);

  require totalBefore >= userFundsBefore;

  deposit(e, amount);

  assert getTotalFunds(e) >= getFunds(e, e.msg.sender);
}

Note the require precondition before the action. Preconditions are not just used to set the stage: they are needed to restrict the space of valid states for a contract. Otherwise, the prover assumes that any state is possible when trying to prove the rule, even unreacheable ones.

The power of this spec is that no matter the initial set of balances, the amount deposited, or the user who sends the deposit, we know that this condition will hold. In a unit test, we'd only be testing this for a specific initial state, with a specific deposit from a specific user. A formal spec proves this property holds for every single input on every initial state covered by the precondition.

CVL also lets us prove that properties hold no matter what function is called. Much like we are proving our property holds for any deposit amount, we can also prove it over any function call on the contract:

rule totalFundsAfterAnyAction(env e, method f) {
  uint256 userFundsBefore = getFunds(e, e.msg.sender);
  uint256 totalBefore = getTotalFunds(e);

  require totalBefore >= userFundsBefore;

  calldataargs args;
  f(e, args);

  assert getTotalFunds(e) >= getFunds(e, e.msg.sender);
}

Note that we are checking that, given any valid initial state and any action executed, the resulting state is still valid. What we are actually doing here is checking that an invariant is preserved: a property that should always be true for a given contract. Invariants are a powerful tool when describing a system, and CVL has a native building block for expressing them:

invariant totalFundsGreaterThanAnyUser()
    forall address user. getTotalFunds() >= getFunds(user)

When presented with an invariant, the prover will use induction to check it, by verifying that:

The property holds once the contract is constructed
Assuming that the property holds (precondition), invoking any function (operation), the property still holds (postcondition)

Pushing the limits

Predicating over all possible values is a powerful primitive, but it has its limitations. For instance, we cannot perform aggregations. Following the previous example, the invariant that total funds are the sum of each individual user funds cannot be expressed in CVL.

Fortunately, CVL introduces another concept that allows us to handle these more complex expressions: ghosts. Broadly speaking, a ghost is a variable or function defined on CVL that allows collecting or injecting information into contract "executions" during verifications.

This is easier to understand with an example. To capture the invariant that total funds are the sum of each individual user funds, we can declare a ghost that "accumulates" each user deposit whenever the funds mapping variable is updated on the contract, and then compares that to the reported value:

ghost sumOfAllFunds() returns uint256{
  init_state axiom sumOfAllFunds() == 0;
}

hook Sstore funds[KEY address user] uint256 newBalance (uint256 oldBalance) STORAGE {
  havoc sumOfAllFunds assuming sumOfAllFunds@new() == sumOfAllFunds@old() + newBalance - oldBalance;
}

The snippet above is declaring a function sumOfAllFunds that returns a number, with an initial state of zero, and gets updated whenever there's a write to storage at the funds mapping, using both the old and new values of the sum and the entry in the mapping. We can now write an invariant that uses this ghost function and matches it to the returned value from the contract:

invariant totalFunds_GE_to_sum_of_all_funds()
  getTotalFunds() >= sumOfAllFunds()

In the snippet above, getTotalFunds is a call to the contract, which is compared to the ghost sumOfAllFunds value that we hold in our spec.

Hooks can also be defined on reads, not just writes. This lets us inject preconditions upon every value that is read out of storage, which can be used to further narrow down the state of the contract that we are verifying.

Hooks are an interesting tool for enhancing the expresiveness of proofs, but they come at a disadvantage. While rules and invariants are predicated on the external interface of the contract, hooks bind a spec to implementation details. This means a spec that is valid for an implementation may not work on a different one even if they have the same interface.

Loops and unrolls

Loops are particularly tricky when we have to prove the correctness of an algorithm. The Hoare approach is to devise a loop invariant, a property that holds across each execution of the loop, and that can be used to prove that the loop finishes and that yields a particular end state.

However, coming up with a loop invariant is not easy, and it's much harder to do in an automated way. Therefore, the Certora prover works by unrolling loops a configurable number of times. This means that loops get converted into N copies of the body of the loop, and treated as regular non-iterative code.

Since unrolling a loop a fixed number of times can hide bugs, by default the prover will alert if the loop would have run more times than it was unrolled. But since this is usually the case, the prover is typically run in optimistic-loop mode, which removes these alerts - at the cost of potentially hiding bugs.

Dealing with multiple contracts

A protocol is rarely composed of a single contract. Even though CVL seems to be geared towards testing individual contract properties, it also has tools for managing multiple contracts.

The simplest option is linking one contract to another. When running the prover, we can tell it that a field in a contract refers to an instance of another known contract. And CVL lets us refer to all registered contracts when writing our rules.

In this example from Certora's documentation, we are indicating that the asset field in the Pool contract refers to an instance of the ERC20 contract:

import "../ERC20.sol";

contract Pool {
  ERC20 asset;
}

$ certoraRun contracts/Pool.sol contracts/ERC20.sol --link Pool:asset=ERC20 ...

In case we have multiple implementations for a given contract, we can register them all and have the prover try every known implementation that satisfies the required interface. In this example, registering the ERC20 interface methods with the DISPATCHER keyword instructs the prover to try every ERC20 implementation we have in stock.

methods {
  totalSupply()                         returns (uint256) => DISPATCHER(true)
  balanceOf(address)                    returns (uint256) => DISPATCHER(true)
  allowance(address,address)            returns (uint)    => DISPATCHER(true)
  approve(address,uint256)              returns (bool)    => DISPATCHER(true)
  transfer(address,uint256)             returns (bool)    => DISPATCHER(true)
  transferFrom(address,address,uint256) returns (bool)    => DISPATCHER(true)
}

This way, whenever our Pool contract being verified makes a call to an ERC20 method, the prover will look for every ERC20 implementation we have and try it.

But things get messier when working with unknown contracts. What happens if we do not know what will be the instance that our contract will be working with? Following the previous example, what if we want to verify our system will work properly with any ERC20 implementation, even one we did not anticipate or a maliciously crafted one?

As we saw in the example above, the prover works on a method-by-method basis when dealing with external calls. For each method called by the contract being verified, we can define how we expect that call to behave. This is referred to as summaries in CVL.

For example, view functions can be annotated as returning anything from a constant to a completely non-deterministic value. Here's an example taken from OpenZeppelin contracts:

methods {
  hashProposal(...) returns (uint256) => NONDET
  hashOperationBatch(...) => DISPATCHER(true)
  executeBatch(...) => CONSTANT
}

The main challenge is dealing with non-view functions. The default behavior of the prover is to assume that an external call can alter all state on every contract but the caller, noted as HAVOC_ECF. This can lead to state changes in external contracts that are unreachable, making verification more difficult. Furthermore, it assumes that the call is non-reentrant, which in reality is a frequent source of attacks. This last issue can be avoided by indicating that calls can re-enter, noted as HAVOC_ALL, but this means that an external call can mutate any state in any contract, caller included. This leaves the contract being verified in a state where we don't know anything about it after an external call is made. This severely limits what we can prove.

A more reasonable approach is to assume that the callee can call back into any contract, but restrict it to actual method calls, instead of arbitrary state changes. However, this needs to be handled manually, by writing a contract that calls into each method based on an arbitrary parameter:

contract Receiver is ArbitraryValues {
  ERC20 asset;
  function exec() external {
    uint callback = arbitraryUint();
    if (callback == 0) 
      asset.approve(arbitraryAddress(), arbitraryUint());
    else if (callback == 1) 
      asset.transfer(arbitraryAddress(), arbitraryUint());
    else if (callback == 2) 
      asset.transferFrom(arbitraryAddress(), arbitraryAddress(), arbitraryUint());
  }
}

The ArbitraryValues base contract provides a set of arbitraryValue() methods that return a non-determistic value whenever we need it. These are used to pick both the method to be called and its arguments.

Note that this approach does not cover all possible interactions, since we are executing just a single callback, whereas there could be multiple reentrant calls.

One last approach to working with unknown contract implementations is to map a method to a function in CVL. Whenever that method is called from the contract being verified, the function will be called instead. This allows us to prove that our contract works as expected assuming that the callee adheres to the spec that has been defined. Note that the callee is not verified here, since there is no implementation to verify it against!

What are the best use cases for CVL?

After going through scenarios where we push the limits of CVL, let's close with the scenarios where it really shines. The presentation on categorizing properties from Certora's tutorial gives a good overview of these.

Understanding a smart contract as a finite-state machine (obligatory mention to Yoichi's bamboo, my favorite smart contract programming language that never happened) allows us to define clear rules on:

what are the valid states for the contract, and
what are the valid transitions between those states.

Let's grab some examples from OpenZeppelin's TimelockController spec. In a Timelock, operations can have different states. We can write a rule that checks, for instance, that calling execute is the only way for moving an operation from ready to done state.

rule readyDoneTransition(method f, env e){
  bytes32 id;
  require isOperationReady(e, id);

  calldataarg args;
  f(e, args);

  assert isOperationDone(id) => f.selector == execute(...).selector;
}

Or that done is a final state: no matter what we call on the contract, a done proposal will always stay that way:

rule doneToNothingTransition(method f, env e){
  bytes32 id;
  require isOperationDone(id);

  calldataarg args;
  f(e, args);

  assert isOperationDone(id);
}

And we can rely on invariants to assert the validity of each of these states (see representation invariants). For instance, an operation is ready to be executed if and only if its associated timestamp is non-zero and in the past:

invariant readyCheck(env e, bytes32 id)
  (e.block.timestamp >= getTimestamp(id) && getTimestamp(id) > 1) 
  <=> isOperationReady(e, id)

Another use case is for writing unit-test-like specs. For instance, in an ERC20, we would write a test that the transfer works: it decreases the balance of the sender and increases the balance of the receiver by the sent amount. We would test it with specific addresses with specific balances and a specific amount. But here we can just write that property, and have the prover verify it for every possible initial state and input, not just the ones we used in the unit test.

rule transfer(env e, address recipient, uint256 amount) {
  address holder = e.msg.sender;
  uint256 holderBalanceBefore = balanceOf(holder);
  uint256 recipientBalanceBefore = balanceOf(recipient);

  transfer(e, recipient, amount);

  assert balanceOf(holder)    == holderBalanceBefore    - (holder == recipient ? 0 : amount);
  assert balanceOf(recipient) == recipientBalanceBefore + (holder == recipient ? 0 : amount);
}

But we can also test more general properties. Following the previous example, we can just check that a transfer always increases the balance of the recipient and decreases that of the sender.

rule transfer(env e, address recipient, uint256 amount) {
  address holder = e.msg.sender;
  uint256 holderBalanceBefore = balanceOf(holder);
  uint256 recipientBalanceBefore = balanceOf(recipient);

  transfer(e, recipient, amount);

  assert balanceOf(holder) <= holderBalanceBefore;
  assert balanceOf(recipient) >= recipientBalanceBefore;
}

Or that transfer cannot create new tokens for the sender or recipient, meaning that the sum of their balances must remain constant.

rule transfer(env e, address recipient, uint256 amount) {
  uint256 balanceSenderBefore = balanceOf(e, e.msg.sender);
  uint256 balanceRecipientBefore = balanceOf(e, recipient);
  transfer(e, recipient, amount);

  assert balanceRecipientBefore + balanceSenderBefore == balanceOf(e, e.msg.sender) + balanceOf(e, recipient);
}

These are examples of high-level properties that hold over every execution of a certain operation, like transfer, or that hold over the entire contract throughout its lifecycle. The latter are best expressed in the form of invariants, as we saw early on with the Bank example.

invariant totalFundsGreaterThanAnyUser()
  forall address user. getTotalFunds() >= getFunds(user)

Learn more

To start playing with CVL, the demo site has a great interactive online editor, where you can write your contract and spec side-by-side and run the prover on it, or try out a bunch of examples.

Certora's tutorial on github is also a great starting point for the basic concepts, though the lessons for more advanced ones are still under development. The documentation provides a good overview and reference for many concepts, though it's also a work in progress, and redirects to an older set of docs for the more advanced ones. A multi-contract example repo is a good complement to see the documented concepts in action.

But when you are ready to move on from the tutorial and docs, the best source for learning are the actual specs for real-life projects, OpenZeppelin Contracts and AAVE being good examples.

Type-checking Lambda permissions with Typescript

Santiago Palladino — Fri, 04 Nov 2022 14:00:00 +0000

TL;DR

With Typescript, we can define the permissions granted to our lambda functions in our serverless apps using types. This lets us type-check access to resources, raising at compile-time any errors caused by missing permissions.

// We define our app permissions as objects
const ProductsAccess = { Products: true } as const;
const MailerAccess = { Mailer: true } as const;

// And we restrict access to any resource by requiring those permissions
getProductStore = (_policy: typeof ProductsAccess) => new DynamoProductStore();
getMailService = (_policy: typeof MailerAccess) => new SESMailer();

// Then we define the type of policies required by our lambda as an argument
async function lambdaHandler(event: Event, policies: typeof ProductsAccess): Promise<Result> {
  // And use those policies when requesting access to a resource
  // so the compiler catches if we try to access a resource for which we don't have the required policy
  const store = getProductStore(policies);

  // Next line fails to compile since our policies do not include acess to the mail service!
  const mailer = getMailService(policies);
}

And since we have defined our policies in code as part of each lambda handler, we can declare all parameters for each lambda in its handler file and use CDK to go through them and create the associated resources.

// src/api/get-product.ts
// We attach the lambda parameters to the handler function
export const handler = makeHandler(lambdaHandler, {
  policies: ReadOnlyProducts,
  httpMethod: 'GET',
  logicalName: 'GetProductFunction',
  resourcePath: 'products/{id}',
  entry: __filename,
});

// bin/stack.ts
// And we iterate through all handlers and create the associated lambda
import { MyStack } from '../lib/my-stack';
import * as handlers from '../src/api';

const app = new cdk.App();
const stack = new MyStack(app, 'MyStack', { ... });

for (const handler of Object.values(handlers)) {
  stack.makeFunction(handler.params);
}

// lib/stack.ts
// We build into the stack the logic to add each new lambda
export class MyStack extends Stack {
  public makeFunction(params: HandlerParams) {
    const fn = new NodejsFunction(this, params.logicalName, {
      entry: path.relative(path.resolve(__dirname, '..'), params.entry),
      ...this.getFunctionSettings(),
    });

    this.grantRights(fn, params.policies);
    this.api.root.resourceForPath(params.resourcePath)
      .addMethod(params.httpMethod, new LambdaIntegration(fn));
  }
}

This lets us define each Lambda in our application, along with its required permissions, in the same file where we declare the handler function, and leverage the type checker to catch any missing permissions.

So if you find this interesting, read on for the longer version, or check out this fork of the AWS serverless-typescript-demo for a full code sample.

The problem with permissions errors

A common error when building serverless applications is missing a permission for accessing a resource in a lambda function. These errors are particularly annoying because they show up late in the development lifecycle, since unit or local tests do not uncover permissions errors: you depend on integration tests to check that your lambdas have all the rights needed to run properly. An error here requires a full redeploy of the stack and a retest, which takes valuable developer time.

Moving these errors to earlier in the development cycle yields a faster feedback loop. In this article, we'll explore how to catch these errors at compile time leveraging the Typescript type checker, and take it one step further by integrating our new typed permissions directly into our CDK stack definition.

Typing permissions

Let's start by defining our application permissions as Typescript types. For the sake of the example, let's say we have a Products DynamoDB table in our application. We'll define two permissions, ReadProducts and WriteProducts, and use them to define a read-only and a full-access policy.

const ReadOnlyProducts = { ReadProducts: true } as const;
const ReadWriteProducts = { ...ReadOnlyProducts, WriteProducts: true } as const;

Note the as const in the declarations. This ensures that the type of each policy requires a true value for each property, and not any boolean.

We could have defined our policies as just an enumeration of permissions instead of using an object as we did above. But using objects like this plays nicely with the type system: a policy that extends another with additional permissions will also extend it in the eyes of the compiler.

function listProducts(policy: typeof ReadOnlyProducts) {
  // ...
};

requiresReadProducts(ReadOnlyProducts); // Works
requiresReadProducts(ReadWriteProducts); // Works, since RW extends RO!

You can define whatever arbitrary permissions you need for your application. These can go about sending emails, managing users, or pushing notifications. And you can combine them freely into policies. We'll worry about converting them into actual IAM policies later.

// Example of a policy needed for running a UserManager
const UserManagerPolicy = {
  ReadUsers: true,
  WriteUsers: true,
  SendEmails: true,
  PushNotifications: true,
} as const;

Checking permissions when accessing resources

Once we have our sets of application permissions defined, we can now enforce them to request access to resources in our code.

Going back to the example from the previous section, we can abstract access to the Products table behind a ProductStore, with a DynamoDB-based default implementation.

export interface ProductStore {
  getProduct: (id: string) => Promise<Product | undefined>;
  getProducts: () => Promise<Product[]>;
  putProduct: (product: Product) => Promise<void>;
  deleteProduct: (id: string) => Promise<void>;
}

We can also restrict the interface above to getter methods, which we will use if the client has read-only permissions:

export type ReadOnlyProductStore = Pick<ProductStore, 'getProduct' | 'getProducts'>;

Now is where things get interesting: we can define a function that returns a read-only or full ProductStore depending on the type of the policies supplied by the caller:

export function getProductStore
  <Policy extends typeof ReadOnlyProducts>(_policy: Policy): 
  Policy extends typeof ReadWriteProducts 
    ? ProductStore 
    : ReadOnlyProductStore {
  return new DynamoProductStore();
}

Note that we don't even use the policy parameter in the body of the function, since actual permissions will be checked by the AWS policies we define. What we are doing here is asking the type system to check if the user has read-only or read-write permissions on the Products table, and return the corresponding interface. On runtime, we just return the same implementation.

This achieves our goal of restricting access to resources based on the type of the policies we're working with, which raises any permission errors during compile-time.

// Works
getProductStore(ReadWriteProducts).putProduct(product);

// Property 'putProduct' does not exist on type 'ReadOnlyProductStore'
getProductStore(ReadOnlyProducts).putProduct(product);

// Argument of type '{ readonly ReadUsers: true; }' is not assignable to parameter of type '{ readonly ReadProducts: true; }'
getProductStore(ReadWriteUsers).putProduct(product);

Declaring permissions for each lambda

The most straightforward way to use this pattern is to declare, for each lambda, which set of permissions we will be granting it. This serves as a documentation attached to each function, which we can use to easily determine which policies we need to define in our infra-as-code.

async function lambdaHandler(event: APIGatewayProxyEvent) {
  // We declare the policies for this lambda once
  const policies = { ...ReadOnlyProducts, ...UserManagerPolicy };

  // And use them whenever we need to instantiate a resource
  const service = getService(policies);
}

But since we are already defining these policies in code, we can take this an extra step and use them to actually generate the policies in our infra-as-code template. As a matter of fact, we can extend this to generate the entire function template from a single source of truth.

Integrating with CDK

Our goal will be to write the policies for each lambda in a single place, and 1) have the type checker verify that we have the required policies for accessing all resources we need and 2) generate these policies in our infra-as-code template. Since we're already working with Typescript, we'll use CDK as our infra-as-code tool.

To do this, we'll attach the policies to the exported handler function, so we can query them when building our stack from CDK.

// src/api/get-product.ts
const policies = { ...ReadOnlyProducts };
const handler = (event: APIGatewayProxyEvent) => lambdaHandler(event, policies);
handler.params = { policies };

export { handler };

So when we define our stack using CDK constructs, we can import each handler and define its IAM permissions from the ones we exported.

// lib/stack.ts
import { handler as getProduct } from '../src/api/get-product';

// We define our resources in the stack constructor
const productsTable = new Table(...);
const api = new RestApi(...);

const getProductFunction = new NodejsFunction(
  this,
  "GetProductsFunction",
  { entry: "./src/api/get-products.ts", ...settings },
);

api.root.resourceForPath('products/{id}')
  .addMethod('GET', new LambdaIntegration(getProductFunction));

// A helper function translates from our custom policies
// to the actual IAM permissions to be created
const grantRights(lambda, policies) => {
  if (policies.ReadProducts) productsTable.grantReadData(lambda);
  if (policies.WriteProducts) productsTable.grantWriteData(lambda);
};

// And we repeat for each lambda in the app
grantRights(getProductFunction, getProduct.params.policies);

But now we have split the definition for our lambda in two different places: policies are in the handler source file, and the rest of the settings are in the stack file.

What if consolidated them into a single source of truth in the handler?

Taking CDK integration one step further

Let's take the approach from the previous section one step further and inject all information relevant to the lambda when declaring its handler function:

// src/api/get-product.ts
const policies = { ...ReadOnlyProducts };
const handler = (event: APIGatewayProxyEvent) => lambdaHandler(event, policies);
handler.params = { 
  policies,
  httpMethod: 'GET',
  logicalName: 'GetProductFunction',
  resourcePath: 'products/{id}',
  entry: __filename,
};

export { handler };

Now we can add a function to our stack that accepts this set of parameters and creates a new lambda, connects it to the API gateway, and grants it the set of permissions defined in the policies:

// lib/stack.ts
class MyStack extends Stack {
  public makeFunction(params: HandlerParams) {
    const fn = new NodejsFunction(this, params.logicalName, {
      entry: path.relative(path.resolve(__dirname, '..'), params.entry),
      ...this.getFunctionSettings(),
    });

    this.grantRights(fn, params.policies);
    this.api.root.resourceForPath(params.resourcePath)
      .addMethod(params.httpMethod, new LambdaIntegration(fn));
  }
}

And we just invoke it for each handler in our application when constructing the stack:

// bin/stack.ts
import * as handlers from '../src/api';

const app = new cdk.App();
const stack = new MyStack(app, 'MyStack', { ... });

for (const handler of Object.values(handlers)) {
  stack.makeFunction(handler.params);
}

This way, we have the definitions of the main resources of the application in our lib/stack.ts file, while each function is declared in its own individual file, along with its associated permissions - which get type checked when requesting access to any resource!

Full example

You can check a full code sample of the pattern above in spalladino/serverless-typescript-demo, which is a fork of the aws-samples/serverless-typescript-demo that showcases a products CRUD built using Typescript and CDK.

A case for secure web3 operations

Santiago Palladino — Tue, 04 Oct 2022 21:25:01 +0000

Security in web3 development has improved remarkably over the past years. Even though we still see frequent hacks due to coding errors, development security practices have evolved significantly across web3 teams. Full test coverage, static analysis tools, fuzzing, and mandatory peer reviews are a requirement across most teams, while audits and bug bounties add an extra layer of security.

However, the security in web3 operations is far from this level of maturity. Hardly any projects have any dedicated ops teams, and there is a general lack of awareness on best practices for operations in the web3 space. Security does not end when the code is frozen and audited: deployments, upgrades, integration testing, administration, automation, and monitoring also need to be bulletproof to avoid any hacks.

Going through the Rekt leaderboard is evidence enough: many of the top incidents were not caused by development mishaps but by operational oversights, and several of them could have been mitigated by proper monitoring and incident response practices. Examples include compromised frontends, hacks that go unnoticed for days, incorrect initializations, compromised keys, and more. In more recent news, a missing initialization in Arbitrum Nova led to a 400 ETH bounty payout, while Wintermute was hacked for $160M due to a compromised private key.

While working at OpenZeppelin, we set out to interview multiple projects in the space to better understand their security needs. While training their Solidity developers in security was top of mind for most teams, we noted that operational concerns were often relegated:

“We write a one-off script whenever we need to upgrade”
“Transactions are sent from a private key stored in a file on a shared server”
“We’d want to use a multisig or timelock eventually but tooling is lacking”
“I don’t know what to monitor”
“The lead developer just deploys the contracts from his working copy”
“I open etherscan every morning to see if everything looks fine”

This research led to the development of OpenZeppelin Defender, today in widespread use across the space for securing web3 operations. Here we'll share the learnings collected along the way and the pain points we found in the space. We’ll focus on five different operational areas: Integration, Deployment, Administration, Transaction Automation, and Monitoring.

Integration Testing & Staging Environments

The DeFi cambrian explosion from a few years back was made possible by a highly interconnected ecosystem, with a synergy only attainable by building protocols on top of others, and leveraging the primitives available to build more powerful instruments.

However, testing in such an interconnected environment is challenging: how do you test your protocol when it depends on so many live systems and moving pieces? As an example, Compound’s recent cETH price feed incident was triggered by perfectly valid code, audited by three different companies, but which interacted with a token implementation that had not been considered.

Testnet deployments are far from representative of an actual production setup. Few protocols deploy their systems to both testnet and mainnet, and even fewer bother to deploy exactly the same versions. Testnets fragmentation doesn’t help either, though the upcoming deprecation of Rinkeby, Kovan, and Ropsten will help. Furthermore, even if the code is the same in mainnet and testnet, the state of the system differs widely due to real production usage.

Mainnet forks help a lot here, but it is still difficult to test what would happen in other possible scenarios. Even if it’s an extreme case, hardly any team has ever tested how their protocol would behave should MakerDAO hit the emergency button on DAI.

Another issue is that automated integration tests on mainnet forks typically only focus on contracts. Nowadays, a web3 system is rarely composed of just smart contracts: it integrates multiple off-chain components as well, such as oracles, bots, and indexing engines, not to mention the frontends that users depend on.

These issues call for new solutions in integration testing. First and foremost, live staging environments, with a setup as representative as possible (both on and off chain) of the actual mainnet environment, is a must for manual testing and assuring that all components work as expected. Long-lived mainnet forks are a good way to start here.

Reliable deployment packages for popular protocols can provide the means for setting up environments with hypothetical scenarios. Imagine being able to spin up a version of Maker going through a black thursday scenario in any network with a few commands, so you can test your system reacting to it. While this requires a massive community effort to populate the many protocols and the many scenarios that are possible, it is worth the investment. This endeavor also requires a declarative deployment standard to build on top of.

Last, blockchain determinism and public record gives us a unique opportunity to test new implementations without even having to put them in production - the opposite of the test in prod meme. As an example, in the traditional development space, Github tests new code strategies by executing them against live production requests and comparing them with the legacy code until they are satisfied with the results. Today, we have all the building blocks needed for replaying live transactions against a new version of a system before making the upgrade, without even having to deploy the system to mainnet for it.

Reproducible & Auditable Deployments

While most web2 systems are deployed from CI/CD pipelines, contract deployment is still very much a manual process. It usually falls on a developer to checkout the code, compile it, write a hardhat deployment script, deploy from their workstation, and then verify the source code on Etherscan or Sourcify.

This has several downsides, besides the hassle for the developer, who also needs to keep a funded private key handy to pay for the deployment gas costs. The main problem is a lack of traceability, as the process for going from the vetted source code to a live instance is opaque. This can lead to issues where the deployed code does not match the audited version, inadvertently introducing a vulnerability. And, in the interest of transparency, having an audit report that refers to a git commit does not offer much information to a user who is interacting with an address on Metamask.

Lack of reproducibility is also a problem as more protocols go multi-chain. Ideally you want to keep the same version of the code running on all the chains where you operate, but to do this, you need to be able to reliably re-deploy exactly the same version. This means starting from the same version of the source code, building with the same settings and compiler version, and deploying with the same configuration.

The low-hanging fruit here is to move deployments to a transparent CI/CD pipeline, where anyone can follow the automated process from the source code to compiled bytecode, and from there to the deployed instance. Online tools can also facilitate auditability by verifying that the code at an address matches a specific artifact. The end goal is to have a reproducible process and auditable trail from a git commit to a deployed instance.

Administration & Governance

With very few exceptions, most smart contract systems keep a set of administrative functions that allow a governing body to tweak how the protocol operates. These can go from adjusting a parameter to a full-blown code upgrade. Treasury management can also be considered part of the administration of a protocol. Given how critical these functions are, it is imperative they are controlled by secure and trusted entities.

The state of the art when it comes to governance has improved remarkably over the last few years. It was not uncommon to see protocols with millions of dollars managed by a single private key sitting in the Metamask wallet of the project lead developer.

Fortunately, it has now become commonplace the use of multi-signature wallets, with Gnosis Safe being the most popular option. However, multisig contract implementations are only one part of the picture: good tooling for creating and reviewing transactions is needed to guarantee secure operations run through these contracts.

Tools for creating transactions need to account for not just the multisig, but also other governance and security mechanisms set up, such as timelocks or vote-based governance contracts. Governance contracts decentralize the decisions in a community, though many projects still restrict who can create new proposals, retaining that power behind a multisig. And timelocks provide two simultaneous benefits: they give the project’s team time to react if their setup was compromised, and they protect the community against rugpulls by giving users the time to exit the protocol if a malicious proposal is put forward. While a multisig transaction builder is good enough for creating transactions sent directly to the application, more complex tools are needed as these building blocks are combined.

Reviewing administrative proposals is particularly challenging from a UX perspective. Many project stakeholders are not developers, meaning they cannot manually run scripts to decode or analyze a transaction before approving it. All too often, an N/M multisig becomes 1/M, where the 1 is the lead developer who pushes a proposal and asks the remaining M-1 to sign, who blindly hit the approve button.

Simulation is the best resource we have for analyzing the outcome of a transaction, but the simulation tools that we use as developers may not cut it when it comes to less tech-savvy users. There is a need for simulation capabilities that are accessible and easy to understand for everyone, so they can verify by themselves, and not trust.

Contract upgrades deserve a separate paragraph. Approving an upgrade as a multisig signer means agreeing to a potentially massive change, while having only the 40 hex characters of the new implementation contract as context. And while having the source code verified on Etherscan is a requirement, the process of linking that code back to a verified or audited git commit is cumbersome (if not impossible) for most users. Easy-to-audit deployments, as detailed in the previous section, are a requirement for secure upgrade operations. It also helps to have a strong suite of integration tests for the new implementation that signers can review before approving.

Transaction Automation

An automated script that submits transactions to the network needs access to a funded hot wallet. Gasless transactions is one of the most popular use cases here, and compromising the key of a meta-transaction relayer would mean draining all the funds allocated to paying gas fees. However, there are scenarios where these off-chain scripts need to manage keys with sensitive privileges, such as updating an oracle or managing a bridge. A compromised private key in this scenario can have dire consequences, as was the case with Harmony’s bridge hack for over $100M.

This makes private keys more sensitive than your average application secret, so storing them in plaintext in a dot-env file in a server where half the dev team has ssh access is not a good idea. It is key (pun intended) to leverage key management solutions that can keep the key safely stored. There are managed cloud-based options, such as GCP KMS or AWS KMS, self-managed like Hashi Vault, and even hardware security modules for hosting your keys.

Most of these solutions also expose cryptographic functions in their API, so you can send your payloads to be signed by the KMS and the private key never leaves the secure vault. Keeping the keys in a secure vault also lets you maintain an audit trail of all requests for using it, so you can easily detect or trace back any unauthorized usage.

Reliability is also a concern when it comes to transaction automation. In blockchain, It is not enough to send a transaction, since you have no guarantees that it will get mined. Any automation infrastructure needs to monitor any in-flight transactions to reprice and resubmit them if network congestion increases, and ensure that a low-priced transaction will not clog the sender for any subsequent ones. There are multiple managed solutions for tackling this problem, though you can also write your own.

Security Monitoring

Monitoring and alerting is commonplace on any web2 application, but its adoption in the web3 space started only recently with platforms like Defender, Forta, or Tenderly. For an embarrassingly long time, the most widely adopted approach to security alerts was samczsun’s trademarked “u up?”. Such was the state of monitoring that the largest crypto hack ever ($624M) went unnoticed for almost a week.

Reacting timely to a security event is important not just for being on top of the incident and keeping your community reassured, but also because many hacks don’t involve a single action. Attacks usually require multiple transactions in preparation and execution, spread over time. As an example, BadgerDAO’s hack lasted 10 hours until all user wallets were drained.

Receiving an early notice of an attack can give you the time to pause the protocol and stop the bleeding. Circuit breakers are a particularly interesting building block here: scripts triggered by security monitoring alerts that rely on transaction automation for pausing the system when a threat is detected.

Last, custom monitoring scripts are also becoming a common practice, but it’s important to monitor the monitoring. A failure on an alerting script can go undetected, since it is expected to be silent, and can lead to a missed opportunity to deter a hack.

Conclusion

As recent hacks prove, security in operations is as critical as in development. Security does not end with Solidity: the most secure smart contract is worth nothing if its onlyOwner wallet gets compromised. There is a need for a DevSecOps approach for the web3 ecosystem, powered by platforms and tools that provide the means to implement its processes and best practices.

Speed up your AWS SAM development by deploying individual functions

Santiago Palladino — Sun, 27 Sep 2020 20:03:37 +0000

Cover image from https://aws.amazon.com/lambda/getting-started/

The Amazon Web Services Serverless Application Model (or AWS SAM, for short) is a framework for simplified development of serverless applications on top of AWS. SAM ships with a CLI that provides common operations, such as packaging and deploying your application, or spinning up a dev server for local testing.

Behind the scenes, SAM relies on CloudFormation, a mature template-based language for describing and deploying entire AWS stacks. Whenever you deploy your application, SAM will compile your code, upload it to S3, and use CloudFormation to update your stack.

The problem

While this process is (usually) reliable and leads to reproducible deployments, it can also become painfully slow as your stack grows. Given a stack with about 200 resources, a deployment where nothing has changed takes about 10 minutes from start to end. Compiling the entire codebase takes time, as well as uploading it and letting CloudFormation run its course.

Though 10 minutes is acceptable for a full deployment, it is not for trying out your changes while developing. You need a much faster feedback loop if you want to stay in flow. To address this, other frameworks such as serverless.com provide a command deploy function that bypasses CloudFormation entirely, and simply uses the AWS Lambda API to update the function code directly. Unfortunately, this is not available as part as the AWS SAM CLI. While researching this, I found a CLI called sampic built by a community member on top of SAM, but it seemed too heavyweight for what I was looking for.

Hacking a solution

Given that switching from SAM to serverless.com can be too disruptive in an already established project, I set out to reproduce the deploy function behavior manually for our webpack-powered typescript AWS SAM project. The end result is a 120-lines script, most of which is just logging, that picks a subset of functions from a SAM template, compiles them, and uploads them via the AWS Lambda API.

Note that this solution only works if the function has already been created by sam deploy. The script will not create the function if it doesn't exist, it only knows how to update its code.

In this post, I'll walk through the necessary steps to build this solution - but you can also just jump directly to the entire code snippet at the end of the post!

Getting started

The first step is to choose which functions to deploy. To do this, we'll compare all function names in the template to an fname substring provided by the user, and filter only those that match.

We'll use the yaml-cfn package for parsing the template, since CloudFormation accepts a set of non-standard YAML tags for intrinsic functions which can break a vanilla yaml parser. And we'll use lodash, because I can't code in js without it.

const { readFileSync } = require('fs');
const { yamlParse } = require('yaml-cfn');
const { map, pickBy } = require('lodash');
const TEMPLATE_FILENAME = 'template.yaml';

const template = yamlParse(readFileSync(TEMPLATE_FILENAME, 'utf8'));
const filtered = pickBy(template.Resources, (resource, name) => (
  name.toLowerCase().includes(fname.toLowerCase()) 
  && resource.Type === 'AWS::Serverless::Function'
));
const functions = map(filtered, (fn, name) => (
  { Name: name, ...fn.Properties }
));

This will return an array of objects like the one below, with the metadata of the functions to be deployed.

Name: 'UserInviteFunction',
FunctionName: { 'Fn::Sub': '${AWS::StackName}-${Stage}-user-invite-fn' },
CodeUri: './build/users',
Handler: 'index.inviteUser',
Events: { InviteUser: [Object] }

Compiling only what's needed

Now that we know which functions we want to deploy, it's time to compile them. I'm currently using webpack, with one entry point for each set of related endpoints; but if you're using a different bundler, you may need to adapt the following steps to it.

// webpack.config.js
module.exports = {
  entry: {
    authorizer: './src/authorizer/index.ts',
    projects: './src/endpoints/projects.ts',
    organizations: './src/endpoints/organizations.ts',
    actions: './src/endpoints/actions.ts',
    users: './src/endpoints/users.ts',
    ...
  },
  output: {
    filename: '[name]/index.js',
    libraryTarget: 'commonjs2',
    path: resolve(__dirname, 'build'),
    sourceMapFilename: '[name]/index.js.map',
  },
  ...
}

To speed up compilation, we will filter the set of entry points defined in our webpack config so we only compile those necessary for the functions to be deployed. If you have over 25 different entrypoints like I do, this can be a major time saver!

const { basename, resolve } = require('path');
const { uniq, pick } = require('lodash');

const WEBPACK_CONFIG = './webpack.config.js';
const config = require(resolve(WEBPACK_CONFIG));

// We map from CodeUris like './build/users' to entries like 'users'
const entryPoints = uniq(functions.map(f => basename(f.CodeUri)));
config.entry = pick(config.entry, entryPoints);

Before we trigger the compilation, we'll add an extra step. When using sam deploy, the SAM CLI takes care of zipping and uploading the code for us, but since we are uploading the code manually, we'll need to zip it ourselves.

Unfortunately, webpack's compression-webpack-plugin does not support zip files, and the zip-webpack-plugin does not support multiple entry points. So, we will just tap into the assetEmitted webpack hook and zip from there. We'll just use the zip OS command to do this, but we could also use a package like yazl or jszip.

const { dirname, extname } = require('path');
const { promisify } = require('util');
const exec = promisify(require('child_process').exec);
const webpack = require('webpack');

const compiler = webpack(config);
compiler.hooks.assetEmitted.tapPromise('zip', async (filename) => {
  if (extname(filename) === '.map') return;
  const cwd = resolve(config.output.path, dirname(filename));
  await exec(`zip index.zip index.js`, { cwd });
});

With all of this set up, we can finally set out to compile our functions.

const stats = await promisify(compiler.run.bind(compiler))();
if (stats.hasErrors()) throw new Error(stats.toJson().errors);

Resolving function names

We now know what functions to deploy and have compiled them. But before uploading the code, we need to know the physical resource names of the lambdas we are targeting.

In a CloudFormation stack, the name you assign to each resource is called the logical name. However, this is not the name used when creating the resources. Given that your resources must have unique names within an account and region, CloudFormation will use a combination of your stack name, the logical name, and a unique identifier for the actual physical name. You can also control the name for each resource by setting a Name property in your template.

Fortunately, the CloudFormation API allows us to retrieve the physical name for a resource given its logical name and stack via a DescribeStackResource method.

const { CloudFormation } = require('aws-sdk');
const STACKNAME = 'MY-STACK';
const cfn = new CloudFormation();

const resolvedFunctions = await Promise.all(functions.map(async (fn) => {
  const response = await cfn.describeStackResource({
    LogicalResourceId: fn.Name, StackName: STACKNAME 
  }).promise();
  const resourceId = response.StackResourceDetail.PhysicalResourceId;
  return { ...fn, ResourceId: resourceId };
}));

Armed with the actual lambda function names, we can now finally use the UpdateFunctionCode API method to upload our code directly to our Lambda functions.

const { Lambda } = require('aws-sdk');
const lambda = new Lambda();

await Promise.all(resolvedFunctions.map(async (fn) => {
  const zipFilePath = resolve(fn.CodeUri, 'index.zip');
  await lambda.updateFunctionCode({
    FunctionName: fn.ResourceId, ZipFile: readFileSync(zipFilePath) 
  }).promise();
}));

Measuring it

When compiling and deploying a single function, the script above takes roughly 20-30 seconds, most of which is spent in compilation. To compare, deploying the stack via sam deploy takes about 10 minutes, which means we're in for a 20x speed increase during development. A faster feedback loop means more development productivity, so achieving this kind of gains can be a major improvement to your project.

Putting it all together

Here is the entire script we are using today for development, which puts together all the steps described above, along with some logging and validations. Keep in mind that some bits may be different on your own setup, such as the paths where the artifacts are generated, or how your template is organized. Nevertheless, I expect it to work in most setups with just minor tweaks.

Happy coding!

Announcing Crystal CodeCamp SF2017

Santiago Palladino — Thu, 23 Mar 2017 21:25:14 +0000

This blogpost was originally posted by MarÃa Inti David on the official Crystal Blog

We're happy to announce that the Crystal team is coming to San Francisco!

Maybe you've heard we're organizing the first #CrystalLang CodeCamp. The event will consist of a 2 day hands-on training dictated by Santiago Palladino & Gustavo GirÃ¡ldez, members of the Crystal core team. Serdar DoÄŸruyol (creator of Kemal) will also be joining us as a guest speaker.

The programme includes hands on labs, Q&A sessions with the team, networking sessions and more than 10 hours of training. We will provide official Crystal certificates for attendees, along with the obligatory Crystal swag.

Right now this event is possible thanks to:

AcademyX, who is sponsoring us and providing the space to host the event at their San Francisco offices.
Twentify, who is sponsoring the event and also making it possible for Serdar to travel and be a guest speaker.
Manas.Tech, the company behind Crystal since 2011.

We're looking for sponsors who want to support the event, so if you're interested (or know someone who might be) make sure to read our sponsorship prospectus. As with every other official Crystal event, all profits from sponsorships and ticket sales will be destined exclusively to Crystal Development. This will help us invest more hours in the language and accomplish our 2017 resolutions (yes, I'm talking about Crystal 1.0).

We hope this is the first of many Crystal CodeCamps around the world, so we're open for suggestions about where we should go next.

PS: This blogpost will be updated as new sponsors join us, we want to thank the companies supporting Crystal in this new event series.

State of Crystal at 0.21

Santiago Palladino — Fri, 24 Feb 2017 12:52:17 +0000

This blogpost was originally posted on the official Crystal Blog

With the release of version 0.21, we wanted to share with you the state of Crystal development so far this year, aiming towards a 1.0 version by the end of the year.

First and foremost, we have updated our roadmap with the goals we have in mind, not just for Crystal during this year, but also tools we would like to see built using the language in the future, such as a full DSL for easily writing Ruby extensions, or a desktop UI library. We have also changed our labelling scheme for Github issues, and updated the contributing guidelines accordingly, to make it easier for anyone in the community to find out how to help with Crystal.

Regarding the key features we had identified for 1.0, we are making steady progress on Windows support, with work from community member lbguilherme and core team member bcardiff. Today Crystal is able to compile some programs in Windows, and the last milestone has been support for exceptions in that platform. We still have a long way to go on the standard library front, as every module was implemented with just UNIX support in mind, so contributions are most welcome from anyone interested in the Windows platform.

The next big thing is parallelism, with core team members ggiraldez and juanedi working heavily on it, based on the work started by waj. We are happy to have a working version of the compiler built with multi-thread support, with a similar model to Go: a fixed thread pool that executes tasks from fibers, including goodies such as work-stealing. Work on this is still experimental, and there are quite a few breaking changes to define, such as explicit Thread handling; but most of the compiler and standard library specs are currently green. Kemal's author sdogruyol even managed to run the web framework in multiple threads already. However, there is still much work to do on testing and performance, to ensure the contention produced by distributing the workload on multiple threads does not offset the speed gain.

We have also started discussions on the type system to ensure the feasibility of incremental compilation. We have identified some potential bottlenecks on generics and on modules-as-interfaces that will have to be addressed, and we'll do our best to identify the breaking changes required as soon as possible, as well as minimise their impact.

On the communications front, we are also now cross-posting from our official blog to the awesome platform dev.to, where you might be reading this post now. The folks at ThePracticalDev were super friendly and set up a crystal-lang account for us in no time on the site. Many of us in the Crystal core team have been following the site and twitter feed for quite some time, and are now really excited to see Crystal have a room in the platform.

Also, and not to spoil the surprise, but we have almost finished a brand new version of our website, with a much cleaner design. Expect to see it online quite soon.

Last but not least, we are happy to have given talks at Google NYC and Recurse Center earlier this month, as well as organised another meetup. We are also organising the first Crystal Code Camp for April in San Francisco: let us know if you are interested in joining, or contact us if you want to sponsor the event!

We'll share news from the state of Crystal in a regular basis, so make sure to stay tuned to the blog and other communication channels. Happy Crystalling!