Posted on November 4, 2021 by Silvia Barredo
Posted in Audits
Runtime Verification is thrilled to announce the audit completion of Element’s Finance Governance Protocol’s Smart Contracts. This blog post will dive into why it’s crucial to audit Governance protocols and a detailed audit description.
Decentralized Governance Protocols are on the rise, and with it, a higher risk for exploits associated with contracts holding funds from the treasury and community. When participating in a Governance protocol, users can minimize the risk of choosing a protocol that could be exploited by checking if a series of factors are met. Let’s take a look at some of the factors:
Users that want to get involved in a project’s community and trust a protocol with their funds should choose projects that take security seriously. The most reliable projects will often follow best practices such as external audits and other actions to reduce the smart contract risk as much as possible (given that it’s impossible to prove that a protocol code is 100% free of vulnerabilities). We want to highlight that Element Finance has taken all the precautions described in the sections above to minimize any possible risks, taking security seriously and prioritizing the well-being of its users.
The audit’s sole focus was Council, Element’s new governance protocol. The goal of the audit was to check if the smart contracts had any vulnerabilities that could drain the funds or represent a risk for its users. Some of the audited contracts were related, but not limited to, voting vaults, treasury, and storage. A comprehensive list of the audited core contracts can be found in the report, making solidity contracts the only audited part of the governance system. It is important to note that off-chain contracts, client-side portions of the codebase, deployment, and upgrade scripts were not in the scope of the audit.
Runtime Verification team leads Daejun Park and Raoul Schaffranek conducted Element Finance’s Governance smart contracts audit and published a detailed report on October 15th, 2021.
The team reviewed the governance code performing a manual audit and applied formal methods to identify possible vulnerabilities and disclose them to Element Finance’s team before opening up the new governance protocol to the public.
The first step consisted of reasoning about the core logic of the contracts to ensure the absence of logical loopholes and inconsistencies between the logic and the implementation. To carry it out, the team formalized the core governance logic, as well as the critical security properties, e.g., no loss or unintentional locking of funds, no unauthorized access to any features, no manipulating votes, etc., and rigorously verified the formal properties to ensure that the system is secure and works as expected in many different scenarios and edge cases. This formal-methods-based auditing technique helps to systematically examine the system’s behaviors in an infinitely large number of input combinations, and reveal novel unknown attack vectors, if any, that are specific to the governance system.
Next, the code was checked against well-known security issues and attack vectors that projects often fail to identify when developing their code. As simple as it may sound, an external person with knowledge about common vector attacks can help to identify possible vulnerabilities that the core developers may have missed, as they are already too familiar with their code and makes it more difficult to spot them.
Finally, we compiled the code and symbolically executed part of the bytecode. A lot of times, the compiler can introduce attack vectors that were not present in the high-level language, in this case, Solidity. This last step adds an extra layer of security to avoid possible attacks.
The audit identified and highlighted some critical issues along with a number of informative findings (see the report for details). Element Finance team properly addressed the issues and concerns raised during the audit and incorporated all the necessary changes in the smart contracts.
The governance contracts were well written and the Element Finance team followed best practices to ensure that the code behaves as expected and to minimize potential attack surfaces. We would also like to highlight RV Care, the security assurance agreement between the Element Finance team and Runtime Verification, which provides ongoing audit coverage to minimize any risks introduced by changes or updates to the already audited contracts.
Element Finance has built a new financial DeFi primitive that enables capital-efficient fixed and variable yield markets. Fixed rates are offered in a decentralized, open format with rates up to 15% on USD, Ethereum, or Bitcoin. Other projects can also develop new products or services by adopting its open-source infrastructure.
Runtime Verification is a technology startup based in Champaign-Urbana, Illinois. The company uses formal methods to perform security audits on virtual machines and smart contracts on public blockchains. It also provides software testing, verification services and products to improve the safety, reliability, and correctness of software systems in the blockchain field.