Property testing a software update mechanism

blog
One of the work-packages of Priviledge has to do with the development of a decentralized update mechanism for Cardano. Within this project we are developing a prototype that aims at satisfying the requirements outlined in our previous blog post. Given the central role that the update mechanism plays in the life of a blockchain system, we are investing a considerable amount of effort to test it. In this article we give an overview of how we test the implementation of an Update mechanism for Cardano.

The ledger layer

The implementation of Cardano consists of three main components: network, consensus, and ledger. The network layer takes care of communication with other peers in the network, it sends and receives blocks to and from the consensus layer. The consensus layer runs the consensus algorithm: it determines which chain to follow (thereby resolving any potential forks), which blocks are valid, when to change the protocol version, etc. The consensus layer relies on the ledger layer to determine the validity of the transactions inside a block, and to determine when updates will take place. Thus, the ledger layer lies at the core of the blockchain protocol.

A thoroughly tested ledger layer reduces the chances of errors and catastrophic bugs in the blockchain implementation. Properties such as absence of double spending or rejection of malicious updates have to be ensured by the ledger. Furthermore, whatever safety property we validate at the ledger level we can extrapolate to the blockchain protocol since it relies on the ledger layer for transaction validation.

Testing the ledger layer

The Cardano ledger interface consists of pure functions, which are of the form:

Ledger State -> Transaction -> Either Error (Ledger State)

This is: given a ledger state and a transaction, a ledger function validates the transaction in the given state and either returns an error if the transaction is invalid, or returns the state that results from applying that transaction to the input state.

Unit testing is the most common way of validating software. It lacks the thoroughness of a mathematical proof and only covers a couple of cases, but they are quite fast and easy to write. A limitation of unit testing is not only that they cover only a few cases, but these cases are further limited by the test writers’ ability to invent test scenarios.

Property based testing on the other hand delegates the creation of test cases to a data generation algorithm: the tester defines by means of a random generation algorithm the space of input data, and properties that the system under test has to satisfy. Then, the testing framework takes care of feeding these randomly generated input data to the system under test and checks that the aforementioned properties hold.

A quintessential example of a property test is the following one:

prop_reverse xs = reverse (reverse xs) == xs
This property can be read as: “for all lists, reversing a list twice should yield the same list”.

When given a property such as the above, a property based testing library such as QuickCheck will generate random lists, and check whether the property is true for these generated lists.

If a property does not hold for a given input, it will be shrunk. Shrinking is important because once the property tests discover an error, it is important that we are provided with a minimal counterexample. In this way, we can easily pinpoint and fix the error.

Property-based testing requires more effort than unit testing, but considerably less effort than a formal proof. One still has to write properties, generators and shrink functions, but no formal proof is involved and the additional effort invested is compensated by the substantial increase in test cases coverage.

Property testing the ledger layer has additional challenges: we cannot express a property for a ledger update function, say ledgerUpdate, in the same way as we did for reverse. Firstly, we cannot generate a random input state since most states will be invalid. Secondly, to be able to test aspects such as approval of proposals we need multiple transactions (as opposed to a single input).

Instead of generating random individual inputs, we need to generate random sequences of events (transactions) and ensuing states. We call such sequences traces.

At the formal-methods group in IOHK we started exploring techniques for writing trace generators. As part of the Priviledge research effort we are working in improving these techniques so that:

  • trace generators are easier to write,  

  • trace generators are more efficient,

  • trace input space is easier to classify,

  • properties are easier to express.


Once we are able to generate traces, we can readily express important ledger properties such as the absence of double spending.

prop_noDoubleSpending trace = allUnique (inputs trace)

In the property above, inputs returns the list of inputs seen in a trace, and allUnique returns true if and only if all the elements of the list are unique.

As another example, the property that only honest versions are approved can be expressed as:

 prop_onlyHonest trace = 
   protocolVersionsSet trace `disjoint` maliciousVersions (testSetup trace)

In the property above protocolVersionsSet returns the protocol versions that were adopted in the trace, and maliciousVersions returns the set of malicious versions in the test setup (which should be rejected).

As we have seen, ledger properties are relatively easy to write, and are automatically checked. But there is no free lunch. The key to good property based testing of ledger properties is a good coverage of the trace space. This is not to say that we must cover as many traces as possible, but that we must identify important classes of behaviors and make sure we generate elements of each class. For instance, if we are generating transactions for the no-double spending property above, we want to make sure that we try to spend the same input more than once. In the development property tests for Cardano, as well as in the new update mechanism, we have also invested a considerable amount of effort in ensuring a proper coverage of our generated input data.

Next steps

Property-based testing is an excellent complement to traditional unit testing, which allows to discover errors that would have otherwise made it to the deployed code. The ledger layer of a blockchain requires a more sophisticated form of property based testing, where test setups and traces of events are generated. We hope the ideas being developed by IOResearch regarding property-based testing will be a useful contribution to the development of high quality ledgers, but also a contribution to the state of the art in testing and high-assurance software development. In the coming months we will have completed the first batch of property tests for the Cardano update prototype, and we are looking forward to sharing our results with you, so stay tuned!


Written by Damian Nadales Agut, IOResearch