The CertiK Chain incorporates trust in every layer of the technology stack to provide safer blockchain infrastructureRead Documentation
The CertiK Chain leverages and provides the safest infrastructure for the blockchain ecosystem, including the CertiK Virtual Machine, CertiKOS, and DeepSEA programming language. Only with verified layers can blockchain fulfill its promise of a fairer, safer, and more transparent system.
- Functionally-Correct OS Kernel
CertiKOS is the world’s first fully certified multi-core OS kernel assured to be safe, functionally correct, and hacker-resistant. The operating system incorporates Formal Verification to ensure that programs perform precisely as intended.
Computer scientists have long believed computer operating systems should have, at their core, a small trustworthy kernel that facilitates communication between the systems’ software and hardware. But operating systems are complicated, and all it takes is a single weak line in the code — one that is virtually impossible to detect via traditional testing — to leave a system vulnerable to hackers.
- Concurrent System
The CertiKOS supports concurrency, meaning the system can simultaneously run multiple threads — small sequences of programmed instructions — on multiple central processing unit (CPU) cores. This sets CertiKOS apart from other previously verified systems and allows CertiKOS to run on modern multi-core machines.
Additionally, the CertiKOS architecture is designed to be highly extensible — that is, it can take on new functionalities and be used for different application domains, not just blockchain.
- OS Verification
Deep specifications and abstraction layers are the key innovations that let us verify the CertiKOS. When writing code, developers simultaneously write specifications stating exactly what the program is doing. Then, proofs show that the code correctly implements this specification. However because the specification is “deep,” developers only have to write such a proof once, afterward, all the work can be done using only the specification, without having to deal with the code again.
A library, written in the Coq proof assistant, then allows users to compile all the individual layers from each specification to get a correctness proof for the entire layer. This method is used to verify the CertiKOS, where the kernel is made up of hundreds of layers that are composed together.
- Security as an On-Chain Value
None of today’s virtual machines expose security as a runtime value or include it as part of blockchain semantics. Formal Verification is done outside of a virtual machine and is invisible to the chain operation and VM execution.
We believe establishing smart contracts and blockchain security brings more dynamic, actionable value to chain operation and VM execution. For example, a secure smart contract may choose to interact differently with secure and non-secure smart contracts. In real life, this kind of differentiation based on security levels is common and useful.
The CertiK Virtual Machine (CVM) exposes smart contracts and blockchain security information to the VM code, enabling unprecedented ways to access, check, depend on, and even dynamically establish blockchain and smart contract security. The interaction of security and other blockchain semantics will result in safer, simpler, and more efficient VM code, which leads to new true killer apps for the blockchain world.
- Advanced Security of and for VM Code
The CVM supports advanced formal verification via mathematical proofs, where the trusted computing base (TCB) is minimal, which is how CertiKOS and the DeepSEA compiler are fully mathematically verified.
In particular, CVM supports bytecode and proofs generated by DeepSEA’s certified compiler. The CVM itself will be required to run on top of CertiKOS, the world’s only fully-certified, concurrent OS kernel. Eventually, the CVM will enforce sandboxing and isolation of any code not fully certified via mathematical proof by being completely formally verified via mathematical proof.
The CVM establishes a hierarchy of VM code security so that different vendors and technologies can coexist and collaborate with clarity. In one extreme, trustless VM code with a complete mathematical proof will be of the highest levels of security and can help achieve true decentralization for the blockchain world. In the other extreme, even non-secure VM code, which has no verification or auditing, may still be allowed to execute in CVM with proper protections against it and still be able to collaborate with other secure smart contracts in CVM.
- A Language to Write Verified Smart Contracts
DeepSEA is a functional programming language that allows developers to handle extremely complex code while formally verifying through the Coq proof assistant. Originally designed for implementing systems software such as OS kernels, DeepSEA uses the same set of features that are used for encapsulating state inside a kernel for implementing smart contracts in the blockchain ecosystem.
The language provides a streamlined solution that automatically generates both executable code and a formal model that can be loaded into the Coq theorem prover. By integrating smart contracts and Coq, users can apply Formal Verification to the most challenging tasks, allowing for a completely verified program.
- DeepSEA Principles
DeepSEA was built with four key principles that combine the best features of several other programming languages.
- Equational Reasoning: Each DeepSEA term translates into a corresponding functional specification, which can then be reasoned about in the Coq proof assistant.
- Layered Specification: DeepSEA keeps proof manageable by abstraction layers that provide a high-level view of the program. The compiler proves that the raw bytecode implementation behaves as intended, while the developer only needs to look at the high-level representation.
- Encapsulation and Composition: Each DeepSEA layer consists of a set of objects that are built on top of another layer, and the layers can be proven correct one at a time.
- Built-In Abstract Refinement: DeepSEA verifies larger systems in user-friendly steps. The process is structured as a series of linked refinement proofs that prove a linked program meets the specification.
- With the CertiK Chain, smart contract publishers have the option to store ABI (the Application Binary Interface) on-chain along with deployed smart contracts. This feature, not found in many other blockchain ecosystems, allows users to interact more easily with smart contracts without needing to keep track of and manually copy-and-paste ABIs every time.
- Users can easily view their token balance, redeem delegated rewards, and send and receive tokens to other users from their DeepWallet, which is accessible through a web browser. Unlike traditional wallets, the DeepWallet has additional enhanced features to allow users to delegate stakes as well as deploy smart contracts. Check out DeepWallet
- Beyond initial auditing and verification, smart contracts on the CVM can validate other smart contracts’ security, in either cryptographic and mathematical forms, for ultimate security assurance. On-chain smart contracts will contain cryptographic certificates as proof of verified security.
The Chain additionally provides different permissions, allowances, and limits of smart contracts based on different security levels. For example, an advanced secure contract with open formal specifications can restrict the outflow of funds to any basic contract, ensuring a deeply secure transaction.