A Smart Contract
Development Stack
Better Abstractions for Correct Smart Contracts
Blockchains and Smart
Contracts are one of the most intense hypes I have ever encountered, a close
number two right after micro services :-) Even the IHK Stuttgart, the
local industry association, recently organised a Blockchain Camp, and around
200 people attended, many of them with no computer science background.
Two Aspects of Smart
Contracts
For me, the topic
conceptually splits into two aspects. One is the non-functional properties
provided by the Blockchain technology, such as trustworthiness and
non-repudiability, as a consequence of the distributed nature of block
processing and the involved math. Even though it builds on many established ideas
and technologies (such as public key crypto), the approach is fundamentally new
and interesting. Some of the particular technologies definitely need to change
to approaches that are way less wasteful of energy though; Algorand looks
very interesting, as well as Ethereum’s native work on proof-of-stake in the
context of Casper.
The other aspects is the idea
that non-programmers can specify, analyse, simulate and ultimately execute
contracts. And I really mean contracts, i.e., processes where multiple involved
parties make (a sequence of) decisions over time. The non-functional properties
of blockchains can be beneficialhere, but are not necessary —
if you trust a central entity, you can delegate the execution of the contract
to that entity and use crypto to control who is allowed to do what as part of a
contract. This second aspect is very much in line with the computerification of
other non-technical domains such as computational
law or computational governance. It is probably not a surprise to
you, dear reader, that I consider this a very good use case for DSLs.
Ethereum and Solidity
The preeminent platform for
executing smart contracts is Ethereum. Except for the energy issue, it is very suitable
for providing the non-functional properties of blockchains I mentioned above.
However, it falls short in the second aspect. The primary programming language
for the Ethereum VM (EVM) is Solidity.
It is essentially a general-purpose programming language with support for the
specifics of programs that run on the blockchain. For example, running code on
the distributed EVM costs money (Ether), and developers can limit the
processing time used by a particular program in order to not run out of money.
And every method that’s called on a contract implicitly carries information
about the sender (more specifically, their account number) so that the fee for
a transaction can be paid by this account; the ID can also be used for
authorisation of operations defined in the contract. However, Solidity (and the
other Ethereum languages I have seen so far) does not provide first-class support
for the typical patterns found in smart contracts that run on the blockchain,
i.e., programs where a group of parties collaboratively make decisions and run
processes. This is interesting, since the community has identified typical
“contract patterns” that are a good starting point for reification into
language abstractions.
An Architecture for Smart
Contract Development
The following picture shows
an overview of how I imagine a Smart Contract development environment to look
like. Let’s walk through the parts.
The first realisation is that
the overall problem can be broken down into the development of contracts and
into its execution.
Contract Execution
Considering that blockchain
technology exists (and ignoring the energy challenge), execution is almost the
simpler problem. Once you have implemented a contract correctly (!), you can
deploy it to the blockchain and execute it there, benefiting from the
guarantees provided by the blockchain (and maybe also suffering from some of
its limitations, such as relatively low throughput, at least for now). Several
different blockchain technologies exist; for example, in a business context, it
seems that Hyperledger might
be(come) more important than Ethereum. It doesn’t have exactly the same
properties or guarantees, but that is good: users can choose the properties
they need. Notice, however, the exclamation point behind the “correctly” above.
That is the crux!
It is of course necessary
that the infrastructure itself provides correctness guarantees. This is why
various projects are under way to formally verify the virtual machine or enhance the
solidity compiler to support advanced checking through integration with a
solver. However, you can still implement the wrong behavior in
your contract (which is then correctly executed by a verified VM). This is
where the importance of the right contract development languages and tools come
in.
Contract Development
It’s almost funny how often I
have heard statements like, “Well, contracts have to be correct,
because, in contrast to other software, money is involved, and you don’t want
to lose that.” True, of course, but if you’re the developer of pace
makers, you don’t want to kill people because of bugs in your software. And if
you develop satellites, you don’t want it to die from a software bug on day two
of the mission. So, ensuring the correctness of a program is relevant outside
of smart contracts, too. And we should take a look at what those communities
do, and not reinvent the wheel (a gentle hint at the formal methods booklet :-)). More generally, this
means that the development of (correct) contracts must also be supported by the
overall toolchain. Here is how I envision this to work.
Contract development should
rely on a language stack. At the core of this stack, I expect a functional
programming language. Functional languages are useful because they are
(relatively) easy to verify, and can also relatively easily support (in-memory)
transactions (as I have discussed in this
previous post), which is useful for contract-style programs. On top of the
functional core, I expect a couple of language extensions that directly support
the above mentioned contract patterns, such as decisions, auctions, agreements
and resource allocations. Each of those can be broken down into a whole range
of configuration options (think: domain analysis, variability, feature model),
that determine the specific behavior. The Executable Multi-Party Contract
Language (EMPCL) in the above picture contains language constructs for these
typical Smart Contract building blocks. It also support state machines, since
most non-trivial contracts are in effect state machines. I will return to this
idea below when we look at example code.
On top of EMPCL, I see
languages (or EMPCL-extensions) that are closely aligned with domains such as
logistics or finance. Each of those has their own idiomatic contract
constructs, and the language extensions should support those directly.
Why language extensions and
not just frameworks or libraries? Because they make it easier to write correct
code (once they are stable). Two reasons. First, by using language constructs
at an appropriate level of abstraction, many lower-level mistakes cannot be
made in the first place. The contract is, to some degree, correct-by-construction.
In addition, a language that makes semantically relevant things first-class
citizens makes verification of the not-correct-by-construction things much
easier (again, a hint at the formal methods booklet :-)); good IDE support can also
be provided more easily. It’s also just less code one has to write, so it’s
easier to understand and review. Even better, by providing an interpreter, one
can interactively play with the contracts and explore their behavior, and write
test cases that are executed immediately. Finally, at least for those DSLs that
are aligned with particular domains (those above EMPCL), there’s a realistic
chance that non-programmer domain experts can read or write the code. Really,
this is the “usual DSL story” that has been proven to work over and over again,
and it will also work here.
Contracts also have a couple
of very specific risks that go beyond functional
safety-style verification that result from their game theoretic nature,
for example sybil attacks or timing problems. For now, dealing
with those is outside of what I am looking at.
Prototypical Implementation
I have implemented some
aspects of this language stack in MPS. In particular, I have started building a
language that could become EMPCL. At this point I have not yet implemented
verification tools, and I don’t yet translate to any blockchain technology for
execution. But some of the core abstractions are available, and this
illustrates how and why they are useful. I will explain them in detail below.
Make sure you have read the post on Dealing
with Mutable State in KernelF, because I rely on it heavily.
The Multi-Party Boolean Decision
The core abstraction I have
implemented is the multi-party boolean decision, i.e., a process which lets a
group of parties make a yes/no decision. It’s the simplest process one can
think of in the context of contracts. We had performed an initial
domain analysis for decisions, and based on this, I have derived the
following set of configuration options.
First, who are the parties involved
in making the decision. In the example above, bernd and markus are
references to global variables of type party. Optionally, the set of
parties can be dynamic, which means that, as the
process executes, additional parties can be made members of the decision
process. If the parties are dynamic, an additional check box
shows up that allows support for sealing the parties: once the
process is sealed, no new parties can be added anymore. The remaining options
concern the actual decision process. The procedure determines how the
final decision is made, e.g., by simple majority, by unanimous agreement or by
a custom algorithm. The turnout determines whether a
minimum number of parties have to actually make a decision. The time limit requires
the decision to be made within a given timeframe, and the revokable flag
determines whether a party can revoke their decision once they have made it.
The decisions are an example
of a process, i.e., a language construct that can be stimulated by
executing commands, and it can be observed by reading values.
Based on the configuration of the process, different commands and values are
available. Since this is a language extension and not just a library, the IDE
knows about these and can provide support, i.e., help ensure some degree of
correctness by construction. A few examples are shown below.
For example, once a turnout is
configured, a non-vote cannot be interpreted as a “no” vote, so the system has
to explicitly support voteFor and voteAgainst commands.
Similarly, although not shown, the decision value is now an opt<boolean> instead
of a boolean because, until the turnout has been achieved,
no decision has been taken (and none is returned). Also, all
the commands to add parties are only offered if dynamic is
selected.
Playing with Decisions — the REPL
Processes have this nice
property of uniform interaction: send in commands, observe values. The KernelF
Read-Eval-Print-Loop, or REPL, has special support for such values through the live() expression.
Applied to a process (such as the MultipartyBooleanDecision), it provides code
completion for the commands that are currently allowed. In fact, it even looks
at the current state of the process and only supports those commands that are allowed
at the current execution state. The REPL also supports a nice,
readable rendering for the values of processes. For a sequence of steps, it
even highlights the changes in blue, so it’s easy to observe how a process
evolved as users issue comm. The next screenshot shows a REPL session on a MultipartyBooleanDecision with a dynamic set of parties and sealing
enabled. Check out how the internal state changes based on the commands issued.
Because all of this is based
on a generic, reflective API, one can imagine other UIs. In particular, we will
build a “simulator” where there are buttons for each command and UI widgets for
each value. This will allow non-programmers to creatively play with a contract
and thus better understand how it behaves.
Of course, one can also
script tests and execute them directly in the IDE, based on the same
interpreter that also drives the REPL.
Combining Decisions with State Machines
The decision described above
supports basic, multi-party decisions. Over time, we will also add support for
auctions, agreements and other contract patterns. However, a contract will also
always have specific behavior that cannot easily be expressed declaratively.
However, there’s no reason to “fall down” to imperative programming just yet.
State machines are a much better abstraction for many of these behaviors,
especially when combined with the processes. Consider the following set of
requirements:
We have a set of products, each can
potentially be sold. First, a
predefined group of stakeholders has to make a decision for each of the
products whether it should indeed be sold or not. Everybody has to vote, and
the
decision is by majority. There is a limited time by which the vote has
to have taken place. Once that decision has been made for all products,
each products can be sold to somebody; a product can only be sold once,
and the price must be the same or higher as the one specified in the
offer, and the offer must not have been sold before. All sales are
recorded. Once all sellable products have been successfully sold, the
contract terminates.
This is a realistic, and not
totally simplistic example of a contract. Let’s look at its implementation
based on declarative decision processes, state machines and a couple of helper
functions. We also need a couple of data types; we start with those, they
should be rather obvious:
Next, we define a few helper
functions, the comments in the code explain what they do.
The remaining implementation
consists of one decision process and a state machine (with a few more embedded
functions). We show the code next, and then discuss it in some detail:
The state machine serves as
the “top level” interface for the contract. Its API are the two events defined
in it. The first one, vote, expresses that the party who votes for
or against (expressed through the Boolean parameter) selling the product with
the given ID. The second event, buy, expresses that a particular
party wants to buy a product for a given price.
The next line is crucial.
Remember that we want to make a separate sell/no-sell decision for every
product/offer. So the salesDecisions variable is initialized
to a map that contains an instance of the ShouldWeSell process associated with
each product ID.
Let’s now move on to the
initial state decideOnSelling. If the vote event
comes in, we react by checking whether the shouldWeSell flag is true. If so, we
retrieve the sales decision process for the respective product and voteForit. Otherwise
we voteAgainst. If, for all sales decisions, the turnout has been
achieved we transition to the selling state.
In the selling state, we
expect the buy event (any other event
leads to a failure of the operation). If it comes in, and the decision to sell
the particular product has been positive (check out the shouldBeSold function),
we retrieve the box that contains the offer and call tryToBuy. Otherwise we
ignore the event. Once all to-be-sold products have been sold, we move to the endedstate.
The final piece of the puzzle
is the tryToBuy function. If the product/offer has already
been sold it does nothing; otherwise it checks if the price paid by
the buyer is greater or equal to the price stated in the offer, and if so, sets
the offer’s sold flag to true and adds
the corresponding sale to the list of sales.
Another Example
This final example is one
where several decision processes interact and processes are started dynamically
by the coordinating state machine. It’s similar to the (in-)famous DAO in
the sense that the set of decision makers changes dynamically. In particular,
the requirements are:
We’re an online community that has to
continuously maintain a (selling)
decision; it can be revoked or granted over time. The group of
individuals, called the deciders, can vote (and revoke) this sales
decision. The vote has to be unanimous. In addition, additional people
can be voted into the group of deciders. The existing deciders vote for
new candidates, by simple majority, but with a time limit. Once voted
into the group of deciders, the new member can participate in the
sell/no-sell decision. Multiple member approval processes can go on at
the same time. While a member request is pending, the sales decision cannot
be changed.
At the core are two decision
processes. Sale runs “forever” and
manages the group decision. It’s membership can change over time. The other
process, AccessControl, manages the join request
and the voting for a potential new guy. It is started, dynamically, for each
join request. The key is that whenever a join request for a new guy finishes
successfully, it’s join process is terminated, and the new guy is added to the
parties of the Sale process. Check out the
code, as well as the REPL session below.
The REPL session is a bit
longish, but it does illustrate the point.
Wrap up and Outlook
It should be obvious from
these examples that the ability to declaratively specify contracts based on a
mix of state machines and (a growing) set of declarative decision, auction,
agreement and resource allocation processes provides a solid foundation for
efficiently implementing Smart Contracts. Many low-level mistakes cannot be
made, and stakeholders can experiment with the contract by playing with it in
the REPL and a future simulator. Tests can be written an executed.
It’s probably worth
mentioning that the whole contract, state machines and decision processes, are
transactional (as discussed in that previous
post). So if anything goes wrong (e.g., an event is posted when there is no
transition that handles it), the machine fails and the transaction, if one has
been started before, is rolled back.
In the future, we will
implement functional verification of contracts based on an integration with
model checkers and SMT solvers; but don’t expect a post that too soon, this is
quite a bit of work.
Finally, we also need a
deployment story. We are working on a Java generator for KernelF and all the
rest, so a plain Java (Enterprise) deployment is not too far away. We are also
working on a generator to Ethereum to exploit its non-functional properties as
well. But again, these things will take some time. My goal with this work, and
this post, was to play with better abstractions for Smart
Contracts; let me know if I succeeded.