Skip to main content

2 posts tagged with "security"

View All Tags

· 7 min read
Dominik Harz

Security is hard to get right in blockchains. It's even harder to make sure that code is correct while still actively developing the product: code changes are frequent, requirements are changing, and the codebase is growing.

In this post, we'll explore options for verifying blockchain code, specifically for the Substrate blockchain framework to try to verify the code of the Interlay blockchain.

My requirements for the test were simple: the tool should be integrated into the Rust toolchain (no DSLs) and I set myself a time limit of a single day to get started and get a useful result.

Spoiler alert: I managed to get two tools running and produce output. This post covers only the setup and I will follow up with more details in a future post.

Substrate Runtimes as Verification Targets

We are building the Interlay and Kintsugi blockchains based on the Rust Substrate framework. For verifying that the "code is correct", we are looking for two targets:

  1. Runtime: The WASM runtime encodes the rules of the blockchain subject to consensus verification. This is where we can potentially introduce logical errors in how the protocols are working or in their implementation such that we either impact the safety or liveness of the system.
  2. Node Implementation: The node implementation wraps around the runtime. Bugs introduced here can impact the liveness of the system.

Diving into Verification

Software verification is most often quite an academic exercise. With the adverse environment of blockchain development, there's a clear benefit of increased security assurance in the software development process. This goes hand in hand with the desire of the verification community to integrate verification into the development process.

I'll not cover the usual testing and fuzzing tools but rather explore the three tools I found most accessible for verification in Rust.

My criteria for selecting tools were:

  1. Actively maintained: The tool should be actively maintained and have a community around it. I checked the GitHub repositories for current contributions and when the last commit was made.
  2. Clear documentation: The tool should have clear documentation on how to use it and get started. If after 10 minutes of parsing the available documentation, I could not get a good understanding of how to install or use the tool, I would not use it.
  3. Rust integration: Since the idea is to integrate the tool into the normal development workflow, I was looking for a tool that integrates well with cargo and also does not require writing verification code in a language other than Rust.

Selected Tools

From the tools I found, I selected the following three tools for further exploration:

More tools are available on the Rust Formal Methods Interest Group website and on Alastair Reid's blog.

For all tools, I installed them and ran them without any additional configuration against the chain implementation of the Interlay blockchain.

A Note on Expectations

I would be happy if a tool runs on the first try: installing the tool without issues and scanning the code base without setting up verification rules. Overall, the code is well-tested, but it is very complex: more than 1,000 dependencies, almost 100,000 lines of code, and invoking external C libraries.


From the developer's website:

Kani is an open-source verification tool that uses model checking to analyze Rust programs. Kani is particularly useful for verifying unsafe code in Rust, where many of the Rust’s usual guarantees are no longer checked by the compiler.

Getting started

I found getting started very easy with just two commands to execute:

cargo install --locked kani-verifier
cargo kani setup

Next, I ran kani against the runtime of the Interlay blockchain:

# From the interbtc repo root
cargo kani

Compilation Errors

That produced the following error during the compilation of the schnorrkel crate:

error: format argument must be a string literal
--> /home/nud3l/.cargo/registry/src/
165 | assert!(hrams.len() == public_keys.len(), ASSERT_MESSAGE);
| ^^^^^^^^^^^^^^
help: you might be missing a string literal to format with
165 | assert!(hrams.len() == public_keys.len(), "{}", ASSERT_MESSAGE);
| +++++

At this point, I wasn't sure how to convince kani to ignore these errors in the dependencies. I tried running kani only on a single crate but it resulted in the same compiler issue.

The authors have a guide on how to get started with real code but it does not include how to handle compiler errors in dependencies.


From the developer's website:

Prusti is a verification tool for Rust programs. It is based on the Rust compiler and uses the Rust type system to verify Rust programs. Prusti is a research prototype and is not yet ready for production use.

Getting started

Getting started with Prusti required downloading the Prusti Assistant VS Code extension. I already had the required Java SDk and rustup versions installed so the process of getting started only involved opening a rust file and hitting the "Verify with Prusti" button on the VS Code status bar.


As the first target, the fee pallet seemed interesting as it's mildly complex, has few dependencies, and with its fixed point math might be subject to issues.


On the first run on the fee crate, Prusti found 358 errors. That seemed quite a lot but after initial inspection, most of the errors were:

  • Unsupported features (313 errors): I was expecting Prusti with its current feature set to run into these issues as substrate makes heavy use of macros, traits, and other advanced features of Rust.
  • Internal errors (24 errors): Several internal errors occured.
  • Unexpected verification error (9 errors): Some verification failed.
  • Verification errors (14 errors): These seem to be the ones worth investigating.


Prusti found potential overflow and underflow errors in the bitcoin crate:

// bitcoin/src/
if position + 4 > raw_bytes.len() {
return Err(Error::EndOfFile);

It also found possible issues with unbounded arrays:

// bitcoin/src/
pub fn op_return(return_content: &[u8]) -> Script {
let mut script = Script::new();
script.append(return_content.len() as u8);


From the developer's website:

MIRAI is an abstract interpreter for the Rust compiler's mid-level intermediate representation (MIR). It is intended to become a widely used static analysis tool for Rust.

Getting started

Installation of MIRAI was straightforward, following the guide:

git clone
cargo install --locked --path ./checker

Next, I ran MIRAI in the interbtc root directory.

cargo mirai

Compilation Errors

MIRAI produces compilation errors on the wasm builds:

     Compiling wasm-test v1.0.0 (/tmp/.tmpfNz4QS)
error[E0463]: can't find crate for `std`
= note: the `wasm32-unknown-unknown` target may not be installed
= help: consider downloading the target with `rustup target add wasm32-unknown-unknown`
= help: consider building the standard library from source with `cargo build -Zbuild-std`

error: requires `sized` lang_item

For more information about this error, try `rustc --explain E0463`.
error: could not compile `wasm-test` due to 2 previous errors
warning: build failed, waiting for other jobs to finish...
error: cannot find macro `println` in this scope
--> src/
3 | println!("{}", env!("RUSTC_VERSION"));
| ^^^^^^^

error: could not compile `wasm-test` due to 3 previous errors


As the wasm build is done on the entire runtime, I decided to try my luck against a single pallet instead. Similar to before, I tried the fee crate. This worked and to my surprise, MIRAI did not print any warnings or errors.

Next, I tried the bitcoin create that implements parsing and other somewhat error prone code. MIRAI gave me results here:

warning: possible attempt to subtract with overflow
--> crates/bitcoin/src/
239 | let target: U256 = parser.parse()?;
| ^^^^^^^^^^^^^^
note: related location
--> crates/bitcoin/src/
177 | let (result, bytes_consumed) = T::parse(&self.raw_bytes, self.position)?;
| ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
note: related location
--> crates/bitcoin/src/
151 | let compact = U256::set_compact(bits).ok_or(Error::InvalidCompact)?;
| ^^^^^^^^^^^^^^^^^^^^^^^
note: related location
--> crates/bitcoin/src/
53 | word << 8 * (size - 3)
| ^^^^^^^^^^


Overall, I was very happy with the results. I was able to run two tools against the crates without additional configuration and they found potential issues. Next up will be trying to implement custom verification rules and dive deeper into the identified issues.

· 9 min read
Dominik Harz

Or why Oracle Vulnerabilities are not the Worst Application of Flash Loans.


  • You can potentially steal all of Maker’s collateral ($700m) and issue arbitrary amounts of new Dai using flash loans if no delay for new governance contracts is introduced.
  • Anyone can execute the attack and only needs to pay the transaction fees (few $) without holding any MKR.
  • If Maker does not introduce a delay until the liquidity pools for flash loan pools gets above a threshold, there is little chance to prevent the attack (race condition).
  • We have reached out to Maker February 8, 2020 about our research and had a call with them on February 14, 2020 to discuss our findings. Maker is aware of the attack vector and is holding a vote this Friday 12pm PST that would prevent the attack.


Maker and its Dai stablecoin is the most popular so-called decentralized finance (DeFi) project on Ethereum with around of $700m locked in its smart contracts. The Maker protocol relies on a governance process encoded in a smart contract. MKR token holders can vote to replace an existing governance contract. Votes are proportional to the amount of MKR. The total number of MKR tokens is around 987,530 where selected wallets or contracts hold large quantities of the token:

  • [Maker Governance Contract: 192,910 MKR]
  • Maker Foundation: 117,993 MKR
  • a16z: 60,000 MKR
  • 0xfc7e22c6afa3ebb723bdde26d6ab3783aab9726b: 51,291 MKR
  • 0x000be27f560fef0253cac4da8411611184356549: 39,645 MKR

Note: the Maker Governance Contract contains MKR tokens of multiple parties.

Governance Attack

In a post from December 2019, Micah Zoltu pointed out how to attack the Maker governance contract. The basic idea is to accumulate enough MKR tokens to replace the existing governance contract with the attackers, malicious, governance contract. The malicious governance contract is then able to give the attacker full control over the system and withdraw any collateral in the system as well as create arbitrary amounts of new Dai.

To reduce the number of required MKR tokens, he proposed to execute the attack when new governance contracts are being voted on. At the moment, 192,910 MKR tokens are locked in the governance contract. However, an attacker would need less tokens if, say two or three contracts, would be voted on in parallel with similar token distributions. This frequently happened in the past as we can observe in the graph below:

The obvious attack strategy would be to crowd-fund the required MKR tokens through a smart contract and pay each attacker a share of the of the winnings. However, the attackers need to amass probably around 50k MKR tokens to have a chance to attack the system without Maker noticing these movements. We do show a strategy for this in our latest paper.

A Brave New Attack Strategy: Flash Loans

However, we can completely lift the requirement to amass MKR tokens if we consider using flash loans instead. Flash loans are a fairly new concept and therefore we give a brief explanation here. Normally, an agent has to provide collateral to take out a loan in the DeFi space. For example, in Maker, Alice can borrow Dai by depositing ETH. This is required since we operate under a model of weak identities and economically rational agents.

A flash loan lifts this requirement as it only takes place in a single transaction:

  1. Alice takes out the loan from a flash loan liquidity provider (e.g. Aave or dYdX)
  2. Alice executes some actions (e.g. arbitrage trading on Uniswap, Fulcrum, Kyber etc.)
  3. Alice pays back the flash loan with interest

A flash loan works in three steps within a single transaction.

The flash loan works because of how the Ethereum Virtual Machine is designed: if at any point during this transaction the flash loan fails, the whole transaction is reverted. Hence, Alice can take the loan risk free, i.e. if she cannot pay it back it would be like she would have never taken it. The liquidity providers are also winning: they have only lent their funds if Alice was able to pay them back.

Arbitrage and Oracle Manipulation with Flash Loans

On February 14 and February 18, two incidents involving flash loans occurred that caused bZx to halt its platform. In the first transaction, a single flash loan was able to make a profit of 1,193 ETH (approx. $298,250). This transaction was executed using a smart contract that opened a short position on Fulcrum on wBTC. In the same transaction, the transaction took out a wBTC loan on Compound and executed a trade of wBTC on Kyber’s Uniswap reserve resulting in slippage ultimately bringing down the price on Fulcrum as well. The full details can be found in the post-mortem by bZx and a detailed analysis of the involved calls by PeckShield.

Similarly, a second incident occurred on February 18 where in a single transaction a profit of 2,378 ETH (approx. $600,000) was made. This transaction involved an initial borrowing of 7,500 ETH to take a long position on Synthetix' sUSD. More details are found in this informal analysis.

Oracle Manipulation to Reduce Required Liquidity

For our attack, we assume that 50k MKR are sufficient. Even if in practice the number of tokens could be higher, we point out how the concept of flash loans makes securing Maker, without a governance delay, hard. In a naive approach, the attacker could take out a flash loan to buy 50k MKR tokens.

At current exchange rates, the attacker needs around 485,000 ETH to buy that amount of MKR as only a single exchange, Kyber, has enough volume available. However, the attacker can also leverage multiple exchanges and buy 38k MKR from Kyber, 11.5k from Uniswap, and 500 MKR from Switcheo for a total of 378,940 ETH. That number is still high but already a reduction by almost 100,000 ETH!

An attacker can use the oracle manipulation strategies above to effectively bring down the price of MKR on Kyber and Uniswap. These are the two largest providers of MKR and have shown to be vulnerable to oracle price manipulation. Further analysis is required to determine how much the MKR price can be reduced. However, on a less liquid token like wBTC an attacker was able manipulate the exchange rate by around 285%.

Obtaining enough Liquidity


Even with oracle manipulation, a large number of ETH is required to execute the attack on Maker. However, an attacker can increase its liquidity by taking out two flash loans within the same transaction. Aave and dYdX protect themselves against reentrancy and allow only a single flash loan within a single transaction. But the attacker can borrow ETH from both protocols within the same transaction.

Thus, as of February 18, the attacker has a pool of around 90k ETH on dYdX plus 17k ETH on Aave available. Hence, at current liquidity rates an attacker could take out a combined ~107k ETH loan from both dYdX and Aave to try to manipulate the MKR token price and obtain enough MKR tokens to replace the current Maker governance contract with its own.

For this to succeed the attacker must be able to reduce average MKR price by at least 3.54 times. Alternatively, the attacker can also wait for dYdX and Aave to increase its liquidity pools. With the current growth rate of around 5% of both protocols, it does not seem unlikely that the attack becomes possible within two months.


Obviously, it is possible to combine the crowd funding approach and the flash loan together. Using the available liquidity of ~107k ETH, it is possible to obtain around 10,800 MKR from Kyber. This would allow multiple attackers to reduce the required amount of pooling together 50k MKR to just around 39.2k MKR. It seems also that some people are indeed interested in such an attack as this informal Twitter poll shows:

It can also be noted that the top four account holders (in fact five, but not considering the current Maker Governance Contract) are able to execute the attack without crowdfunding.

No Time to Wait

Once enough liquidity is available through the flash loan lending pools (with or without the combination of using oracle manipulation), anyone is able to take over the Maker governance contract. Once Maker starts a vote when the liquidity pools have reached that threshold, Maker needs to ensure that MKR tokens are as little distributed as possible. If the distribution of MKR at any point in this voting procedure allows for an exploit of the vulnerability, any collateral can be taken away.

That attacker would be able to steal $700m worth of ETH collateral and be able to print new Dai at will. This attack would spread throughout the whole DeFi space as Dai is used as backing collateral in other protocols. Further, the attacker can use his Dai to trade other currencies worth around $230m. We give a more detailed analysis in our paper.

Counter measure

Maker should put a new governance contract in place that prevents flash loans from attacking their system. Specifically, a new governance contract should be able to be checked by the Maker Foundation for malicious code and give enough time to react. At the bare minimum, a new governance contract should not be able to go live within a single transaction. That way, the attacker can likely not profit from the attack and thus not repay the flash loan. If the attacker cannot repay the flash loan, the attack is like it would have never happened.

Maker is putting such a contract to vote on Friday, 12pm PST, February 21, 2020. The proposed contract would activate the Governance Security Module (GSM) and prevent such a flash loan attack.