Form and function

IOHK is building Cardano into a global financial and social operating system. This enormous task requires both quick iteration and absolute precision. It is why IOHK has chosen to combine the speed of agile development with high assurance code and formal methods. Fusing flexibility and formality led our engineers to pioneer this modern development philosophy.

IOHK believes firmly in research, formal methods, functional programming, and building in a rigorous manner. As a competitor in the blockchain development industry, we also have to consistently demonstrate progress and create value for our global community of stakeholders. This means we can’t compromise on robustness or on development speed and flexibility. In an ever-changing marketplace this is a challenge, so our developers have to strike a balance.

Agility versus formality

The start-up standard for developing technology has been to build a minimum viable product quickly and then continually iterate until it is ready for the mass market. This is known as an agile process. It is a great way of showing that a project is advancing while eventually building a fully functional product. However, an agile methodology assumes there will be bugs and weaknesses in each step of development that can be ironed out later. This is fine if there is no value at risk – but, with virtual currencies, there is an enormous amount of money and stakeholder trust on the line.

Building a digital asset on a blockchain provides several challenges to overcome in terms of organizing a development process. As a proof-of-stake cryptocurrency, Cardano is a distributed system in an adversarial environment where consistent performance is critical. The protocol has to maintain security in the face of malicious actors attempting sabotage. This means that no one can afford to build quickly and deal with problems later.

Trust is essential for a currency to be accepted and correctness proofs are an important way to increase the veracity of a system. This is why the code should not only be correct, but there should be evidence of its correctness, such as extensive meaningful tests and mathematical proofs. In a young industry like cryptocurrencies, IOHK engineers have to anticipate the addition of new features while maintaining the correctness guarantees established in the initial version. The platform can only scale globally if it is able to grow while maintaining security and utility for everyone. This is why Cardano developers streamlined their methodology, combining a variety of tools ranging from property-based testing all the way to machine verifiable proofs, to create high assurance software even in the presence of changing requirements.

Research to code

The methodology begins with scientific research. To date, IOHK has released more than 60 research papers that have contributed to creating the platform. Each paper examines a critical aspect of blockchain technology from first principles. How do we gain consensus in a decentralized way? How is a smart contract designed? What is the right reward structure to incentivize good behavior? IOHK researchers examine these questions, and submit their answers to scientific journals and conferences. These papers contain proofs that must pass rigorous peer review. Then, to ensure that the quality of our software does justice to the science, it is developed using formal methods.

In essence, this means that IOHK engineers specify what the code should do mathematically. That way, they can ensure that when the code is run, it contains the desired properties designed into it. The code is written in Haskell, a high-assurance functional programming language with a strong type system. While Haskell is a great tool for implementing reliable software, it is not foolproof, so the code still needs to be tested. A great way to write tests is using QuickCheck, which allows developers to state properties that should always hold in a program. QuickCheck then generates test cases, and searches for minimal counterexamples that violate those properties.

In code that interacts with the external world, in particular network applications, it can be hard to find minimal counterexamples. This is because the order of execution is not deterministic: it can change every time the software is run. The same code can be run hundreds of times, and only fail once. We can get around this by using simulations with deterministic execution order. Running tests in simulation allows us to reliably find and fix a class of bugs in testing, which would otherwise only occur randomly in production.

Bridging the gap

To get a picture of the development methodology employed for Cardano, let’s consider the metaphor of bridge building. When a civil engineer builds a bridge, a large portion of their time is spent behind a desk. The civil engineer plans a design, calculates the statics, and orders geographic surveys. During that time, nothing happens at the building site. An observer would be unable to see any progress being made. For building bridges, this is the correct approach. If the planning is not accurate, it is difficult and expensive to correct problems at a later stage. Ultimately, the result would be a delayed bridge at a higher cost, or one which fails completely. Lack of visible progress is a good price to pay for a functional and safe bridge.

When building software, making changes in later stages is much easier than in construction. That is what enables the common agile development approach. If an agile developer was building a bridge, they would construct a pillar in one rapid sprint and then the next in a second sprint. The gap between the pillars would be spanned in a final sprint and, if things didn’t hold up, the developers would add on one more sprint to fix any issues. While progress would be demonstrable at the building site, the final product would likely have a great deal of problems built into it. This creates clean up work at the end of the project which could have been avoided by better planning at an earlier stage. Furthermore, the minimum viable product would likely be given to a small group of people for a test drive with the expectation that it would fail in order to alert developers of bugs. Needless to say, it is best that bridges aren’t designed in this way.

When hearing the words 'formal methods’, a lot of people in software development think about the civil engineering approach, which is dubbed ‘waterfall’ and generally shunned. This is a common but unfortunate misunderstanding. Indeed, using appropriate formal techniques allows us to have our cake, and eat it too: to have an overall design (a deliberate design, not an accidental one from fitting together pieces developed in sprints), to show progress continuously, and to retain the ability to react to changing requirements.

A key technique employed by IOHK developers is executable specifications. These are high level designs, which abstract over low level details, written in a language that the computer can understand and execute. Executable specifications can be used as prototypes to show progress, get feedback from users, and test assumptions. On top of that, lower level details can be added via successive refinements. Our developers build the bridge to solve the biggest problems first then add pillars to reinforce it at a later time. In a software system, the pillars would be features like saving data to disk, or using performant algorithms, which are needed for a final product, but which are not essential to demonstrate the overall functionality.

Using executable specifications, we get the benefits of proper planning without sacrificing flexibility. IOHK developers can fix what the system should look like on a large scale, and then implement suitable components as needed. Continuous testing guarantees that each component fits the overall design. This helps prevent problems that are common in a late integration approach. With this methodology, we get the best of both worlds: we can use a top-down design (avoiding late integration troubles, having a good handle on the overall design at all times), and have working code early (demonstrating progress, and allowing for tests and feedback through the whole process).

Future proof

Ultimately, the method of construction should be determined by what is being built. IOHK is building a global social and financial operating system which requires rigor and speed. Formal versus agile is a false dichotomy. Instead, we’re continuing to develop our methodology which fuses the best of both approaches: formal techniques within an agile delivery framework, with robust, higher assurance code upon which we can build for all our futures.

The goal of the Cardano Shelley era is to bring full decentralization to Cardano, moving beyond the federated epoch and handing control of the ledger over to the community via stake pools.  As part of the process of delivering Shelley, we create formal specifications which allow us to verify that the final code is in line with what the researchers initially envisaged in their publications. By creating implementation-independent specifications, we can build components of the system using different languages, confident that they will work together.

We are pleased to announce that we have successfully reached an important milestone in the Shelley journey, with the key specifications now completed. The finished specifications are as follows:

To provide a smooth transition from the Byron era to the Shelley era, the Shelley code will have to be compatible with the Byron rules. To enable this, we have created specifications for the Byron era as well:

The process of implementing these specifications in production code is well underway, and the specifications will continue to improve with feedback from the mathematics, research, and development communities.

For the most up to date version of the specifications, check the Formal Models for Ledger Rules GitHub repository.

Artwork,

Mike Beeple

Ada is not among the 26 cryptocurrencies identified by US researchers last week as being vulnerable to ‘fake stake’ attacks.

1

The Cardano blockchain underlying Ada is based on proof-of-stake (PoS), but its Ouroboros protocol uses no bitcoin code and is not affected by the PoSv3 problem.

2

This is not just good luck, but a consequence of the thorough, formally-verified approach taken during Cardano’s development.

The vulnerability

The vulnerability is explained very well in the original article. In order to understand why Cardano is not affected by it, we will summarise the essence of the vulnerability here.

All the vulnerable systems are using PoSv3, a modification of the bitcoin code that aims to replace hashing power with stake for the purpose of determining who is eligible to create a block. In the original bitcoin code, the decision of who gets to create the next block is based purely on hashing power: whoever manages to find a suitable random number, and thus get a correct hash first, wins. PoSv3, however, adds an additional variable, to simulate the notion of stake.

In a PoS system, the likelihood of getting to create a block is proportional to how much stake a user has in the system: the more stake a user has, the more likely it is that they get to create the next block. To mimic this functionality, PoSv3 allows users to add additional information to their candidate block, in the form of a ‘staking transaction’. The more tokens they have available to use in their staking transaction, the easier it becomes for them to get a correct hash, and thus earn the right to create the next block.

Whilst PoSv3 does successfully tie block creation rights to stake in this way, it also makes block validation more difficult. Not only does the hash of the block itself need to be verified (as in bitcoin), but so does a user’s staking transaction: that is, did the user actually own the tokens they used in their staking transaction? To verify this information, a blockchain node has to be able to refer to the ledger, and – if a block does not simply extend the current chain but introduces a fork – also the history of the ledger. Since that is neither cached nor cheap to calculate, blocks in PoSv3 systems are not validated immediately, but are rather (at least partially) stored in memory or on disk when they pass some heuristics.

The vulnerabilities discussed in the original article can be exploited in a number of ways, but ultimately involve fooling those heuristics and presenting lots of invalid blocks to a node, such that the node runs out of memory and crashes before it can correctly identify that the blocks are invalid.

Why Cardano is different

For Cardano, IOHK took a different approach. Instead of finding a minimal variation of bitcoin, we relied on world-leading academics and researchers to create a new protocol and codebase from scratch, with the requirement that it should provide equivalent (or better) security guarantees than bitcoin, but rely entirely on stake. The result is the Ouroboros protocol

3

, the first provably secure PoS protocol, upon which Cardano is built.

The basic design of Ouroboros is remarkably simple: time is divided into discrete increments, called slots, and slots are grouped into longer periods, called epochs. At the start of each epoch, a lottery determines who gets to create a block for every slot. Instead of this lottery being implicit, ie whoever gets a right hash first wins, the lottery is explicit: a generated random number determines a slot leader for each slot, and the chances of winning for any given slot are proportional to the stake one controls

4

.

In this protocol, validating that a block has been signed by the right stakeholder is also simple: it requires only the leader schedule for the current epoch (which will not change in case of a temporary fork), and the checking of a signature. This can and will be done by each node once they get the block header, in contrast to the PoSv3 systems that are vulnerable to fake stake attacks.

In short: Cardano is secure against fake stake attacks because it’s based on a fundamentally different system. PoSv3 cryptocurrencies run on proof-of-work (PoW) systems, modified to take stake into account in the implicit leader election, and the vulnerability in question is a result of that modification, and the additional complexities it involves.

Not only does Cardano have a fundamentally different foundation, but that foundation is the result of multiple peer-reviewed academic papers, and an unprecedented collaboration between researchers and developers. The formal and semi-formal methods involved in creating the upcoming Shelley release of Cardano ensure that its construction at code level evidently matches the protocol described in the peer-reviewed research papers, building in reliability and security by design – and avoiding the problems of PoSv3, which have arisen as a result of modifying an existing protocol instead of creating a thoroughly proven, bespoke protocol like Ouroboros.

Footnotes

1. ‘“Fake Stake” attacks on chain-based Proof-of-Stake cryptocurrencies’ by Sanket Kanjalkar, Yunqi Li, Yuguang Chen, Joseph Kuo, and Andrew Miller of the Decentralized Systems Lab at the University of Illinois at Urbana-Champaign.↩

2. To be precise, the following discussion is targeted at the upcoming Shelley release of Cardano. The currently deployed Byron release is running in a federated setting, and thereby operationally protected from this kind of attack anyway.↩

3. There are by now a number of variations of the Ouroboros protocol. We describe only the classic version of Ouroboros here, but the general argument holds for all variants – in particular for Ouroboros Praos, which will be the protocol used in the Shelley release.↩

4. To be precise, leader election for a given epoch uses the stake distribution at a point in time before the epoch starts, to prevent grinding attacks and a re-calculation of the schedule in case of a temporary fork at the epoch boundary.↩

Artwork,

Edan Kwan