CertiK has completed a security audit for Terra
Certik has 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. The full audit report provided by Certik can be accessed here.
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.
Here are some of the 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 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 economy 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.
About Terra:
Terra is designing a price-stable digital currency that will power the next-generation payment network on the blockchain. Terra partners with an ever-growing alliance of global e-Commerce platforms to bring blockchain’s benefits such as low transaction costs to merchants and everyday consumers. By bridging the gap between digital currencies and real-world application, Terra aims to evolve into an open platform for innovative financial dApps and grow the real GDP of the blockchain economy. Founded by a team of business, finance and blockchain experts, Terra has offices in Singapore and Korea. For more information, go to https://terra.money
About CertiK
CertiK is a blockchain and smart contract verification platform founded by top formal verification experts from Yale and Columbia University. Incubated by Binance Labs, Certik has strategic partnerships with the world’s top crypto exchanges such as Binance, OKEx, and Huobi, as well as Public Chains such as NEO, ICON, and QuarkChain. Different from the traditional testing approaches, CertiK’s formal verification method mathematically proves blockchain ecosystem and smart contracts are hacker-resistant and bug-free. CertiK’s key features include a layer-based decomposition approach, pluggable proof engine, machine-checkable proof objects, certified dApp libraries, and smart labeling.
To request the audit/verification of your smart contracts, please email audit@certik.org or visit certik.org to submit the request.
Twitter: https://twitter.com/certikorg
Telegram: https://t.me/certikorg
To read more articles from CertiK:
Official Partnership Between Binance and CertiK
CertiK Has Conducted Successful Audit of Crypto.com
CertiK Has Completed a Security Audit of Celer Project
CertiK AutoScan Engine: 53 of the top 500 tokens by market cap were found to have vulnerabilities
