In preparation for the launch of the BTG Pactual ReitBZ token on Tezos, Least Authority reviewed the ReitBZ Security Token and Token Management Dashboard delivering a final report on March 13, 2020. The ReitBZ Security Token is a real estate backed token implemented with a smart contract using the FA1.2 standard interface, including additional functions for whitelisting token holders and distributing dividends to them. The Token Management Dashboard allows BTG administrators to interact with the token contract and its multisig admin through an interface. The dashboard collects signatures from Ledger hardware wallets through the browser, stores them until 3 are collected, and uses a “gas wallet” through Amazon Lambda / secrets manager to sign operations and send them to the chain. The dashboard shows all relevant token information, such as past operations, and manages user accounts / PKHs.
A unique challenge with auditing smart contracts in Michelson is the language is extremely idiosyncratic. The documentation provided by Tezos on the Michelson language, FA1.2 standard, the domain specific language Lorentz, and how these rest on the Tezos blockchain is crucial to understanding the distinctness of their approach. The Michelson language was created with simplicity and security in mind with a stack based approach that is less suitable for static analysis but is intentionally better suited for formal verification. Due to these and other differences in Tezos, we considered and adjusted our idea of known attack vectors given our previous experience with other smart contract systems.
The Tezos Michelson language has implemented tools in the Morely library, consisting of a type checker, and emacs editor mode options that we found useful. We hope to see more tooling specific to security or useful tools like common linters to help keep implementations consistent in the Tezos ecosystem of languages. For each language supported or compiled to Michelson, there is the opportunity for the development of tools such as static and dynamic analyzers, documentation on real world vulnerabilities, if any found, or attention paid to any issues that may arise from compiler errors that new languages may contribute to. Standardization around styles and lint guidelines and security best practices unique to Tezos contracts should begin to appear as the smart contract languages mature.
We found the ReitBZ Security Token code to be well written and good test coverage was present for both the contract and dashboard that we reviewed. The documentation for the contract contained a specification document, Haskell style reference, and contract API including a description of the dividends calculations and management that we found useful for quickly understanding the contracts at a high level, along with many code comments available to describe rationale for decisions and for understanding of the control flow better.
Our security audit was performed from November 25 to December 31, 2019, by Ramakrishnan Muthukrishnan, Sajith Sasidharan, Mirco Richter, Nathan Ginnever, Emery Rose Hall, and Alex Leitner. We identified six issues and four suggestions – all of which were resolved with the exception of one issue and one suggestion which were partially resolved. The issues and suggestions are all outlined in detail in the final audit report. An initial audit report was delivered on January 3, 2020 with a final audit report being delivered after two rounds of verification.