Certik, a blockchain and smart contract verification platform founded by top formal verification experts from Yale and Columbia University, recently completed a security audit of Terra, the company that has designed an algorithmic stablecoin to power the next-generation payment system on the blockchain.
Terra’s mainnet, which went live in April, is a Delegated Proof-of-Stake (DPos) system that utilizes the Cosmos SDK and Tendermint Consensus Engine.
Auditing Process
The audit work was conducted by experienced economists, security researchers, and security engineers from CertiK, with collaboration from the Terra research and development team. CertiK performed a comprehensive review of Terra’s economic model to test against potential market manipulations, an architectural review with special attention put on ensuring all implementation of Cosmos plugins were well-protected against possible edge scenarios and attacks, as well as careful manual review by experts on Go — the language in which Terra’s code is written in.
Highlights
- The audit work spanned multiple months, starting with an earlier version of Terra documents and implementation. Through an interactive weekly syncing between the CertiK and Terra team, intermediate audit opinions were communicated, and discussed during the auditing process. The audit work wrapped up on the final Terra documents and implementation, which were used to launch the Terra mainnet.
- CertiK studied the Terra whitepaper as well as other research, analysis, and design documents from Terra, to comprehend the complete semantics of Terra. From an economics theory’s standpoint, CertiK validated the correctness of the mathematical reasoning and the model’s robustness against potential high-level ill-intentioned currency manipulations.
- Another focus of the audit was on validating that the implementation of each Cosmos plugin conforms to and fully implements aspects of Terra protocol’s theoretical model. Special attention was also put on making sure the implementation was well-protected against possible edge scenarios and attacks.
- Overall, Certik found Terra’s theoretical model as well as the Go implementation to be well designed and executed. While Certik does not comment on the final performance of the Terra blockchain, the modeling and mathematical reasoning are considered sound. The implementation was well-structured and demonstrated a good command of Go programming patterns as well as common good programming practices.
- CertiK used multiple methods during the audit, which include, e.g., automated static analysis, mathematical reasoning, as well as careful manual review by experts on Go, formal verification, and security.
CertiK was highly impressed by Terra’s clever and highly effective design of economic theory, especially the proper decoupling of controls for currency stabilization and predictable economic growth. CertiK also found Terra’s technical implementation to be one of the highest quality ones it has seen, which demonstrated extremely principled engineering practices, mastery command of Cosmos SDK, as well as diligent documentation efforts.