Here at METASTATE, besides protocol development, we are also developing a smart contract language called Juvix. A few talks I went to at Devcon 5 have me reflecting on some thoughts of smart language design. I'd like to tie them up with our Juvix work and share them in this post.
Smart contract developments are fundamentally different from other software developments. First, smart contracts often have very high stakes. Mis-specifications are thus extremely costly. Second, smart contracts are public and the incentives to hack them are high because of the monetary rewards. Defending against vulnerabilities of smart contracts is mandatory.
The 3 talks I summarized below offer solutions/tools to some of these issues - however, I believe that we can do a lot better than gambling that developers will go through all the measures entail in these talks plus the many other that were presented at Devcon 5! Read on to see the better alternative!
Talk 1: Formal Verification of Smart Contracts and Protocols: What, Why, How by Grigore Rosu, Everett Hildenbrandt
Summary:
Program analysis techniques are used to minimize mis-specifications, but have trade-offs between cost and assurance. The less costly techniques offer less assurance but the techniques that offer more assurance are costly. The techniques from the least assurance to the most assurance (as on the presenter's slide) are:
- Testing
- Runtime Monitoring
- Static Analysis
- Symbolic Execution (bounded model checking)
- State-of-the-art Verification (language & property specific)
- Formal Modelling and Validation
- Verification/Proving using frameworks (E.g., Isabelle, Coq, K)
Techniques 1 - 4 can be automated and should be. Given that smart contracts usually have high stakes, it makes sense to also use frameworks to get the most assurance. A few automation tools/frameworks were demonstrated.
Implications on smart contract design:
Many of the program analysis techniques are not perfect. Specifically, with formal modeling and validation, the proofs may not be valid because there can be a gap between the actual language and the model that is being checked. A well-designed smart contract language should assist developers overcome these challenges. For example, a language with support to write proofs as you write the program would not have such a problem.
What we are doing in juvix:
Juvix has a built-in proof system that allows formal verification of contracts. Because the specification and the contract are written in the same language, there is no gap between the checked formal model and the program. This minimizes mis-specifications as you write your contracts.
Juvix also incorporates cutting edge programming language advances which help you write correct contracts:
-
dependent-linearly-typed core language increases expressive power of developers and assurance of correctness.
-
modern high-level frontend syntax lowers overheads on developers and make them less likely to make errors.
Talk 2: Smart Contracts: Coding Best Practices and Security Recommendations by ConsenSys Academy
Summary:
This talk introduced some of the best coding practices Solidity developers should follow. These practices focus on minimizing mis-specifications, enhancing efficiency, and reducing vulnerabilities.
For example, developers should:
- order variables such that gas consumption is minimized. E.g., pack 16 bytes variables together, not in between 32 bytes variables.
- use the SafeMath library to prevent overflows.
- receive calls before making calls
- make sure data is empty in the
fallbackfunction. - make entries of the transaction before the actual transaction to prevent re-entry attacks.
- use
tx.originwith care because it can lead to attacks. - check that the contract doesn't have known weakness from the SWC registry.
Implications on smart contract language design:
A few design choices of Solidity lead to vulnerabilities! Developers should not need to keep in mind many of the practices above. The language itself should have the precautions built-in. For example, the language can optimize gas consumption for the developers. It should have a built-in math library that doesn't have overflow problems. It can make sure that calls are received before they are made. There should not be a fallback function - that way it's always empty. To avoid attacks caused by the use of tx.origin, use appropriate syntax structure to enforce that appropriate measures are added when the function is called.
As for known weaknesses, there are tools that scans for vulnerabilities in the SWC registry. E.g., MythX and Mythril scan for vulnerabilities in EVM-based blockchain smart contracts. And OpenZeppelin Contracts is a library for secure smart contract development in Solidity. Similar to the tools for verification above, one can design a smart language such that the language itself does most of these checks for you after you've written the contract and proofs. These checks should be agnostic to ledgers.
What can we do in juvix?
Most of the syntax/function implementation problems won't be a concern for Juvix because Juvix is a dependently typed pure functional language.
As for vulnerabilities, we can go through the SWC registry (or other similar databases) and translate the known weaknesses into properties in the type system of Juvix. Juvix can enforce that the weakness properties are proven to be false. For example, this weakness concerns contracts using random number generators that are predictable - users may not remember to check that certain values are truly random and Juvix can enforce proofs of that. Whenever possible, all known issues would be checked as the library gets updated. More implementation details to be determined.
Talk 3: Designing Smart Contracts with Free Will by Philip Daian
Summary:
Mechanism design concerns some party (principal) designing rules such that the incentives for all the parties involved drive the desired outcomes to be achieved. For example, Vickrey–Clarke–Groves (VCG) auctions use the VCG mechanism (all buyers send in secret bids and the auctioneer sells the item to the highest bidder at the second-highest bid price) to achieve the socially optimal outcome.
Mechanisms can be broken (by so-called anti-mechanisms) when not properly defended against, and this poses challenges for smart contract mechanism design. The ease of coordinating bribery means that protocols can break and cause unexpected/undesired outcomes. For example:
- Oracles: bribe certain responses, bribe unavailability, bribe which point is sampled from continuous series, etc.
- Voting: buy votes, influence governance, etc.
- Identity: Lease identities, buy permissions at fine-grained granularity, etc.
Particularly, MPC and SGX remove user free will (the ability of a user to learn their own secrets) in cryptographic systems. One can use “Complete Knowledge” (CK) proofs for secrets to regain free will. See this tweet for details.
CK proofs are required to build bribery/collusion-free cryptographic protocols. If you do not use CK proofs, your permissionless protocol is almost certainly vulnerable to bribery and coercion.
Implications on smart contract design:
The smart contract language can provide native support to CK proofs or other defences against anti-mechanisms. Further, because briberies will likely happen without defences, the smart contract language can check that these defences are in place and warn developers of absence of such.
What can we do in juvix:
Juvix already has future plans of supporting inline zero knowledge verifiers and proofs with built-in functions and types. We can extend this to CK proofs. Juvix's proof system also allows reasoning about properties like complete knowledge in types.
We may also enforce that the contracts will not be attacked by anti-mechanism by checking that the profits from breaking the contracts is lower than the costs of the attacks. Implementation details to be determined.
Conclusion
Smart contracts suffer high costs from mis-specifications and have to defend against vulnerabilities. Moreover, there are issues other than the ones I touched on above that are not easily addressed. A well-designed smart contract language should provide infrastructure to defend against any known issues. Automation at the smart contract language level not only saves developer overheads, it also provides more guarantee on contract soundness.
Our approach with Juvix is "correct-by-construction". Currently, developers have to reason about all these different cases and specific vulnerabilities because they don't have ways to prove composite properties of contracts - developers who write in Juvix and prove properties of their contracts will have a much stronger guarantee. Because Juvix is ledger agnostic, it can be the go-to language for all smart contract developers.
Juvix is still under active development. There is plenty of chances for us to improve the language. Feedback and contributions are welcome as we bring this smart contract language ideal to fruition! Stay tuned for our upcoming blogposts!
Written by Marty Stumpf, core developer and researcher at Metastate.
Metastate has ceased its activities on the 31st of January 2021. The team members have joined a new company and working on a new project. If you're interested in programming language theory, functional programming, type theory, formal verification, or compiler engineering positions, check out the open positions at Heliax.
If you have any feedback or questions on this article, please do not hesitate to contact us: hello@heliax.dev.