Why CertiK?

CertiK has one Mission;
To deliver provable trust across all facets of blockchain.

CertiK Ecosystem Overview

CertiK utilizes a suite of applications, such as CertiK Security Oracle and CertiKShield, alongside a hyper-secure technology infrastructure, including CertiK Chain, DeepSEA, CertiKOS, and CVM to provide end-to-end, compatible security solutions that establish the infrastructure of provable trust for all.

CertiKShield

Decentralized reimbursement mutual system for digital assets

Security Oracle

Real-time and on-chain security insights for Smart Contracts

CertiK Chain

Security-oriented blockchain that enables provable trust for all

Skynet

Multi-dimensional tech suites on security monitoring and analysis

DeepSEA

A programming language to write verifiable and secure Smart Contracts

CertiKOS

The world’s first fully certified hacker-resistant, multi-core OS kernel

CertiK Security Oracle

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

CertiKShield

  • Introduction
  • The estimated amount of cryptocurrency which has been stolen by malicious actors from 2018–2020 has reached a grand total of $7.1B. Due to the pseudo-anonymous, immutable nature of blockchains and the crypto assets which power them, the vast majority of users who lose their funds — whether from a hack or misplaced private key — never retrieve their assets.

    CertiKShield fixes this.

    A CertiKShield Pool is a decentralized pool of CTK that is used to reimburse lost, stolen, or inaccessible assets from any blockchain. The amount that’s lost can be reimbursed by the members of the CertiKShield Pool.

  • So, how does it work?

    There are two parts of the CertiKShield system: 1) members who fill the pool with CTK as collateral to be used to reimburse approved Claim Proposals, and 2) members who seek to protect their crypto assets by reserving a part of the CertiKShield Pool.

  • The Workflow
    Let’s start with the members who are filling the Pool. Just like liquidity providers in DeFi, these members are staking their CTK. In addition to normal staking rewards, these members also gain a portion of the fees paid by the other members who reserve a portion of the Pool to protect their crypto assets. These members who are filling the Pool must recognize the risks associated with being liquidity providers: their staked CTK may be used to pay out approved claims of reimbursement. High risk, high reward.

    Now let’s talk about the members who seek to protect their crypto assets. Each CertiKShield Pool is intended to protect the users of a specific crypto asset (like BNB, for instance). If you’re a BNB holder and you are  a member of the CertiKShield Pool, you can reserve a part of the funds to request a reimbursement if your BNB gets lost or stolen. You’ll pay a fee, and as mentioned, this will go directly into the members who have pooled their own CTK as liquidity providers.

    Reimbursement eligibility is defined by the provable and irretrievable loss of crypto assets — this can be from a hack, a malfunctioning contract, or other unfortunate event, but losses from social engineering (sim swap, Telegram/Twitter scam, etc.) or a misplaced private key are not eligible because proof of a legitimate loss, as opposed to a coordinated “loss,” is not absolute.

    Members seeking reimbursement must submit Claim Proposals, which are voted by the decentralized group of CertiKShield members to approve or reject the claim. All submissions require fees, protecting the system against illegitimate claims and gaming of the system.

    The blockchain world is filled with early adopters and long-term holders, so the CertiKShield offers a safer way to protect your crypto assets from any unexpected losses.

Skynet

  • Introduction
    Skynet is a unified set of security tool chains that leverages automated technologies to check deployed smart contracts against a wide range of known vulnerabilities at scale. It produces accurate smart contract security scores, which indicate the risk potential for hacks and code malfunctions.
  • How does it work?
    Skynet  consists of a combination of static and dynamic technologies, which we call Security Primitives. Security Primitives are similar to security service endpoints, but are used for scanning smart contracts. Each Security Primitive assesses a specific security area against a smart contract and assigns a security score between 0–100.

    Currently, there are five QuickScan Security Primitives from two categories (Static and Dynamic). We are actively integrating new Security Primitives into QuickScan. That being said, a smart contract will be scanned against 5 thorough security checks for one run of the QuickScan. Depending on the complexity, it may take up to 6 hours for completion as Security Primitives requires huge volumes of computational resources.
  • Usage of security scores
    Security scores are accessible both on-chain and off-chain:
    • Off-chain: Public data endpoints are available to retrieve security scores for each QuickScan Security Primitive. Blockchain projects can reference those scores and enhance their security, while end-users can interact with projects with more confidence and trust based on security scores.
    • On-chain: Security Scores will be aggregated on CertiK Chain and constantly synchronized to security oracles deployed on different blockchain platforms like Ethereum and Binance Smart Chain. Smart contracts can leverage near real-time data as risk indicators to prevent potential external transactions.
  • Skynet QuickScan Primitives
    Static analysis and dynamic monitoring are security industry standards, and the following 5 Security Primitives cover both of these.
    • Whitelist Primitive | Dynamic

      • Scores based on certificates issued on CertiK Chain
      • The more certificates a smart contract has, the higher the score
      • Sample certificates: audit, source code verification, compiler verification
    • Blacklist Primitive | Dynamic

      • Scores based on CertiK in-house security intelligence monitoring systems
      • Technologies utilized: social monitoring on Twitter/Telegram, Anti-Money-Laundering databases, anomalous transaction detection
    • Quality Primitive | Dynamic

      • Scores based on qualitative aspects of a smart contract
      • Manual work involved and updated frequently
      • Criteria: open source, user activity, documentation, team anonym
    • Bytecode Analysis Primitive | Static

      • Scores based on static analysis tools detecting errors in bytecode
      • A lower score means more weakness entries detected
    • Source-Code Analysis Primitive | Static

      • Scores based on static analysis tools detecting errors in the source code
      • A lower score means more weakness entries are detected
      • Technologies utilized: formal verification, fuzzing tests
  • Conclusion
    We envision Skynet  to be both the initial step prior to a full security audit and a necessary component once your smart contracts go live. With its combined nature of static analysis and dynamic monitoring, Skynet fills the gap on real-time security insights and enables more trust for your community and organization.

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.