CertiK Chain: DeepSEA’s Native Chain
In comparison to traditional finance, blockchain ecosystems are more risk-averse and have a lot more to lose due to the decentralized and open source nature. Due to the ability for people to share valuable and high risk data across an entire network, security must be at highest priority. However even blockchains with the best designed systems and rules can fail, and be at risk for hacks.
The CertiK Chain revolutionizes the way blockchains prioritize security. It establishes robust security in every layer, allowing anything built on top to focus on the promise of a robust blockchain. From the operating system to the built-in support for formally verified smart contracts, the chain promises unprecedented security.
Building on the promise of security, the CertiK Chain serves naturally as the native chain for DeepSEA — a functional programming language that allows rigorous reasoning about smart contracts at a high level of abstraction and generates trustworthy code with machine-checkable mathematical proof.
CertiK Chain’s DeepSEA Support
DeepSEA is unique, because unlike other programming languages it is designed specifically for writing certifiably correct code.
Today nearly all contracts are written in programming languages that were designed without Formal Verification in mind. And languages that do integrate with Formal Verification are geared towards dealing with simple cases. DeepSEA provides the flexibility to verify complex programs, like cross-chain interactions or voting schemes, by realizing the full potential of interactive high-order logic proof assistants. The DeepSEA compiler generates both executable bytecode and a corresponding formally verifiable model so that developers can obtain mathematically proven correctness through the proof assistants. To learn more about DeepSEA, review CertiK’s explainer article.
By integrating DeepSEA, the CertiK Chain prioritizes first class safety without any compromises. When using DeepSEA, the deployer (or other users) may write a correctness-proof based on the generated compiler output and push it onto the chain. The proof will be then validated and published, completing a certification for the smart contract. Eventually users and smart contracts may be able to choose whether to interact with another contract based on its certification and the associated proof.
EVM-Compatible Bytecode
The DeepSEA compiler has a verified backend to generate EVM-compatible bytecode. The programs are ABI-compatible with Solidity, so contracts written in Solidity can call contracts written in DeepSEA or vice versa.
DeepSEA programs can be deployed onto the traditional Ethereum Network. But because the CertiK Chain’s CVM is EVM-compatible, they also run on the CertiK Chain. Importantly, DeepSEA contracts running on the CertiK Chain have a few upgraded capabilities compared to traditional Ethereum contracts:
- The chain has built-in support for recording that a program has been formally verified to satisfy a particular specification;
- Contracts can make checks at runtime to query whether a particular address satisfies a specification or not.
The DeepSEA compiler outputs a higher-order logic specification for the program which is a one-of-a-kind specification that can be registered with the chain. In the other direction, a DeepSEA program can query if an address has been formally verified or not. For example, this could be used to only interact with those contracts which have proven themselves to be callback-free.
A Blockchain of Proofs
In previous systems, each user had to either check the proofs themselves, or trust a third party to do so. This is potentially error-prone, since the user needs to vet the proof-tools and libraries to make sure that they didn’t smuggle in any bad assumptions, and in any case it does not work if smart contracts want to query proofs at run-time.
To solve this, the CertiK Chain will include proof checking as a first-class capability. A long logical proof of a theorem is split into multiple pieces, each piece is checked by a few verifier nodes, and if all the verifier nodes agree, the theorem is recorded as proven in the next block of the chain.
This means that, in a world-first, the CertiK Chain will build a consensus about which claims have been proven. Once a theorem has been added to the chain, everyone knows exactly what assumptions went into it, other users can use it as an assumption in their own Formal Verification developments, and contracts can query it at run-time.
Deploy and Interact with DeepSEA
DeepSEA can be directly deployed using the CLI, or through the DeepWallet.
The CLI makes a call to DeepSEA compiler, and gets the bytecode and ABI. Deploying a DeepSEA contract uses the same command as deployment for Solidity; it’s just as easy/straightforward:
certikcli tx cvm deploy <ckt> <filename>Alternatively, developers can compile their own bytecode (optionally ABI), save it to a file, and deploy using the same command (optional — abi flag). Functions deployed via DeepSEA or Solidity contracts can also be called using same command:
certikcli tx cvm call <address> <ckt> <function>DeepSEA can additionally be deployed through the DeepWallet. DeepWallet is a secure wallet application that allows users to send, receive, and stake tokens with the added functionality of building secure programs with DeepSEA. Users can interact with DeepSEA directly through DeepWallet’s user friendly interface.
Building Limitless Possibilities
Clearly, security is fundamental in order to fulfill a blockchain’s promise of a transparent and safer system. Because the blockchain requirements are so demanding, they can ultimately only be met by computer-checked, mathematically proven security.
Developed partly with grants from the Columbia-IBM Blockchain Center and The Ethereum Foundation, DeepSEA brings us closer to building a secure blockchain infrastructure with a level of security that other languages can’t achieve. The integration of DeepSEA and CertiK Chain empowers all Chain users to build programs and new killer apps based on the ultimate trust and proof, pursuing unlimited possibilities with a bold imagination.
Want more information? Join the Chain mailing list for further details and upcoming announcements!
Originally published at https://certik.foundation on March 30, 2020.
