Introduction

In the second community call and AMA session, the Atlendis Labs team was pleased to welcome special guests Raoul Schaffranek, Formal Verification Engineer at Runtime Verification and Stephane Coquet, Co-Founder and Chief Technology Officer at Atlendis Labs. This was an opportunity to discuss the Atlendis’ smart contract audit and security, to enable the Atlendis community to learn more about the recent audit of the Atlendis protocol that was conducted by Runtime Verification, Web3 protocol auditing, and security best practices in general.

This article is the written transcript of the following audio, available on Atlendis' YouTube channel:

https://www.youtube.com/watch?v=BzBFwJyFt6I

Hello Stephane! Can you please introduce yourself, tell us about your background and what you are working on at Atlendis Labs?

Stephane: Thanks and hello to the Atlendis community! I’m very happy to be here today. I am Stéphane, Co-Founder and CTO of Atlendis Labs. I have been in the Ethereum ecosystem since 2017, particularly on the technical side of the blockchain. These last few months I have been building the Atlendis protocol smart contracts and other components of the protocol along with our engineering team. As such, I have been working closely with the Runtime Verification team to make sure that the audit went as smoothly as possible.

Thank you Stephane. Hello Raoul! Could you tell us a little bit about your background and your role at Runtime Verification?

Raoul: Thank you, hi everyone! Hi to the Altendis community and thank you for the invitation and the opportunity to have this discussion with you today. I’m Raoul Schaffranek and I work at Runtime Verification as a Formal Verification Engineer and my focus is on Ethereum or EVM based projects. In this engagement I was the lead auditor.

Thank you Raoul and welcome! Let’s start with a high level question. Could you briefly introduce the auditing activity to the audience?

Raoul: Yes, sure. This kind of engagement was a manual review audit and the easiest description of what we do is we try to find as many bugs as possible before an attacker could find and execute them. There is one thing that can often confuse people, many people think of audits and then think OK, this contract has been audited so it must be 100% secure and safe, but this is not a real expectation to have. What we try to do is to discover as many bugs as possible, but we think that auditing should be only one activity in a complete suite of your security strategy, along with testing, static analysis, and bug bounty programs. We think auditing is valuable, especially having an independent company doing an audit, because it requires a completely different mindset to develop code and to do a security analysis of the code. In our team, we are all developers to some extent and we know we have a completely different mindset when developing and auditing, and that’s one of the benefits of having an independent company doing the audit for you.   

Could you describe Runtime Verification’s mission as an auditor, specifically in Web3?

Raoul: We observe that Web3 is growing very fast. With fast growth comes a lot of security challenges. Exploits generally generate a lot of media attention and contribute to the volatility of the ecosystem and lead to slow adoption and we want to avoid this. We think that security is mandatory in both the short and long-term for the ecosystem to grow. 

Thank you! Now Stephane, two questions for you: first, why did Atlendis Labs proceed with an audit of the Atlendis Protocol, and second, why did you specifically decide to work with Runtime Verification for the audit?

Stephane: The Atlendis Labs team decided to audit the smart contracts because the Atlendis protocol is a complex and innovative piece of code, at the forefront of what is being done in DeFi today.

We could not imagine going to production without making sure that our code is as safe as possible to use and follows all the best practices. One of the core values of the Atlendis Labs team, not only the technical team, is to do things the right way and to not take shortcuts. As skilled as our team of engineers might be, we are pragmatic and we did not want to miss even the slightest thing in our code. An audit is also a way for us to show how serious and committed we are to making the Atlendis protocol a success, and unlock new opportunities for both our lenders and borrowers.

We decided to work with Runtime Verification for their reputation, their past work, and their diverse set of skills. In addition to their expertise in smart contracts and DeFi, they also specialize in formal verification. This was a great match with the Atlendis Protocol, since apart from looking for bugs in our smart contracts, they also analyzed the soundness of the protocol.

How long did the audit last, and how did the two teams work together throughout the audit?

Stephane: The audit was initially planned to last 4 weeks, starting on January 10th, but in the end it concluded on February 18th, after 6 weeks, because the code base was denser than expected.

Over these 6 weeks, the teams regularly communicated on both the protocol specification and the smart contract implementation.

The findings of the Runtime Verification team were discussed as they were discovered. Communication was really fluid between the teams, and regular exchanges went back and forth: the Atlendis Labs team managed to support the Runtime Verification team as they were ramping up on the protocol, while the Runtime Verification team gave additional advice to the Atlendis Labs team as development went forward. In particular, the Runtime Verification team helped us weigh the pros and cons of certain implementation decisions that we wanted to make on the contracts.

Thanks Stephane. Raoul, could you tell us more about Runtime Verification’s approach and differentiators? Also, could you tell us about your team?

Raoul: Sure. As Stephane mentioned, auditing is a collaborative activity. Because we don’t own the code base, we need the input from your developers during the engagement. So we don’t lock ourselves in for six weeks and then come up with a report, but it’s an ongoing collaborative effort where we have many technical discussions with the different dev teams. We wanted to be as collaborative as possible. One thing that sets us apart from other auditing companies is that we do formal verification based audits, that means we apply formal verification methods where it is practical. Sometimes in the early phases of an audit there are other activities that might be more effective, but once we get to the later stages of the audit, there are some possibilities to apply formal methods and get a huge benefit out of it and this was also the case in this engagement. 

About our team, we are a diverse, globally operating company, we have our own infrastructure teams working on in-house software and we have different teams working on specific ecosystems. As I said earlier, I’m working on Ethereum based and Solidity based projects.

Thank you for that overview! Now that we have a few elements of context, let’s get into the details of the audit. Raoul what was the scope of the audit of the Atlendis protocol?

Raoul: The scope was the totality of all the Solidity smart contracts and especially the Pools and the NFT position contracts, but all the other contracts were audited as well. What was not in the scope was off-chain activities. We only looked at the on-chain code of the protocol. 

Thank you. For those who may not know what’s under the hood of the Atlendis protocol or who have not yet read the whitepaper, could you describe the two smart contracts of the protocol, Stephane?

Stephane: The Atlendis protocol has two main parts: the Borrower Pools contract and the Position Manager contract.

The first one contains all the data relative to pool functionalities, including but not limited to the pool’s asset type, pool maturity, maximum borrowable amount, or the liquidity reward rate that will be paid out to liquidity providers by the borrower. This contract will actually pool all the funds from the lenders, that will be deposited on a third-party yield provider like Aave. 

The second smart contract will manage the individual positions of lenders as they deposit into the pool of their choice. Lenders will choose an asset, a pool and the rate at which they are willing to lend to the borrower. In return, they will receive an NFT that represents their detailed position in the pool. The position, and therefore the NFT representing it, will be able to change status during the lifecycle of the loan, since funds will be either lent out to the borrower, or deposited on a third-party yield provider as mentioned before. All of this will be automatically managed by the position manager smart contracts.

Now Raoul, could you please describe the various steps of the smart contract audit conducted by your team?

Raoul: Sure. I wish there was a general approach to auditing, but there isn’t. We always use a holistic approach and I think I can break it down into a couple of steps.

First, we need to get an understanding of your product. We review all the documentation, the whitepaper, and any literature that you have, and then we try to get an understanding of your business model. When we obtain this mental model, we try to map it to the actual implementation and we actually try to draw arrows and we can say for example, this particular feature in the whitepaper is linked to this piece of code, and also the other way around, we try to see if something is missing. If there’s a missing arrow, it’s not necessarily a bug, but it’s often a good indicator of a bug. 

Once we have mapped the implementation to the business model, we then develop an abstracted high level mathematical model that serves two purposes: it eases the communication between the development teams and makes it easier to identify invariants that we later try to prove in the implementation.

In the next step we check the code base against known security vulnerabilities. Of course, every security vulnerability is particular to one specific contract, but we notice that security issues often follow patterns and we look out for and try to identify these patterns. 

Last but not least, we try low level reasoning about arithmetic, precision errors and in particular rounding errors that can occur. One last thing to mention is that these are conceptual phases that overlap and finding an issue requires you to go back to the documentation. That summarizes the steps we took in this audit. 

Were there other topics covered in the audit, Stephane?

Stephane: We tackled the question of gas consumption and best practices in security, but also usability.

The Atlendis protocol consists of an order book of interest rates. This means that when lenders assess the borrowers, they will choose the rate they agree to lend their funds at, within a preset range. Not everyone will have the same opinion of the borrower, and in the end a fair rate will be discovered. For that reason, the protocol allows lenders to deposit at a variety of rates, which we call ticks. Each tick is in itself a small pool of liquidity. The Atlendis protocol shares some similarities with other Web3 players like DeFi 2.0 protocols, in the sense that it allows for a refined management of liquidity.

When a loan is taken towards the pool, the smart contracts iterate on all the ticks to get the funds at the best possible rate for the borrower. Iterating in smart contracts can induce high gas costs, and we had to find a good balance between the funds management precision - having a lot of ticks - and usability - making our protocol usable by most lenders thanks to reasonable gas usage.

Gas fees can be a barrier for DeFi adoption. Raoul, did your team comment on gas consumption and optimization during the audit?

Raoul: To be clear, our top priority is security and not gas efficiency. Of course we know there are trade-offs sometimes involved. However, users care a lot about gas efficiency. We report gas optimization potential along the way if we see an opportunity for improvement. Two potential gas savings were discovered in the report, but we focus on security.

Stephane, could you tell us more about how the Atlendis Labs team tackled gas optimization?

Stephane: During the first protocol iteration, development was focused solely on the soundness of the Atlendis protocol. We wanted to verify our hypotheses, and prove that our model was working. We also focused on correctness of our calculations and security. Gas optimization was very early on in our minds, but we did not want to focus too much on it at the beginning to not set limits to what we could do or not.

Throughout the second development phase, during which the audit was conducted, we came back over and over on the logic, always improving our code logic on the way, removing security flaws if there were any. At this point, we started looking into more details about gas optimizations. For that reason, we reassessed all of our base imports - we changed our ERC-721 implementation because it contained features we did not need like enumeration - and we rethought our data structures to make them as efficient as possible. In smart contracts, less storage means less gas usage, which led to code refactorings. We were also continuously measuring the gas usage of our contracts with a dedicated set of test scenarios, which led to optimizing the logic to reduce the number of operations.

How did the Atlendis Labs team address gas consumption by dropping ERC-721 Enumeration for instance? What is the position NFT ERC standard, and how will it reduce gas usage?

Stephane: To ease development and rely on strong and proven standards, the Atlendis Protocol relies on the OpenZeppelin smart contract suite. These contracts are widely used within the Defi ecosystem, and have been audited and battle tested countless times. We rely on them for the upgradeability of our contracts, ERC20 tokens interactions and ERC721 implementation. The OpenZeppelin ERC721 implementation consists in a base contract, that implements all the base methods of the standard, and a choice of extensions that allow the addition of features on top of the base layer. At the beginning of the protocol development, we chose a feature rich implementation, including token enumeration. Token enumeration allows token ownership discovery to be done directly on chain, you can for example choose an owner address and find out all the NFTs this address has. In practice, this is a nice feature. However, it uses a lot of additional storage variables in its implementation, which drastically increases the gas consumption of our contracts. During the second development phase of the contracts, we reviewed our dependencies, decided that the enumeration feature was not critical for us and chose to stick with the base implementation of the ERC721, which cut our gas consumption by more than 10%!

Thank you Stephane! On another topic Raoul: when auditing a DeFi protocol, what are the best practices in terms of solving found vulnerabilities, even minor ones, and how was this reflected with the Atlendis team?

Raoul: For the first part, we generally classify our findings on two axes, the first being severity and we try to answer the question: how much damage can be done if this issue is ever exploited? The second axis is difficulty and that’s a completely independent measure that answers the question how difficult is it for an attacker to execute this vulnerability. Obviously you try to avoid the sweet spot of high vulnerability and low difficulty, as these can be attacked with low effort. 

Like I said earlier, many security vulnerabilities follow certain patterns, and what’s good about this is that there are known mitigation techniques. Often solving a security vulnerability comes down to applying known security mitigation.  

Stephane, was this your first audit?

Stephane: Yes, it was the first audit I was involved in. Security is really a key subject when it comes to the development of smart contracts, and as such I have been educating myself on it, as well as reading other protocol codebases and audit reports. It was an interesting experience, as it was extremely collaborative and the Runtime Verification team was very helpful during the entire process. Prior to the audit, the Atlendis protocol was developed only within our team and advisors, and tested with a few selected users - but this was the first time our code was going to be reviewed by external auditors.

Can you share any significant discoveries or learnings from your first audit with the Runtime Verification team?

Stephane: Sure! The Atlendis protocol is basically built as a layer above a third-party yield provider protocol such as Aave. As such, we hold our own internal accounting, while the funds are deposited on Aave. During the development process, we focused a lot on the internal accounting part of the protocol, and less on the integration of external components, such as the Aave V2 protocol and the pools underlying ERC-20 tokens. As it happens, even though the ERC-20 is a specification that most of the tokens we will be using support, some of them have less functionalities, and some of them have more. For example, some take fees on the transfers, do not return a boolean parameter where they should, can allow for external hooks to be called before and/or after a transfer etc. There is a wide array of possibilities that we had to support, in order to make sure we did not leave any open doors for toxic tokens to harm the protocol.

What is an external vulnerability? Could one of you explain the importance of assessing and mitigating external vulnerabilities in the specific case of the Atlendis Protocol audit? 

Raoul: If you look at a smart contract in isolation, you can reason about the business logic and see if it adheres to the specifications, and that’s all good. What we observed in the recent past, is that some exploits are not targeting internal business logic of a contract, but instead targeting the boundaries. And ultimately any useful smart contracts will have to interact with foreign or different smart contracts. For simplicity, assume we have two smart contracts and their internal logic is valid and they have no security issues and that's an idealistic case. Yet, there are still security issues that could come from these two contracts interacting with each other. 

External vulnerabilities are vulnerabilities that happen at the boundaries when one smart contract wants to talk to another smart contract. We have observed an ongoing trend and attackers are specifically looking out for sec issues at the boundaries of protocols. In the case of the Atlendis protocol – and this is true for many others – using ERC-20 tokens is already one significant integration that comes with pitfalls and opens the gates for bugs and potential abuse or hacks. Another integration comes from the protocol’s feature to deposit non-borrowed funds into an external third-party yield providing protocol.

Can you share an experience or well known case in mind that epitomizes external vulnerabilities?

Raoul: The most infamous example is the DAO Hack of 2016, which was one of the first major hacks in the crypto ecosystem. If I remember correctly, assets worth around $70M were stolen. It was an interesting attack from a security perspective, the first of its kind, introducing a new attack surface and it was the first in a series of hacks. 

Could you both share some security “best practices” as the team continues developing and expanding the Atlendis protocol’s smart contracts?

Raoul: There are three major points I want to point out. First, always be transparent about security and security issues. This community call is a good sign of your willingness to be transparent. 

Second, don’t rely on a single security technique like audits, but always have a comprehensive security strategy, use testing, static analysis, independent auditors and bug bounty programs, and all these security techniques together are worth more than their sum.

Third and finally, security is nothing that can be added on top of a protocol after its development. It's a continual effort from the initial design and throughout the complete lifetime of the product, security should be a top priority. 

Stephane: Always come back to your code with different points of view, do thematic reviews. When writing contracts, it’s easy to tunnel into your vision and not be aware of interactions that you did not predict. Also, security should be everyone’s concern, there’s a lot of material online on known security pitfalls that everyone can read. 

Finally, I agree with Raoul: testing, audits and bug bounties are extremely valuable and are key parts of a security strategy.

Conclusion

Special thanks to Raoul from Runtime Verification and Stéphane from Atlendis Labs for taking the time to join us. Don’t miss the next Atlendis Labs community call and AMA session! 

Read the Atlendis protocol V1 whitepaper here. The audit report of the Atlendis protocol by Runtime Verification can be found here.

Join the Atlendis Labs Discord to be a part of the community and participate in the evolution of the Atlendis protocol!

Have a wonderful day and see you soon in the Atlendis World!

Links

Atlendis.io | Audit Report | Whitepaper | LinkedIn | Twitter | Discord | Newsletter | YouTube