A magnificent view across the Black Sea from a sunny rooftop terrace in Odessa – it’s hard to imagine a more beautiful location for a blockchain conference. Guests and speakers from more than 20 countries were at the fifth Blockchain Incredible Party, BIP001, a leading cryptocurrency and blockchain event in eastern Europe. The event started only two years ago but has already built up a following who keep coming back for the friendly atmosphere, line up of international speakers and emphasis on social events put together with a hospitable touch.

Lilia Vershinina and Pavel Kravchenko, the organisers and founders, say Ukraine is fertile ground for blockchain start-ups because there is funding, a pool of talented developers and a general appetite for new business ideas. "There are a lot of people trying to experiment, and they are not afraid," said Pavel.

The event aims to showcase the Ukrainian scene and strengthen ties between blockchain advocates in Ukraine and the west, he says, pointing out that they are a long way from Silicon Valley. Another goal is providing education for the enthusiastic and fast-growing Ukrainian blockchain community. Speakers at the sold out conference included Vlad Zamfir, developer at Ethereum, Giacomo Zucco, CEO at BlockchainLAB, Rob Viglione, co-founder of ZenCash, and Pavel Kravchenko, co-founder at DistributedLab.

Charles Hoskinson, CEO of IOHK, took to the stage to talk about the biggest challenge that he sees facing cryptocurrencies.

He drew a sobering comparison between what he said was a current cryptocurrency bubble, and the early period of the 20th century. Tracing an arc from the Knickbocker crisis of 1907, when a three-week financial panic crashed the US stock market, to the founding of the Securities Exchange Commission in 1934, Charles charted the excesses of capitalism that ravaged the economy during those years. From insider trading scandals to the novice investors who ploughed their savings into badly judged investments, the financial turmoil of that era took the US to the verge of bankruptcy and triggered the Great Depression.

Comparing then to now, Charles said: "We are in a bubble and there will be a collapse. A lot of businesses will wash away; the strong will survive. Moving beyond that we either repeat history and create another Federal Reserve, or we can ask ourselves, 'what can we put into code?'"

 "That is the ultimate challenge we face as a space. If we are successful, not only do you create something much better, more transparent, and efficient – it will be a global system. That is my hope for what cryptocurrencies can achieve. If we can get there scams will disappear, and there will be an expectation that things will work the way they ought to, as opposed to today."

Other speakers also tackled the growing trend of ICOs, or looked at the issue of regulation.

Also at the conference was Professor Roman Oliynykov, part of the IOHK Veritas team, which is based in Ukraine. Set up in 2016, the six-person team conducts due diligence, research and development in the area of cryptocurrencies. He summed up the local interest in the subject:

"In my city, Kharkiv, there were more than 1,000 registrations for the last Bitcoin meet-up, which would have been unimaginable only six months ago. There is a huge popularity of blockchain systems in Ukraine and there are many qualified professionals for scientific research into blockchains."

A main focus for the Veritas team has been research into treasury systems. This mechanism provides a pool of funding for the development of cryptocurrencies and allows communities, rather than single individuals or entities, to vote on the decisions that determine the future of a cryptocurrency.

Roman said: "Researchers at Lancaster University in the UK in collaboration with the Veritas team have almost finished a new voting protocol for a treasury, which provides privacy in voting, yet in a transparent process. It also provides delegation. Moreover, we can find out how popular each expert is, how many people are delegated to each expert, but the delegation itself remains private."

An expert as referenced in this case is a person trusted by the community. Some people will prefer to delegate their vote to experts.

For the organisers of BIP, an expanded programme is being planned for the next event. Pavel is looking at the possibility of a week-long conference that could include courses too. That would be great news for the loyal fans of this well put together event.

I am delighted to see the recent news coverage about the Ouroboros paper being accepted to Crypto 17, the most prestigious cryptography event of the year. No other blockchain protocol, apart from Bitcoin, has achieved this level of academic peer review. This is recognition from the academic community that this paper is a serious contribution to cryptography, in being the first Proof-of-Stake protocol to be provably secure. In computer science, what matters in terms of gaining a stamp of approval for new research is not being published in journals, as is the case in many other fields. Instead, what is most important is having the paper accepted by conferences to be scrutinised by fellow academics. This is why we are very proud that our researchers’ work has been admitted to Crypto 17.

The conference takes place in California during August and topics covered include all aspects of cryptography, not only Bitcoin and blockchain.

Developing a secure Proof-of-Stake protocol is one of the big problems to solved in cryptography. It is the key to blockchains being scaled up to handle many more users than it can at the moment. You only have to look at the hurdles that Proof-of-Work based Bitcoin is facing, as it undergoes a struggle to upgrade its technology, to see why Proof of Stake is important.

Proof-of-Stake protocols have the advantage of avoiding the huge computer processing resources demanded by Proof-of-Work systems – one study showed that the energy required to run Bitcoin’s blockchain was equivalent to the power consumed by a small country.

It is highly unusual for a new protocol to progress this quickly from research to implementation, with publications usually taking years to mature for real-world use. Our researchers know of no other cryptography paper that has progressed through peer review this fast. Ouroboros is already being applied to industry use – it is going into Cardano, a blockchain platform being developed by IOHK.

Professor Aggelos Kiayias, who led the research, says: "Building a secure Proof-of- Stake blockchain is an important open problem and I am very happy that we will share our progress towards its resolution with fellow cryptographers at Crypto this year. In Ouroboros, we flesh out for the first time the combinatorial nature of proving the security of Proof of Stake blockchain protocols and I anticipate that our methodology will be valuable widely to blockchain researchers.

"By developing a provably secure Proof-of- Stake protocol, we can now confidently build a blockchain that can handle many more users, resolving many of the scalability and performance issues faced by proof-of- work based protocols like Bitcoin. We have already implemented Ouroboros and tested it with a cloud deployment with very good results."


"With Ouroboros, as well as the upcoming version of our protocol ‘Ouroboros Praos’ that will be released soon, IOHK is at the forefront of efficient and secure blockchain research and development," Prof Kiayias adds.

Crypto 17 is the 37th International Cryptology Conference. It will be held from August 20 to 24 this year, at the University of California, Santa Barbara, and is sponsored by the International Association for Cryptologic Research (IACR).

Further information on the Ouroboros paper is also available in a series of videos.

It is well known that randomness is a fundamental resource for secure cryptographic schemes. All common encryption and authentication schemes are only as secure as their randomness sources are good. Using a poor randomness source can basically render insecure every cryptographic scheme that would otherwise be secure. In many cases, it is sufficient to have a trustworthy local source of fresh randomness (e.g. your operating system’s randomness pool or a Random Number Generator (RNG) embedded in your CPU). However, in many distributed applications, it is necessary to use a publicly accessible source of randomness that allows users (and external observers) to make sure they are all getting the same random values. With such applications in mind, in 1983 Michael Rabin introduced the concept of a randomness beacon, a publicly accessible entity that provides a periodically refreshed random value to its clients. More recently, NIST, the National Institute of Standards and Technology in the United States, started offering a randomness beacon service that derives its randomness from quantum physical processes.

When users are willing to trust a centralised randomness beacon they can simply choose one of them to perform this role or use a publicly available beacon, such as the one from NIST. However, standard randomness beacons provide no means for users to verify that the output values are indeed random and not skewed in a way that gives an advantage to an attacker.

As we know, cryptographic schemes have suffered both from poor implementations and from governmental agencies (e.g. the NSA) that actively work to undermine existing and future standards. In this context, a centralised randomness beacon could be providing bad randomness because of simple implementation mistake or in order to do the bidding of third party attacker who has undermined the central randomness generator or simply presented the people running the service with a subpoena that compels them to do so.

Using a coin tossing protocol (a concept also introduced by Rabin in 1981) is an obvious approach to (partially) solve this problem. Coin tossing allows several users to come together and generate an output that is guaranteed to be uniformly random without having to trust each other or any third party.

In a coin tossing protocol, good randomness is obtained if at least one of the parties is honest. If you run a coin tossing among many servers, somebody who trusts at least one of the servers can be assured that the output is truly random. In many applications (such as cryptocurrencies) we assume that at least half of all parties are honest by design.

Even though using coin tossing protocols solves the trust problem, it still does not make it any easier to ensure that all users will receive the random output. For example, a user with a faulty internet connection or an attacker who wants to mount a Denial-of-Service attack against the protocol (and consequently the application using the final randomness) can simply abort (i.e. stop sending protocol messages) before the output is obtained, keeping all the other users from receiving randomness. In fact, a malicious user can do even worse, he can execute the protocol up to the point where he learns the random output but still not send the final message that would enable the other users to also learn this output.

Tal Rabin and Ben-Or introduced a classical method for making sure all users receive the proper protocol output – assuming at least a majority of them is honest – in a seminal paper in 1989. The main idea is to use "secret sharing" to split each user’s input into "shares" that do not reveal any information about the input by themselves but allow for total recovery of the input if a sufficient number of them are put together. If each user is given a share of every other user’s input – such that the inputs can be recovered if more than 50% of the shares are pooled – malicious users still cannot learn anything because we assume that more than 50% of the users are honest. However, if a malicious user aborts the protocol at some point, the honest users can pool their shares to recover the malicious user’s input and finish the protocol by themselves.

This general approach can be used to make sure that all the users running a coin tossing protocol will receive the final random value. However, this still does not allow users and external observers to make sure that the output is being generated correctly. In order to do that, the users must use a kind of secret sharing that is publicly verifiable, meaning that anyone can make sure that the shares of inputs are correctly generated. This prevents malicious users from posting invalid shares and then aborting in such a way that the honest users cannot reconstruct their inputs. This approach has been used for generating publicly verifiable randomness in the Ouroboros Proof-of-Stake based, permissionless consensus protocol and for constructing a stand-alone randomness beacon in a paper by Syta et al. that will be presented at the IEEE Symposium on Security and Privacy 2017.

The main ingredient in building randomness beacons through this approach is Publicly Verifiable Secret Sharing (PVSS), a type of secret sharing scheme introduced by Stadler that allows users to split their inputs in shares whose validity can be promptly verified by any third party. Using such schemes, it is possible to construct coin tossing protocols with Guaranteed Output Delivery through the approach of Rabin and Ben-or, meaning that every user is guaranteed to receive the final randomness produced by the protocol. However, the PVSS scheme from Schoenmakers, which until recently was the most efficient PVSS scheme, still requires a number of modular exponentiations that is quadratic in the number of users, meaning that if there are n users running the protocol, verifying the n shares produced by one of them requires O(n^2) exponentiations. Note that this poses serious scalability issues since this quadratic overhead means that the number of expensive modular exponentiations required for verifying n shares grows quite a lot given even a small increase in the number of users.

In a recent joint paper with Ignacio Cascudo, SCRAPE: Scalable Randomness Attested by Public Entities that will presented at ACNS 2017 in Japan this July, we have solved this scalability problem by introducing a PVSS scheme that only requires O(n) modular exponentiations to verify n shares (5n modular exponentiations to be precise) while maintaining efficiency of all other protocol components. The main idea behind our protocol is to use a cheap information theoretical trick to verify the validity of shares instead of performing expensive modular exponentiations. As a result, our protocol requires only 5n modular exponentiations in the verification phase and 4n modular exponentiations in the distribution phase (where shares are generated), while the protocol by Schoenmakers requires 4n+(n^2)/2 exponentiations for verification and 4n+t exponentiations for distribution, where n is the number of users/shares and when n/2 shares are required for reconstructing the secret. Our efficient PVSS protocol can be used to improve the randomness generation component of Ouroboros and the recent result by Syta et al.

It took a little longer than expected but I finally made the trip to Buenos Aires, Argentina. In fact, I'm standing at a work desk by the window in Frankfurt airport waiting for my flight back to Dublin. I'm enjoying a gloriously sunny day here through the wall of glass. 

It was another productive trip, a lot has happened since the Team Grothendieck trips to Poland and St Petersburg. In our work to build a Scala client for Ethereum Classic there has been a lot of code written, a lot of understanding gained, and a couple of milestones reached: we now have the ability to download and execute blocks of transactions from the ETC chain. We have also evolved a lot as a team.

The remaining milestones to reach include mining, and the JSON API – to allow Mist and other dapp wallets to use our client. In parallel with that we need to focus on our codebase. It was this process that the Grothendieck team’s Alan Verbner and Nico Tallar, and I spent our time on in BA. 

As a background, in an ideal world we would create code from day one supporting the coupling that made sense as we approached the release. However, this is an almost impossible task because we can't usually know the most sensible "final" coupling when starting out. For the ETC client we took the (oft used) approach that we would write clean unit tested code that implemented the functionality we understood at the time and then refactor as we learnt more. For example, when we finished the block download phase we had very little in the way of model classes for ‘blockchain’. However, as we spun up the "Tx Execution" phase, we discovered it made a lot of sense to create a set of functions coalescing around a ‘blockchain’ model. 

There's a school of thought that says this is the way to carry on: don't waste your time building "reusable" components that aren't reusable and won't be reused. I have sympathy for this approach because building reusable components is hard and it is embarrassing for your new component – the one you spent time and effort on – to fail at the first attempt at reuse because it doesn't quite do what you need it to. Better to allow the new functionality to drive refactors as and when it comes. There's a humility to this approach that appeals to me. 

Guess what's coming next? We're going to look at ways to modularise our client. Why? Firstly and most importantly it's a functional requirement for the codebase to support a significant level of flexibility. Four things that might define the core of a blockchain client are the network module, the ledger, the consensus mechanism and the wallet. Closely coupling the wallet and ledger together, we would like to experiment with different types of ledger and different types of consensus. And these should be able to use a well defined network module.  

So we will first attempt to isolate the 'network' module. This is a module that maintains connections to peers and sends and receives a configurable set of messages. It allows messages to be addressed to a peer or broadcast to many peers. It allows clients of the module to register for types of messages and types of message per peer. It's also functionality that we have already created. We just need to organize it so that it's reusable!

Why now? The JSON RPC API – in theory – should be controller layer code. The mining integration should – also in theory – not affect the workings of the network module. So the functionality to be reused should already exist and when we repackage it without breaking the existing system we know it's useful. By the time we get around to examining the coupling of the ledger and consensus the same should be true, we won't be making up use cases for invented modules, we will have specific working code to repackage. Will we produce interfaces and coupling that can be reused? That's the challenge. And after that – optimization of the internals...

Mining, web API and modularisation are not trivial tasks but they will end. And with them we reach the end of the existing roadmap – stability, bug fixes and auditing aside. For the past five months we have been playing catch up, we didn't need to talk about future evolution of the technology because we had a clear and challenging mandate – to recreate a client from the ground up. Now that we're relatively close to doing that, the exciting process of talking about the future of the codebase can begin. 

While in BA, Sergio Lerner kindly hosted the three of us at his office and over decent coffee and alfojores we had a good discussion about Ethereum tech, and some of the things he's been up to. And of course, RSK's upcoming release of their platform at Consensus 2017 in NYC. (Best of luck RSK!)

I'm always interested in how a global blockchain aimed at general purpose use can scale, with no way to delete defunct contracts from the global state trie. Sergio made the interesting point that ETC probably won't need to scale for a couple of years. He also suggested that with storage being so cheap for a network in a steady state (with most nodes staying up to date) it would be more expensive for all nodes to delete a contract than to keep it.

Apart from Rootstock, the Bitcoin Embassy in Buenos Aires, where Alan and Nico normally work is littered with interesting people working on multiple ways of leveraging the Bitcoin blockchain. There's a great atmosphere in the building, calm and friendly but industrious and I really enjoyed my time there, so when it was suggested we attend a live podcast…we said yes!

A special shout out to Alan Verbner, a man who is proud of his city and I think the city can be proud of him. We walked the city the whole weekend and I got a real sense of it. BA is modern but you don't have to look too hard to find old world charm – French restaurants with dark wood and marble counters, majestic old cafes full of Art Deco gold fittings and the smell of cardamon infused coffee. And then there's the steak. Vegetarians, look away now. I'm delighted to report that Argentina’s reputation for steak is well deserved. The variety of cuts, the sauces, the cooking...it might be worth going back just to eat steak. 

TL;DR You want to avoid the next DAO-like disaster: so you want confidence that the system underpinning your cryptocurrency doesn’t have a hidden flaw that could be triggered at any time and render your assets worthless. To get that confidence you need a high assurance implementation of the system operating your cryptocurrency. Formal methods (mathematical specifications and proofs) are the best way to build high assurance software systems, and that is what we are aiming to do with the software behind the cryptocurrencies we build.

How can you sleep at night?

A gold bar or a wodge of cash stashed in a safe has the rather nice property that it doesn’t just evaporate overnight. Money managed by computer software is not inherently so durable. Software flaws can be revealed without warning and can destroy the trust in whole systems.

We only have to look around us to see the prevalence of software flaws. The IT trade press is full of news of data breaches, critical security patches, zero-day exploits etc. At root these are almost all down to software flaws. Standard software development practices inevitably lead to this state of affairs.

With the DAO in particular, the flaw was in the implementation of the smart contract that defined the fund, not directly in Ethereum itself. So the implementation of contracts and the design of smart contract languages is certainly an important issue, but the next flaw could be somewhere else. It’s hard to know.

So how are we to sleep soundly at night? How can we be confident that our cryptocurrency coins are not just going to evaporate overnight? What we need is assurance. Not to be confused with insurance. Assurance is evidence and rational arguments that a system correctly does what it is supposed to do.

Systems with high assurance are used in cases where safety or a lot of money is at stake. For example we rightly demand high assurance that aircraft flight control systems work correctly so we can all trust in safely getting from A to B.

If as a community we truly believe that cryptocurrencies are not a toy and can and should be used when there are billions at stake then it behoves us to aim for high assurance implementations. If we do not have that aim, are we really serious or credible? And then in the long run we must actually achieve high assurance implementations.

In this post we’ll focus on the software aspects of systems and how formal methods help with designing high assurance software. Formal methods can be very useful in aspects of high assurance system design other than software, but that’ll have to wait for some other blog post.

What does assurance look like?

While we might imagine that assurance is either “yes“ or “no“ – you have it or you don’t – it actually makes sense to talk about degrees of assurance. See for example the summaries of the assurance levels, EAL1 to EAL7, in the CC security evaluation standard. The degree of assurance is about risk: how much risk of system failure are you prepared to tolerate? Higher assurance means a lower risk of failures. Of course all else being equal you would want higher assurance, but there is inevitably a trade-off. Achieving higher levels of assurance requires different approaches to system development, more specialised skills and extra up-front work. So the trade-off is that higher assurance is perceived to come with greater cost, longer development time and fewer features in a system. This is why almost all normal commercial software development is not high assurance.

There are two basic approaches to higher assurance software: the traditional approach focused on process and the modern approach focused on evidence, especially formal mathematical evidence.

Historically, going back to the 1980s and before, the best we could do was essentially to think hard and to be very careful. So the assurance standards were all about rigorously documenting everything, especially the process by which the software was designed, built and tested. The evidence at the end is in the form of a big stack of documents that essentially say “we’ve been very methodical and careful”.

Another approach comes from academic computer science – starting in the 80’s and becoming more practical and mature ever since. It starts from the premise that computer programs are – in principle – mathematical objects and can be reasoned about mathematically. When we say “reason about” we mean mathematical proofs of properties like “this program satisfies this specification”, or “this program always computes the same result as that program”. The approach is that as part of the development process we produce mathematical evidence of the correctness of the software. The evidence is (typically) in the form of a mathematical specification along with proofs about some useful properties of the specification (eg security properties); and proofs that the final code (or critical parts thereof) satisfy the specification. If this sounds like magic then bear with me for a moment. We will look at a concrete example in the next section.

One advantage of this approach compared to the traditional approach is that it produces evidence about the final software artefacts that stands by itself and can be checked by anyone. Indeed someone assessing the evidence does not need to know or care about the development process (which also makes it more compatible with open-source development). The evidence does not have to rely on document sign-offs saying essentially “we did careful code review and all our tests pass”. That kind of evidence is great, but it is indirect evidence and it is not precise or rigorous.

In principle this kind of mathematical approach can give us an extremely high level of assurance. One can use a piece of software called a proof assistant (such as Coq or Isabelle) which provides a machine-readable logical language for writing specifications and proofs – and it can automatically check that the proofs are correct. This is not the kind of proof where a human mathematician checking the proof has to fill in the details in their head, but the logician’s kind of proof that is ultra pernickety with no room left for human error.

While this is perhaps the pinnacle of high assurance it is important to note that cryptocurrencies are not going to get there any time soon. It’s mostly down to time and cost, but also due to some annoying gaps between the languages of formal proof tools and the programming languages we use to implement systems.

But realistically, we can expect to get much better evidence and assurance than we have today. Another benefit of taking an approach based on mathematical specification is that we very often end up with better designs: simpler, easier to test, easier to reason about later.

Programming from specifications

In practice we do not first write a specification then write a program to implement the spec and then try to prove that the program satisfies the specification. There is typically too big a gap between the specification and implementation to make that tractable. But it also turns out that having a formal specification is a really useful aid during the process of designing and implementing the program.

The idea is that we start with a specification and iteratively refine it until it is more or less equivalent to an implementation that we would be happy with. Each refinement step produces another specification that is – in a particular formal sense – equivalent to the previous specification, but more detailed. This approach gives us an implementation that is correct by construction, since we transform the specification into an implementation, and provided that each refinement step is correct then we have a very straightforward argument that the implementation is correct. These refinement steps are not just mechanical. They often involve creativity. It is where we get to make design decisions.

To get a sense of what all this means, let’s look at the example of Ouroboros. Ouroboros is a blockchain consensus protocol. Its key innovation is that it does not rely on Proof of Work, instead relying on Proof of Stake. It has been developed by a team of academic cryptography researchers, led by IOHK Chief Scientist Aggelos Kiayias. They have an academic paper, Ouroboros describing the protocol and mathematical proofs of security properties similar to that which Bitcoin achieves. This is a very high level mathematical description aimed for peer review by other academic cryptographers.

This is a great starting point. It is a relatively precise mathematical description of the protocol and we can rely on the proofs of the security properties. So in principle, if we could prove an implementation is equivalent (in the appropriate way) to the description in the paper, then the security proofs would apply to our implementation, which is a great place to be.

So how do we go from this specification to an implementation following the “correct by construction” approach? First we have to make the protocol specification from the paper more precise. It may seem surprising that we have to make a specification more precise than the one the cryptographers wrote, but this because it was written for other human cryptographers and not for machines. For the refinement process we need to be more like the pernickety logicians. So we have to take the protocol specification written in terms of English and mathematical symbols and redefine it in some suitable logical formalism that doesn’t leave any room for ambiguity.

We then have to embark on the process of refinement. The initial specification is the most abstract and least detailed. It says what must be done but has very little detail about how. If I have a more detailed specification that is a refinement of the initial specification then what that means intuitively is: if you are happy with the initial specification then you would be happy with the new specification. You can have different refinements of the same specification: they differ in details that are not covered in the original specification. Refinement also has a quite specific formal meaning, though it depends on exactly what formalism you’re using. In process calculi, refinement is described in terms of possible observed behaviours. One specification is a refinement of the other if the set of possible observed behaviours are equivalent to the other. Formally the kind of equivalence we need is what is known as a bisimulation.

In the case of Ouroboros we start with a very abstract specification. In particular it says very little about how the network protocol works: it describes things in terms of a reliable network broadcast operation. Of course real networks work in terms of unreliable unicast operations. There are many ways to implement broadcast. The initial specification doesn’t say. And it rightly doesn’t care. Any suitable choice will do. This is an example where we get to make a design choice.

The original specification also describes the protocol in terms of broadcasting entire blockchains. That is the whole chain back to the genesis block. This is not intended to be realistic. It is described this way because it makes the proofs in the paper easier. Obviously a real implementation needs to work in terms of sending blocks. So this is another case for refinement. We have to come up with a scheme where protocol participants broadcast and receive blocks and show how this is equivalent to the version that broadcasts chains. This is an interesting example because we are changing the observed behaviour of protocol participants: in one version we observe them broadcasting chains and in the other broadcasting blocks. The two do not match up in a trivial way but we should still be able to prove a bisimulation.

There are numerous other examples like this: cases where the specification is silent on details or suggests unrealistic things. These all need to be refined to get closer to something we can realistically implement. When do we move from specification to implementation? That line is very fuzzy. It is a continuum, which comes back to the point that both specifications and programs are mathematical objects. With Ouroboros the form of specification is such that at each refinement step we can directly implement the specification – at least as a simulation. In a simulation it’s perfectly OK to broadcast whole chains or to omit details of the broadcast algorithm since we can simulate reliable broadcast directly. Being able to run simulations lets us combine the refinement based approach with a test or prototype based approach. We can check we’re going in the right direction, or establish some kinds of simulated behaviour and evaluate different design decisions.

There are also appropriate intermediate points in the refinement when it makes sense to think about performance and resource use. We cannot think about resource use with the original high-level Ouroboros specification. Its description in terms of chain broadcast makes a nonsense of any assessment of resources use. On the other hand, by the time we have fully working code is too late in the design process. There is a natural point during the refinement where we have a specification that is not too detailed but concrete enough to talk about resource use. At this point we can make some formal arguments about resource use. This is also an appropriate point to design policies for dealing with overload, fairness and quality of service. This is critical for avoiding denial of service attacks, and is not something that the high-level specification covers.

Of course any normal careful design process will cover all these issues. The point is simply that these things can integrate with a formal refinement approach that builds an argument, step by step, as to why the resulting design and implementation do actually meet the specification.

Finally it’s worth looking at how much flexibility this kind of development process gives us with the trade-off between assurance and time and effort. At the low end we could take this approach and not actually formally prove anything, but just try to convince ourselves that we could if we needed to. This would mean that the final assurance argument looks like the following. We have cryptographers check that the protocol description in their paper is equivalent to our description in our logical formalism. This isn’t a proof, just mathematicians saying they believe the two descriptions are equivalent. Then we have all the intermediate specifications in the sequence of refinements. Again, there are no formal proofs of refinement here, but the steps are relatively small and anyone could review them along with prose descriptions of why we believe them to be proper refinements. Finally we would have an implementation of the most refined specification, which should match up in a 1:1 way. Again, computer scientists would need to review these side by side to convince themselves that they are indeed equivalent.

So this gives us some intermediate level of assurance but the development time isn’t too exorbitant and there is a relatively clear path to higher assurance. To get higher assurance we would reformulate the original protocol description using a proof assistant. Then instead of getting a sign-off from mathematicians about two descriptions being equivalent, we could prove the security properties directly with the new description using the proof assistant. For each refinement step the task is clear: prove using the proof assistant that each one really is a refinement. The final jump between the most detailed refined specification and equivalent executable code is still tricky because we have to step outside the domain of the proof assistant.

With the current state of proof tools and programming language tools we don’t have a great solution for producing a fully watertight proof that a program described in a proof assistant and in a similar programming language are really equivalent. There are a number of promising approaches that may become practical in the next few years, but they’re not quite there yet. So for the moment this would still require some manual checking. Really high assurance still has some practical constraints: for example we would need a verified compiler and runtime system. This illustrates the point that assurance is only as good as the weakest link and we should focus our efforts on the links where the risks are greatest.

Direction of travel

As a company, IOHK believes that cryptocurrencies are not a toy, and therefore believes that users are entitled to expect proper assurance.

As a development team we have the ambition, skills and resources to make an implementation with higher assurance. We are embarking on the first steps of this formal development process now and over time we will see useful results. Our approach means the first tangible results will offer a degree of assurance and we will be able to improve this over time.