Solution: Secure Smart Contracts

Half of the time DeFi is in the news is because of hack that has caused a massive leak of funds from a DeFi protocol. No matter the size of the attack and whether or not it was fixed, the project and protocol never recover. Many of these vulnerabilities are direct consequence of the language they were developed in, Solidity, being Turing complete.

Turing completeness describes the ability of the language to express all tasks accomplishable by computers. This sounds powerful in theory, creating no bounds to what could be done on the blockchain (if we ignore gas). But what started as a powerful idea has actually turned into a problem. With this open-ended ability came hard to anticipate attack vectors. To date, there are 16 known attack vectors in Solidity, which much of the DeFi ecosystem is built upon, most of which would not be possible if Solidity was Turing incomplete.

Figure 2 – Unnecessary risk associated with turing completeness

With Turing completeness comes unnecessary risk.

Kadena’s smart contract language, Pact, seeks to improve on this problem by designing a language with the known limitations of blockchain in mind, resulting in a Turing incomplete language that is purpose driven to produce easy to read, secure and efficient smart contracts. This is amplified by the built-in support of formal verification, giving developers immediate feedback on possible bugs that would otherwise go unnoticed. This overlooked detail ensures eckoDEX will be not only secure transactionally via PoW but also secure from attack.