Scaling your dApps with Legicash

A revised version of this article is available under the title “Scaling your dApps with Alacris.io” at https://medium.com/alacris/scaling-your-dapps-with-alacris-io-e7ab53f5b864

You may have heard how we at Legicash are working to scale cryptocurrency payments. And these days, who isn’t? But our technology isn’t just about payments — it’s a general approach to developing and scaling dApps. Payments are just the first step, necessary for any dApp that involves cryptocurrency. In the future, our platform will support non-custodial exchanges and cross-chain payments. And on that platform, you will be able to build your own secure, scalable dApps.

Technical Summary

First, let’s summarize our technical offering before we examine it in detail.

At Legicash, our approach to designing dApps is that they do as little work as possible on the main chain, and as much as possible off-chain. Legicash is agnostic to the main chain being deployed. For practical purpose, the main chain is currently Ethereum. The only requirement for the main chain is its ability to securely express the rich smart contracts of Legicash. Using the main chain is strictly limited to making final settlements and to keeping everyone’s interests aligned via smart contracts where participants post bonds to serve as collateral. This way, regular transactions can scale without being limited by the necessarily high latency, low value, and high cost of the main chain consensus.

Auditable off-chain work happens on one or several side-chains. Unlike earlier side-chain proposals, the Legicash design is unique in that users do not have to trust the side-chain managers, who we call facilitators. Instead, these facilitators are bound to the rules of the dApp protocol by a smart contract on the main chain and are held accountable by the threat of losing their bond if they fail. Our contracts use formal logic so that we can precisely describe the role and responsibilities of each participant in the dApp protocol. Abuse claims can then be verified using interactive proofs while a court registry ensures that side-chain managers continually publish the complete, well-formed state of their side-chain, thus ensuring that anyone can partake in these proofs.

That’s quite a mouthful of a technical summary, so now let’s recapitulate in detail.

Game Theory and Smart Law

At Legicash, we think about software first and foremost in terms of distributed applications that involve multiple actors with distinct and possibly divergent interests. Studying interactions from the point of view of whether the interests of actors are aligned or opposed is the domain of game theory. This is a scientific topic at the intersection of Economics, Mathematics, and Military Science, familiar to all you information security professionals out there.

The technology that ensures that computerized actors’ interests converge and remain aligned is called “smart law” — where “smart” denotes automation, not intelligence, and “law” denotes an analogy to human law, not a substitute to it. This smart law can take the form of smart statutes, whereby they are rules baked into the interaction protocol itself that applies to all participants, or of smart contracts, wherein the rules are defined as an add-on to the protocol, that only applies to those participants who opt in. The protocol can therefore be seen as a court system, that prevents and resolves disputes between participants by enforcing property rights and contracts. In this, our vision is very similar to that of Truebit or Plasma.

On the other hand, our vision challenges a common view of contracts as a means to conduct arbitrary computations on the blockchain. Instead we understand that computation on the main chain is inherently more expensive than outside the main chain. For example, computing on Ethereum is currently a million times more expensive than on the cloud, and there is reason to believe that it will always be much more expensive. In human terms, resolving conflicts in a federal court system is much more expensive and risky than resolving them in local courts, or even better, settling conflicts out of court, or better yet, avoiding conflict altogether. In smarts contracts as in human contracts, going to court should never be plan A; rather, it is a last resort if the other party doesn’t comply with the agreed-upon contract and also refuses to settle out of court. A strong contract is very clear about who is responsible for what, and what the consequences are if they fail to comply. And while there is always uncertainty as to how human courts will interpret a human contract when things break down, a smart contract can be written in such that there is no leeway for misinterpretation.

The goal of a smart contract is therefore to set excruciatingly clear parameters and consequences, such that the interests of all involved are aligned towards participating in the protocol as intended. Even so, the contract can only guarantee that offenders will be penalized and victims compensated. It cannot magically make someone else do something that they won’t or can’t do. Therefore, users should carefully choose partners, even if the contract ensures protection. Engaging with the wrong person will waste time and immobilize your resources, even if the court grants you reparations in the end. Meanwhile the thing you wanted done won’t have happened and you may have to find someone else to do it for you. All this is true of both smart contracts and human contracts.

LegiCash seeks to use contracts as means to verify arbitrary computations on the blockchain; it doesn’t seek to run arbitratry computations, like Plasma does. Actual computations are to be run on private computers and side-chains; only the minimum necessary involves the main blockchains. The contracts only verify whether these computations did or did not happen when an aggrieved party posts a complaint. The good news is that verification does not require a “Turing equivalent” language to specify on-chain contracts. There is no need for unlimited recursion and the “deepest” necessary computations only involves checking Merkle proofs. When a suitable contract-checking language is devised and its effectiveness is demonstrated on an altcoin, chances are good that it will become a universal standard, and that it will even be adopted by Bitcoin. This means our technology will remain relevant even in the odd chance that Bitcoin maximalists are proven right in the future and other cryptocurrencies fade away.

Game Semantics and the Logic of Blockchain

Contracts are written in terms of mathematical logic. Each clause in the contract is a formula typically of the form ∀x P(x) → (∃ y Q(x,y)) ∨ S(x) where one party makes a claim P based on a “witness” x, and challenges the other party to come up with a response Q based on an opposing witness y, or else the other party is penalized according to sanction S. P and Q, are written as logical statements that the “judge” can check. S is an action that the judge can order as their sentence. The process of making a claim and then challenging the other party to respond is an interactive proof. The other party has limited time to respond (typically two hours), but if they don’t respond in time, anyone else can respond to make sure malicious actors don’t get away with fraudulent claims. The interactive proof can take as many steps as there are challenge steps, which is bounded by the number of alternations between ∀ and ∃ in the formula. While there can potentially be a lot of them, techniques such as Skolemization can help bring this number down.

The branch of mathematics that deals with seeing logical formulas as games that yield interactive proofs is called game semantics (not to be confused with “game theory,” as discussed above). There is even an approach to logic that takes game semantics as its starting point and defines the logical connectors and operators in terms of existing games, rather than trying to identify games that correspond to pre-existing logical frameworks. That approach is called computability logic. We believe that the best level of abstraction for specifying the logic of a dApp is a variant of computability logic. The primitive operations of that logic are the usual arithmetic and cryptographic functions and the logical connectors are those that can be argued through interactive proof games.

LegiCash seeks to use mathematical precision in defining the logic underlying every dApp. We will consistently extract all the moving parts of a dApp from a specification in the logic, including:

• Mathematical proofs that the dApp makes sense from the viewpoint of game theory.
• Code for each of the participants to act within the agreed-upon constraints.
• The “smart contract” code in the main chain’s virtual machine (e.g. EVM for Ethereum), that will serve as referee in case of dispute.
• The on-chain strategies for the “lawyers” of each party to play the interactive proof games when a lawsuit takes place.
• The off-chain strategies for the “smart lawyers” of each party to avoid “smart lawsuits,” to negotiate cheaper off-chain settlements whenever it makes sense, and to explain to users their rights and responsibilities under the contract.
• Continuous tests in a test network that comprehensively demonstrate that predictable attack scenarios are effectively prevented. It’s not enough to prove the code correct, it must be clear to all participants that the system will function as anticipated.

Legicash is focusing on these features because the smallest discrepancy between any of these aspects means a broken dApp and may result in massive financial losses for users of the dApp. Contracts in particular cannot be revised after they are executed, even to fix bugs, so it is particularly important to get them perfectly right the first time around. If even the top dApp specialists have lost $280M due to a bug in a 400 line contract, what chance do mere mortals like us have at writing non-trivial contracts without a fatal bug? We need tools that can prevent such bugs during development.

Legicash uses the Coq proof assistant as the foundational tool on which to develop our dApps. As of June 2018, our demo is written in a mostly pure functional style in OCaml and Solidity. Once the design is stable, we’ll translate as much of it as possible into Coq and then we’ll generate the OCaml and Solidity (or EVM) code from Coq in a way that can be proven correct. We thus differ from TrueBit and Plasma in that even though their authors understand the basic principle of game semantics, they don’t take advantage of the power of formal methods to weave together robust dApps.

The Court Registry: a Public Oracle for Data Availability

Enforcement of side-chain rules depends on publishing a concise cryptographic summary of side-chain activity, known as a “Merkle root hash,” and adjudicating disputes based on cryptographic proofs based on this summary of side-chain participants’ behavior. Constructing these proofs requires full knowledge of all side-chain activity, so it’s necessary for all participants to have access to a canonical view of side-chains at all times.

The challenge faced by all smart contract systems in which an open set of users can join or leave the contract, is that in order to audit the behavior of a side-chain manager, all the side-chain data must be publicly available. If a side-chain manager could illicitly update the state of their side-chain by posting the content address of that state without showing the actual content, they could post invalid content that credits them and Sybil identities with unearned tokens, and no one could prove them wrong before they make off with the funds. This is what the Plasma paper calls a “block withholding attack.”

Current attempts at developing Plasma prototypes involve a variety of “exit games” to mitigate such an attack: if and when the manager withholds data, users exit en masse to the main chain, using a protocol meant to prevent double spending. But ultimately, if such an attack is possible at all, then it becomes impossible to conduct interactive validity proofs in bounded time. The “exit games” allow honest users who carefully watch the chain to get their money out of the contract, but will cause the entire main chain to grind to a halt if the side-chain was trying to scale beyond what the main chain could handle. The fees would become exorbitantly high, and users with small accounts, those not connected during the mass exit, or those who fail to exit before the timeout, etc., may all lose their money to the malevolent manager.

The solution we offer is to prevent such attacks using a court registry, a network of servers that guarantee that the data is indeed well-formed and publicly available in its entirety. This allows users and third-party verifiers to check that the data is valid and raise any disputes in court before state updates are confirmed. In smart contract parlance, this court registry is an oracle, i.e. a way for the court system of smart law to verify facts about the world outside the main chain consensus itself. What this oracle establishes in this case, is that the data is indeed available for verification by third-parties. To that effect, the registrars, for a small fee, accept data from the facilitators, check that the data is indeed all present and well-formed, sign off on the data, and allow anyone to review that data. As long as at least one honest registrar signs off on the data, a block withholding attack is impossible. Facilitators must obtain signatures from at least half of the registrars to be able to validate their state updates. An attacker must therefore capture 50% of registrars (by stake) to be able to break the system by either withholding blocks or denying validation.

The court registry is a new component that comes with its own costs and benefits and its own guarantees and vulnerabilities. There are many challenges to building a secure court registry. However, as compared to more general oracles trying to relay outside information, a court registry relays information validated by the participants themselves, so this is a more tractable problem. Ultimately, the honesty of court registrars can be reduced to the same problem as the honesty of verifiers for a cryptocurrency blockchain, a problem that while not trivial, is considered solvable. The very same techniques used to secure a blockchain could be used to secure the court registry. Yet, a court registry is overall simpler and faster to achieve than a distributed consensus, since it only needs to build shared knowledge (information known by everyone), rather than the much more expensive common knowledge (information that everyone knows that everyone agrees upon). The parts of the protocol that do require a common knowledge will be resolved on the existing main chain (e.g. Ethereum) rather than on the new component that is the court registry.

We’ll talk more in detail about the court registry and how to properly use and implement it in a future article. For now, it is suffice to say that the court registry is a key component of the Legicash architecture that allows it to scale safely, and is missing in rival proposals.

Towards faster, cheaper, and safer dApps

The Legicash architecture enables users to write dApps in a faster, cheaper, and safer way. By using side-chains, regular operations take a fraction of a second. Additional safety precautions require the use of the court registry, which takes a few seconds. Complete safety still requires waiting for the consensus. But assuming the facilitator is honest, which is commonly the case since the facilitator is backed by a sizeable bond, users can trust operations to be complete as fast as the facilitator can confirm them. What will make Legicash dApps safer than other dApps, though, is the use of formal methods, and the fact that they cover not just the contract strictly speaking, but also all the off-chain parts of the dApp that interact with the side-chain.

Anyone on the Internet can duplicate our code, which is largely free software, and start their own facilitator network, then use it to write applications as Layer 2 solutions. But for security reasons as well as for performance, it is better for them as well as for us to join forces, and enjoy the network effects — especially since the main risk for the capture of the Court Registry is it being under-capitalized relative to the funds it is securing. To increase these network effects, we will offer a way to write contracts as Layer 3 solutions on top of our network. Our general-purpose facilitator contract will itself allow the definition of contracts on the side-chain. It will sport a simple virtual machine that is designed to verify computations only, not to carry them out, and will include all the required cryptographic primitives (digests, signatures, merkle proofs, zk-SNARKs, encryption, etc.) with no unbounded recursion. It will be able to deconstruct existing data structures without building new ones (beyond initial constants), and it will have subtraction or division of natural numbers without addition or multiplication. That virtual machine will be usable as the backend of our logic specification language.

In our next article, we will describe an example application for our technology: CryptoScalies, or Cute Lizards at Scale. In the meantime, we invite you to share your thoughts and continue the conversation on Telegram at https://t.me/LegicashCommunity.