Injective is Audited by Informal Systems

Informal Systems has audited the Injective code base and the Injective chain.

TLDR: Informal Systems is a leading auditor specializing in Cosmos-SDK based projects. The Informal team is composed of world-class researchers, engineers and operators, led by CEO Ethan Buchman, who co-founded Cosmos and Tendermint.

Injective has performed rigorous internal testing to ensure the security and robustness of the exchange protocol. Informal has overall found the Injective code to be of high quality. The focus of this audit was to review the codebase for both spot and derivative markets. The spot markets milestone focused mainly on the audit of the exchange module while the derivative markets milestone focused on auditing the exchange, along with the oracle and insurance modules. Very minor errors were found in the code base and were quickly fixed by developers.

Moving forward, rigorous testing will continue to be performed on the codebase to ensure the stability of the exchange. Community developers and contributors will continue proceed with caution with regards to security to ensure the safety of funds.

The article here will delve into the background of Informal and provide some further details on core takeaways from the audit that was conducted.

Full Audit Report: Link

Introduction to Informal Systems

Informal Systems is a full-suite Research & Development institution and a leading contributor to the Cosmos and Tendermint project. Since its founding in 2019, Informal Systems has become a leader in building verifiable distributed systems, including core blockchain infrastructure in Rust and formal verification tools such as Apalache. While the majority of auditors rely on manual testing of codebases, Informal stands as a pioneer by leveraging a combination of English and TLA+ specifications, Model-Based-Testing and code inspections. They reconstruct protocols from the original codebase in order to make protocol assumptions and guarantees more explicit. This unique auditing model has allowed them to comprehensively explore the codebase and identify potential issues.

The Informal team is composed of world-class researchers, engineers and operators, led by CEO Ethan Buchman, who co-founded the Cosmos and Tendermint projects, along with Arianne Flemming (COO), and Zarko Milosevic (Chief Scientist).

“We were very impressed by the depth of understanding that Informal Systems demonstrated during their month-long audit of our protocol. Not only did they possess expert-level knowledge of the nuances of the Cosmos-SDK but they also leveraged their unique skills in formal verification to create precise state representations of our protocol which were invaluable for programmatically generating rare cases that would be otherwise challenging to encounter through manual or fuzz testing. It was a privilege to work with the Informal team and we are grateful for their contributions in helping us bolster the security of our protocol,” said Injective co-founder and CTO Albert Chon.

The Injective Audit by Informal Systems

Injective contributors have worked tirelessly to improve the performance of the exchange protocol, prioritizing an unparalleled and inclusive financial ecosystem. This mission cannot be achieved without robust security standards acting as a core backbone of the vision.

Today, most DeFi projects differ from Injective's security approach by rushing the development stage and often disregarding the importance of security. Due in part to this practice, countless protocols have suffered from vulnerability attacks over the past few years.

Injective has undergone rigorous testing to ensure that funds traded on the exchange are highly secure. Informal Systems went on to note in its audit report, “We quickly found that the general code quality was high and the Injective Labs team tested their code on a regular basis…”.

The focus of this audit was to review the codebase for both spot and derivative markets. The spot markets milestone focused mainly on the audit of the exchange module while the derivative markets milestone focused on auditing the exchange, along with the oracle and insurance modules.

The report outlined that the straightforward attempts to attack the Injective system did not succeed, as the codebase contained all the necessary validation tests and was written with a high level of attention to detail.

The majority of the findings were not severe, as they only affected the client interface. There were specifically five issues highlighted by the auditor that required knowledge of the source code and the ability to execute carefully crafted sequences of transactions in order to exploit. Therefore these were not found to be easily exploitable, as they would not have been found by standard static analysis or fuzzing. Nonetheless, the reported issues were immediately fixed in order to further bolster network security.

Informal Systems Principal Scientist Igor Konnov said the following: “We enjoyed working with Injective Labs on the audit of the Injective Protocol. They provided us with near instant feedback on their code and minor issues quite quickly. Thanks to this feedback, we could quickly figure out that several standard attack patterns were not feasible. In general, the code had extensive validation logic (except for the inputs from price oracles, as we found in the later stage of the audit). Hence, we focused on more complex attack vectors that required automation.

When we noticed several potential issues in the code, which were hard to trigger, we decided to proceed with a more systematic approach to bug discovery. We opted for model-based testing. To this end, we wrote high-level specifications of spot markets and derivative markets in TLA+. Further, we ran the symbolic model checker Apalache to produce scenarios that would lead to the potentially problematic system states. By doing so, we have found four major issues that could halt the blockchain or freeze tokens. All of these issues have been resolved by the Injective Labs team. The most severe issues required a deep understanding of IBC and ABCI and Injective codebase, so we believe that they were not easy to trigger.

While manual code inspection and model-based testing cannot guarantee absence of bugs, we observed that the Injective blockchain could in general cope with adverse scenarios, especially after the discovered issues had been fixed.”

With the release of DEX ahead, it is crucial to ensure that every component of the exchange is secure and reliable. The Informal audit report provided evidence of this, which inspires confidence about releasing the Injective DEX on the Canary Chain, inching one step closer to the long-awaited Canonical Chain release.

Conclusion

Moving forward, Injective contributors will continue to prioritize rigorous testing on the codebase to ensure the stability of the exchange. Caution is of the utmost importance with regards to security to ensure the safety of funds.

The canonical chain will be the next major milestone for Injective, thanks to the heavy lifting and support of the community in this final home stretch. Injective has pledged to deliver a highly secure and performant protocol that will shape the future of finance, and it's thrilling to have reached such a monumental step in this direction.

About Informal Systems

Informal Systems has become a leading auditor in the DeFi space and is the most prominent auditor for Tendermint-based projects. The Informal team is comprised of world-class researchers and engineers, led by Ethan Buchman, who co-founded the Cosmos project, along with Arianne Flemming, and Zarko Milosevic. Ethan, Arianne, and Zarko previously served as the Technical Director, Managing Director, and Head of Research at the Interchain Foundation, respectively.

About Injective

Injective is a lightning fast interoperable layer one blockchain optimized for building the premier Web3 finance applications. Injective provides developers with powerful plug-and-play modules for creating unmatched dApps. INJ is the native asset that powers Injective and its rapidly growing ecosystem. Injective is incubated by Binance and is backed by prominent investors such as Jump Crypto, Pantera and Mark Cuban.