Build

Inside Miden’s Audits (Interview with François & Marti)

Miden’s product marketer Gaylord Warner (@zkGaylord) chatted with cryptography engineering lead François Garillot (@huitseeker) and protocol engineer Marti Górny (@mmagician). They discuss what Miden’s external audits uncovered, how the bugs were fixed, and why the team is taking extra precautions during rollout.

The audits covered different parts of Miden. OpenZeppelin audited the protocol and smart-contract standards, while Trail of Bits audited the VM and developed formal-verification tools. Miden also commissioned audits from Spearbit.

What do you work on, and what part of the audits were you involved with?

Marti: Daily, I work with the core Miden protocol: defining how transactions, accounts and notes work, and how the VM executes a transaction.

Then the other part is the smart contract standards. We don’t want users to write this from scratch because it’s difficult, and there’s usually bugs when people do this from scratch. So we want to minimize the surface of potential vulnerabilities. This is joint work between the protocol team and the OpenZeppelin team. I’m involved in both, and the audits covered both.

François: My team has been focused on the audit of the Miden cryptography project as well as the VM.

That roughly consists of everything that looks like a STARK prover, as well as everything that creates a virtual machine around that. That runs from the implementation of the processor all the way into how we organize the state and the code of the Miden VM, which is maintained using commitments in the Merkle trees that everybody in the blockchain community is familiar with, as well as regular old computer science.

Was anything else audited?

Marti: We also had a few other audits that covered things outside of the core protocol work. There are two other prominent audited areas; the first one is the Agglayer bridge contracts. This was one separate piece of work and one audit.

And then the second one was the USDC faucet standard. This was also a separate audit. Now this is part of the protocol core repo, and also the Agglayer work is part of the protocol repo. But in my head, these are two separate audits.

What makes Miden different to audit?

François: It’s very often the case that blockchain projects have their own little in-house language, and Miden is no exception. We have a language rooted at the heart of the Miden blockchain, and nothing goes on without going through that language.

For example, when you’re doing simple transfers, we are expressing proofs about that transfer using Miden’s language, which is Miden Assembly, or MASM. This is the “one funnel to rule them all,” the “one ring” through which all transactions and all ways of operating on the Miden blockchain go. It’s the one way to make proofs, and so it’s a very core and important way of wrapping your head around what the Miden blockchain and what the Miden VM do.

Marti: If it’s the first time you look at Miden Assembly, it’s a bit scary. This is a very low-level language, you push items on the stack, you pop items off the stack… Using a stack is a low-level concept, which people don’t really think about anymore when programming.

Do you have some examples of bugs the audits found?

François: Trail of Bits found an issue with our rotation operation, which does a bit rotation on a 64-bit integer, and that one could have overflow problems on very large inputs. We fixed that, that was great, found with formal modeling, fantastic. Then there were a couple of those bugs, relatively minor and fixed very quickly – we’re talking a one-line fix. But they’re still quite important, I don’t want to minimize those bugs.

Marti: There was this one finding in an OpenZeppelin smart contract audit which was classified as critical. We had this issue with a single transaction that could execute multiple notes – well, we still do have this capability, that’s fine, but the problem was that one note could basically call “remove assets” on another note. You could give it an index of another note, and then it would remove assets from another note.

It was very specific, this wouldn’t work for any random notes, and you couldn’t just steal it from any random note, but there could have been notes that don’t have checks against this. Actually, there were some in our standards that were vulnerable to this attack.

So even more concretely, what could have happened to a Miden user?

Marti: If you picked up a note script, maybe it was like a free ticket. You win a lottery ticket, and then you add 10 USDCx to your account. If you don’t inspect it and you don’t see that there’s a second part that actually takes 100 USDCx from another note that is consumed, then what could have happened is that this first note could have created a note for the attacker and put assets from another note into this note for the attacker.

This one was a very sophisticated attack because it relied on you consuming multiple notes in the same transaction. This other note would have to be unprotected against this attack. The vulnerable note would have to not have a check that says, “I had this initial amount, and I’m moving out this final amount, and they’re the same.” If it just moved out the final amount without checking that it’s the same as the initial amount, then this attacker’s note could have removed assets in between.

How was that fixed?

Marti: We have a concept of native account context, so that some actions can only be called from within the native account. The native account is the executing account of a transaction. Something can be executed as part of account code or as part of a note script. The attack was executed as a note script, so we restricted the action of removing assets to being callable from the account context only.

With MASM so central to Miden, how did Trail of Bits approach it?

François: That’s the great thing about working with Trail of Bits: they have a lot of background and formal training in language analysis and semantic analysis. When you work with them, those methods come out in the form of tools.

MASM as a programming language has a particular way of modeling computation, and then it has an implementation behind the scenes. This requires checking that the specification about the instruction and what its impact is supposed to be on the state of the Miden VM actually corresponds to what is implemented in the backend using a circuit constraint. This is where formal verification becomes quite useful.

Formal verification, as a term, is really just a way for academics to organize the topics of their conferences: here’s where you should submit your paper and here’s where you shouldn’t submit your paper [smiles]. But the idea around formal verification is that it’s a bag of sub-disciplines.

One of them is formal theorem proving using Lean, where we are writing theorems about a model of the Miden VM, and then checking that this model corresponds to the code. There’s another approach, which is abstract interpretation, which looks at certain relations within the data flow of Miden in its standard library, and then tries to extract and verify certain properties about this data flow. Trail of Bits has actually delivered two, not one, formal verification methods.

Let’s expand on this: how far does that formal work go today?

François: When it comes to formally verifying a full model of the Miden VM, at the moment we have focused mostly on arithmetic operations that we expose to the user. The workhorse internal type that we’re using is a field element of the Goldilocks field. That field element is not your vanilla 64-bit integer. It looks very close to your 64-bit integer, but it has slightly different properties.

What we’re really trying to do is to give users normal 64-bit integers to deal with. To give that familiarity, we need a little bit of a translation layer across the operations and instructions that are offered by the VM.

There are many other aspects of the VM, which is a stack machine: it has a particular interpretation of memory, has a particular advice tape... We don’t have a full model for all of what is going on in all those other parts of the VM (yet).

What we intend to do is slowly and progressively extend our model from the core of the arithmetic operations over field elements, and how those are composed to offer a familiar and valid u64 API to users. And over time, we expect that we’ll have more and more confidence over other areas of the VM.

What did the auditors’ tools add to the process?

François: Those tools have been developed by Trail of Bits in the form of prototypes. They’ve been run against Miden VM, and they have found relatively subtle bugs that we wouldn’t otherwise have had the time to find and drill into. That has been in itself valuable.

Marti: We were given access to OpenZeppelin’s AI audit platform. Basically, how this works is you specify the scope, basically the files on GitHub. You connect your GitHub account to their audit page, specify the scope, and then can run audits a few times and see what the AI agents find. This produces a bunch of false positives, but we did actually find a few vulnerabilities there that we later fixed. So that was definitely useful.

And what does it take to keep using those tools?

François: We are taking over the maintenance and the professionalization of the tools developed by Trail of Bits, which then are becoming part of our tool set and are run regularly on a routine basis on our VM, to make sure that basically we close the door to those bugs. The key thing that was important for us is, those tools have chances of eliminating an entire class of bugs.

We didn’t want just the one spot check that gives us insight into the bugs that are there today. We wanted to make sure that we had the ability to never see that kind of bug come back, so that we can move on and deliver features to our users instead of constantly fixing the security of the VM.

Sadly, there are relatively deep reasons for why there isn’t a single tool that fixes it all. If there was one, we would know.

Marti: Using OpenZeppelin’s platform does introduce a little bit of overhead for us because we have to triage those findings manually. We ended up doing this manually a couple of times, between different people involved in the work streams.

Even after the audits, Miden is rolling out gradually. Why?

François: I am very happy about Miden’s approach to doing very pragmatic, roll-up-your-sleeves rollout and deployment, in the ways that engineers that are typically not in blockchain consider an absolute minimum. Going directly to a public mainnet is considered great from a point of view of decentralization because it’s permissionless. We are kind of going against the flow by having a vetted, permissioned set of participants in that initial partner mainnet.

I think this requires comparing this to the history of the deployment of privacy-preserving blockchains. Every single asset circulating on a private blockchain has a supply, an asset supply or money supply in the case of your own token, that is tightly controlled. Some of the bugs we’ve seen historically put doubt on whether that property was maintained.

What remediating this means is that you have to take all the state that came out of your prior experiment that had a bug, and then take all the assets of all your users, require them to migrate out of that old state into a new state, because suddenly you cannot trust that their older state didn’t have one of those inflation bugs. All of this is quite cumbersome on users.

Marti: Proving systems are still kind of a new concept. We’ve had the cryptography around for a while, but the actual implementations that are being used by us and by other teams in the blockchain space, these are pretty fresh.

Like, at Miden we’re using the Plonky3 library, right. I remember using Plonky2 on another project, I don’t know if this was four or five years ago, and Plonky3 was only just getting started. So think about that in the context of software and cryptography that have been out there on the internet for twenty or thirty years…

There might be bugs in the core libraries themselves, but that’s one layer of the stack. The other layer of the stack is writing the constraints of your virtual machine as constraints in the proving system. This used to be my area of expertise, but I haven’t really worked in this for the last two years. Now I’m more on the protocol side, and there could be bugs as well on that layer.

There’s a lot of layers of what you could formally verify. Without having all these guarantees, we want to make sure that we don’t lose users’ funds or our funds, and that the system is secure.

What do those precautions and “training wheels” look like in practice?

François: The way that normal software engineering and enterprise software engineering occurs in the world, in cloud deployments, is to do “canary deployments.” You slowly open the valve that flows users into your system. Partner mainnet is a way for us to do this.

We have many other aspects of Miden’s approach to deploying a private blockchain that follow the exact philosophy of making sure that we minimize the blast radius of any errors. We are timing decentralization, ramping up the decentralization over time.

Marti: Let’s start by unpacking what the training wheels mean, at least for the protocol side. The whole idea of Miden is that we have local execution of transactions, and that means the validators don’t actually have to re-execute – and this is in contrast to what basically any other blockchain does. We also have the added benefit of privacy here by the way. Or you can think of it the other way, maybe privacy is the main point, and then you actually also achieve saving the execution. Look at it the way you like, we have two birds with one stone, or whatever the saying thing is [smiles].

So you execute something locally, and then you prove the transaction. Then the validators only verify your proof. The cost of verifying a proof of a transaction is much cheaper than the cost of executing the transaction itself. OK.

So for now we have this dual system where we have the proof that the user generates, but we also have the validator re-execute the transaction in the beginning. This does mean that they’re learning the private inputs of the users, but these training wheels help us detect potential bugs in the cryptography, so they’re useful for users’ security during this phase.

So, how confident are you in Miden’s security?

François: Am I 100% sure that Miden contains zero bugs? No, I’m not.

Am I pretty sure that we have a methodology and defense in depth for addressing those bugs as they present themselves while minimizing their blast radius? Yes.

We’ve spent a lot of time looking at the entire 360 degrees of Miden, deployment of Miden and rollout. And we have plans, plural, for this.

Reports and further reading

For more detail on the audits and current privacy safeguards: