Technology

The CertiK Chain incorporates trust in every layer of the technology stack to provide safer blockchain infrastructure

Read Documentation
The CertiK Chain incorporates trust in every layer of the technology stack to provide safer blockchain infrastructure

Components

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.

CertiK Security Oracle

  • Introduction

    Oracle

    ”A person or thing regarded as an infallible authority on something.”
    Oracles are utilized on the blockchain in order to send external (off-chain) data into and out of smart contracts.
  • The CertiK Security Oracle retrieves a set of security scores from a decentralized network of security operators, who assess the reliability of source code and are rewarded in CTK, the native digital fuel of the CertiK Chain. The Security Oracle relays these assessments and combines them to create a real-time, on-chain aggregate score that can be used by anybody seeking to validate the security of the contract.

    Depending on the risk tolerance of the interacting party—whether it’s a user or another smart contract—the security score can provide insight into whether transaction sizes should be smaller, split apart, or even stopped altogether.We can see this in action below:

  • The Security Oracle retrieved a low security score, and the security check saved the user from losing their assets in this dangerous transaction.

    The Security Oracle continuously aggregates the security assessments of a smart contract into the on-chain score—projects can get their code audited in an agile fashion to meet their aggressive timelines. By using a decentralized group of security operators, the suite of security primitives is constantly growing. New static analyzers and security tools can be created, and their assessments would also get incorporated into the ever-updating Security Oracle score. 

    The Security Oracle will build upon the security auditing work of CertiK, which has secured over $8B worth of digital assets across all sectors of blockchain, including the booming DeFi sector. Leading exchanges worldwide, including Binance, Huobi, OKEx, CoinOne, and Kucoin, have chosen to partner with CertiK’s expertise to audit blockchain projects, so these Security Oracle scores will be important proxies to the reliability of smart contracts.Security bugs never sleep, so neither does the Security Oracle.

    Components

    • Business Chain: The targeted blockchain platform (that can support smart contract functionality) where CertiK Chain provides the Security Oracle to, i.e., Ethereum.

      • Security Oracle Interface: The one and only smart contract serves as the interface to accept security inquiries from DeFi applications for upcoming transaction calls they need to make. If such an inquiry has no result or an expired result, then a new task could be broadcasted to CertiK Chain for fulfillment.
    • CertiK Chain: The underlying blockchain to our solution which offers built-in components to facilitate the handling of security inquiries from Business Chains. CertiK Chain itself is envisioned as the Guardian of the Blockchain Galaxy, and it provides a range of Combinators that are tailored to solve different perspectives of security problems.

      • Oracle Combinator: The built-in frameworks from CertiK Chain that facilitate the functionalities to fulfill general oracle workflows with characteristics on decentralization and transparency. Oracle movements such as task managements and result aggregation calculations will be broadcasted to CertiK Chain and recorded in states as proofs. By having a list of critical rules and reinforcements applied to the system, we could guarantee a professional and serious oracle network where good got prized and bad got punished.
      • Security Primitive: This is the platform for Security Providers to register their on-chain services or off-chain API endpoints as Security Primitives and then for Oracle Operators to invoke with. Security Primitives are diverse service functionalities that tackle security considerations from different angles. It is best practice to have a select combination of Security Primitives thus to make the best judgement over the security score of a given smart contract address and its function signature.
    • Cross-Chain: Communications and interactions are essential to the success of the Security Oracle network. Official authorized cross-chain components will be built and maintained by the CertiK Security Council, of which the members would be nominated by the broader CertiK community.

      • Oracle Operator: Everyone could register as an Oracle Operator on CertiK Chain and start to contribute to the whole network. Technically speaking, an Operator needs to run and maintain a software that interacts with a CertiK Chain node. Each Operator is free to use their own infrastructure or leverage tech stacks provided by CertiK Foundation for quicker onboarding.
      • Oracle Syncer: The Oracle Syncer is the Cross-Chain component that is solely owned and managed by CertiK Foundation’s Security Council. It could subscribe to the Security Oracle events on Ethereum and port to CertiK Chain. Vice versa, it also subscribes to transactions on CertiK Chain and pushes oracle results to the Security Oracle on Ethereum.
    • Offchain Internet: This is the traditional Web2.0 ground where computing operations such as security scans and analysis happen. Tools will be provided to Oracle Operators to support popular communication protocols like HTTP/RPC to connect with those Security Primitives for accessing security insights and proprietary technologies.
  • Workflow

    The mission of the Security Oracle is to give DeFi projects the insight (security score) on whether a potential transaction call is secure or not, thus gaining the confidence on the decision of issuing such a transaction. Here we describe the steps for the workflow via the perspectives of a targeted Business Chain and CertiK Chain.

    • Business Chain (i.e. Ethereum)

      • CertiK Foundation deploys and manages a Security Oracle contract that serves as the oracle inquiry interface and holds all security scores that processed via the oracle network;
      • The DeFi contract make a call to the Security Oracle to query for a upcoming transaction by providing the contract address and function signature offset;
      • Once receiving the inquiry, the Security Oracle would:
        • Respond back with the insight if such data record has already been monitored and logged. - Since there are a significant number of external dependencies shared by different DeFi projects, the chance for hitting the Oracle result table is considerably high;
        • Respond back with a default score indicating no suggestion at the moment. - Under the hood, such inquiry could be turned into a task on CertiK Chain and accepted by a group of Oracle Operators, who will then answer back their results;
      • The DeFi contract receives the result for the security insight and makes the next move with confidence.
    • CertiK Chain:

      • End users submit oracle tasks, funded with CTKs, for those security insights they wish to have on the Business Chain;
      • Oracle Operators will receive the task by subscribing to CertiK Chain events;
      • For each Operator, it will forward the task details to its customized Primitive Combination for real-time security checks;
      • After the generation of a  security score, the operator will respond to the oracle task by broadcasting a transaction to CertiK Chain;
      • With the closing on the task response window, CertiK Chain’s Oracle Combinator will gather all responses per that task and aggregate with a final security score; (Task bounties will be issued out to operators accordingly;)
      • A cross-chain bridge component, maintained by CertiK Foundation, will then push the final security score to the Security Oracle contract on the Business Chain.
  • Conclusion
    The Security Oracle we present is built to solve security pain points by bridging the gap between on-chain transactions and real time security checks via decentralized approaches. By adopting this innovative yet practical solution, DeFi projects will be shielded with more security guarantees by having security insights, with significant reference values, on every potential move to mitigate the risk factors. With its decentralized and distributed characteristics, we believe that CertiK Chain with its Decentralized Security Oracles will serve and link the security technologies and become an indispensable component of the ever-growing blockchain ecosystem.

CertiKOS

  • 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.

CertiK Virtual Machine (CVM)

  • 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.

DeepSEA

  • 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.

On-Chain Contract 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.

DeepWallet

  • 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

Built-In Smart Contract Security

  • 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.