Smart contracts are critical programs running on a blockchain. Tweag’s High Assurance Software Group has become a well-known and trusted actor in the Cardano blockchain ecosystem when it comes to auditing and improving the reliability of these products. Let me guide you through our auditing process, how we improved upon classic testing techniques, and where we’d like to go next with formal methods.

The fictional company FooCorp is planning to provide a service AwesomeFoo to its clients through the deployment of a smart contract on the Cardano blockchain. For the sake of this blog post, they asked us to audit it.

What is AwesomeFoo exactly?

Just like you and me, Alice and Bob have an account at their local bank. What they possess there is described by a single number: the balance. When they spend or receive money, this balance is updated accordingly. Some blockchains (such as Ethereum) have a similar concept of account and balance but Alice and Bob are also regular users of the Cardano blockchain which follows another design. Instead of accounts, Alice and Bob each own a wallet containing objects called UTxOs (Unspent Transaction Outputs). A UTxO is like a one-use banknote or coupon: it has a value, and you can spend it once. Spending it allows you to create new UTxOs with values and owners of your choice, as long as it adds up to the value spent.

Let’s look at an example. Consider the UTxOs in black in the following diagram:

Alice has two UTxOs: one with 10 Ada (the currency on the Cardano blockchain) and another with 5. She wants to pay 12 Ada to Bob. No UTxO has that exact value so she submits a transaction request (in blue) in which she spends her two UTxOs (15 Ada in total) and creates a 12 Ada one that goes in Bob’s wallet, and a 3 Ada one (the remainder) to herself. The green transaction from Bob is another example. This is how value is exchanged with no need for the concept of centralized accounts.

The diagram shows transaction requests that have been accepted on the chain, but some requests can be rejected if they don’t follow the rules:

• Rule #1: The total input and output value must match¹.
• Rule #2: If a UTxO from a wallet is spent, the owner of the wallet must sign the transaction request.

Some UTxOs don’t belong to individuals like Alice and Bob, but are associated to programs instead. When you submit a transaction request in which you spend such a UTxO, the associated program is executed. It is a pure function that returns a boolean. Given the context of the transaction (inputs, outputs, signers, etc.), it says whether spending the UTxO is allowed (True) or not (False).

• Rule #3: If a UTxO associated to a program is spent, the program must return True given the context of the transaction request as parameters.

The AwesomeFoo smart contract is a collection of such programs. Smart contracts are autonomous and make it possible to run complex services and protocols on the chain such as distributed exchanges (DEX), stable coins (e.g. Djed), crowdfunding, auctions, staking, etc.

Why is FooCorp right to ask for an audit?

• High risks
  • No updates. As you noticed on the diagram, each UTxO on the chain has an address. For wallet UTxOs, it is a key belonging to the owner. For programs, it is the hash of the program. This means that updating the program changes the address but all existing UTxOs are still associated to the previous address. These will go through the old version when spent. It is only possible to migrate, not update. Therefore, it is crucial to get the product right from the start.
  • Distributed design. In complex smart contracts, users craft transaction requests in which multiple UTxOs, sometimes belonging to different programs, are spent at the same time to achieve some result. In such cases, every individual program has to be designed with that collective result and the other programs in mind. Design and implementation are prone to many hard to detect errors, as in distributed or concurrent programming.
• High stakes. In case of unexpected behavior, bugs, or attacks exploiting vulnerabilities in the product, FooCorp and its clients could suffer from major and unrecoverable financial losses.
• Testing is limited. An audit has a fair chance to spot specification or design flaws which no amount of testing can identify. Besides, an external pair of eyes is likely to catch issues FooCorp may have missed in internal tests.

We help FooCorp by uncovering vulnerabilities, bugs, weaknesses, specification issues, design flaws, and wastes of space/time in their smart contract. We also suggest mitigations when applicable.

In the High Assurance Software Group, we have audited around a dozen Cardano smart contracts, a few of them twice when the client wished for a second audit. In around 75% of our audits, we found at least one concern that would expose parties of the smart contract to risks of abuse (e.g. weaknesses or direct exploits to steal money).

The audit begins

FooCorp has just provided us with:

• The specification documents of AwesomeFoo including high level requirements, use cases, examples, and diagrams.
• The implementation in Haskell of the programs comprising the AwesomeFoo smart contract.

In a few weeks, we are expected to deliver:

• The audit report listing our concerns and suggestions sorted by type (unclear specifications, bugs, vulnerabilities/exploits, code quality, optimization) and ranked by severity (from critical to very low).
• The audit code: an audit-oriented API using our homemade framework to interact with AwesomeFoo along with all the scenarios we tried, which FooCorp can use as regression tests or expand/tinker with if they want.

First look at AwesomeFoo

First, we need to really understand what AwesomeFoo is about, so we study the specs and skim through the code.

New finding. We quickly notice an unclear item in the documentation: it states that users of AwesomeFoo can’t perform some action after a deadline but it doesn’t say if the validity interval includes the deadline, nor what’s to become of any unspent deposit once the deadline has elapsed. The code tells us what happens, but not what’s intended to happen.

We simply ask the engineers at FooCorp about it! The auditing process involves a continuous dialogue: we inform them of every important discovery or question as we study their product. Here, they help us clarify the above item but we will log it in our report anyway and suggest an improvement.

Simple tests

In the industry, audits often consist of a manual inspection of specs and code. At Tweag, we go way beyond that. We have been continuously developing and improving our homemade auditing toolbox, cooked-validators, in parallel with our audits. It lets us interface with smart contracts to experiment with test scenarios. According to many of our clients who joined our user base, cooked-validators is easier and more efficient at that task than existing libraries.

A test has a sequence of transaction requests that are submitted one by one to a simulated blockchain, which either accepts or rejects them. The test specifies the expected outcome.

To write such tests, we need to design transaction requests. We use cooked-validators to create an API to build requests that correspond to meaningful AwesomeFoo interactions. We don’t reuse FooCorp’s API because:

• It is written with the end user in mind. It ensures transaction requests are well-formed from the start and fit the expectations of the smart contract, whereas we want to craft weird and unexpected transactions to find undesired outcomes. We write a more flexible API to that end and use our experience from previous audits.
• Writing our own API brings us an in-depth understanding of AwesomeFoo, after the overview we get from the specification and skimming through the code.

Once we’re done with the API, we warm up with a few unit test cases covering common usage scenarios. We also test a few properties using property-based checking².

New finding. An implementation bug escaped FooCorp’s test suite: a utility function that generates supposedly-unique identifiers actually loops back at some point on existing ones. For now, AwesomeFoo has an undocumented implicit limit on the amount of resources using the identifiers so the issue is dormant. We report it to FooCorp immediately and explain how it may become critical if they ever increase this limit.

At this stage, our audit may look like a glorified API and test suite. Actually, this test suite is ammunition for the secret weapons hidden in cooked-validators.

The trace modification framework

Remember the structure of a test case:

Each test case has a sequence of transaction requests, the trace, detailing a scenario. cooked-validators provides a powerful framework to modify, generate, and combine transaction requests and traces. If you are interested in the technical details, refer to our previous posts: Part 1 presents the underlying trace abstraction that uses a freer monad, and Part 2 the LTL³-based language used to specify modifications. A library of ready-to-use higher-level modifiers, which we are about to detail next, is built on top of this lower level framework. The idea is to derive lots of new meaningful test scenarios from existing ones, with little effort.

Tweaks

Tweaks are functions to modify transaction requests (add, delete, change):

You can combine them to easily create a new trace from another. They make it possible to punctually explore outside the space of what the base AwesomeFoo API can produce, without having to manually expand or generalize said API. This makes it extremely convenient to think out of the box and quickly implement many new ideas.

In the above, we modify a test scenario into another in which Bob tries to create the necessary conditions to steal money. This scenario is expected to fail. Thankfully for FooCorp, it does.

We use tweaks to expand coverage of our unit test suite.

Automated attacks: find targets and apply tweaks on a large scale

We know a bunch of common vulnerabilities in smart contracts. We often want to attempt attacks that exploit them without a specific setup in mind. Manually writing new traces is tedious and likely to miss specific conditions in which an attack is successful. To maximize our chances of finding a setup where the attack works, we try it on all the test scenarios we have so far. Our framework makes it possible to target locations in traces to apply the required modifications with tweaks.

Automated attacks can produce several new test cases from a single one such as in the following example.

Then, we can automatically attempt common attacks on all our previous scenarios, turning dozens of test cases into hundreds of meaningful test cases.

New finding. The automated attack reveals a vulnerability in AwesomeFoo. It is actually due to a typo in a function that checks whether two values are equal. One case has been forgotten by FooCorp. Neither manual code inspection nor tests carried out by FooCorp and us in the early stages of the audit had detected it.

Our experience with other techniques

• Unit testing: writing individual tests is tedious and likely to miss interesting cases. The tweaks make it possible to write additional tests extremely easily by slightly changing previous test cases, going out of the box, and the automated attacks considerably increase coverage afterwards.
• Model checking is exhaustive. All of the (finite) input space is tested. We explored that path before but it was impossible to verify interesting properties on smart contracts in a reasonable time without reducing the state space to some trivially small and irrelevant subset.
• Property-based checking compromises by only considering randomly generated inputs. Writing good generators for these inputs is hard. By applying our automated attacks to existing meaningful traces (including manually tweaked traces), we cover inputs that are naturally more likely to yield interesting results compared to random distributions.

The following diagrams illustrate how the different techniques differ in terms of coverage.

Looking ahead: towards formal verification

As we told FooCorp, no audit is guaranteed to catch all bugs and vulnerabilities. Our auditing process is constantly evolving. Although we have improved upon existing testing techniques, we would ideally like to formally verify (demonstrate mathematically) that the implementation of a smart contract fits its specifications. Part of our research activity is dedicated to the use of formal methods in the pursuit of this goal. In particular, we’re developing Pirouette, a language-agnostic functional symbolic evaluation engine with a backend for smart contracts on Cardano. We’re also working on using LiquidHaskell, which uses refinement types and SMT solvers, to prove properties on smart contracts.