Expert Review

We are a team of distributed systems and protocol experts that is known for uncovering hard to find bugs and errors in code and protocol. We have profound expertise in protocol design, implementation, and analysis in the blockchain ecosystem, with origins in Tendermint and Cosmos as well as academic research on Byzantine fault-tolerant systems.

During code inspections, we manually analyze the source code for the purpose of reconstructing the underlying protocols. The code serves as the ultimate source of truth as we find it quite often diverges from specifications. Vulnerabilities are often found in codebases due to a number of reasons, including:

  • Incorrect engineering practices
  • Code evolution
  • Insufficient input validation
  • Overseen conditions

Protocol errors and bugs surface when protocol rules are violated when software runs in production. We perform audit activities to uncover these behaviours. These activities include:

  • Reverse protocol engineering
  • Mathematical protocol analysis
  • Protocol vulnerability analysis

Based on the results of the reverse protocol engineering practice, we try to answer two main questions:

  • Are there any flaws in the reconstructed protocols?
  • Are there discrepancies between the documentation/specification of the protocols and their implementation?

Automated Analysis

Our team has decades of collective experience in academia and in industry in model checking distributed protocols. We are the architects and maintainers of Apalache — a user-friendly automated formal verification tool we leverage in our security audits.

Model checking is known for unveiling unforseen edge-cases in protocols. In “adversarial testing” we turn these edge cases into tests. Without advanced and proper adversarial testing, blockchains can suffer a number of errors that pose a risk to user funds and instill distrust in the system. In these cases, blockchain consensus engines halt and protocol crashes occur.

We perform vulnerability searches by constructing TLA+ models which we leverage for code-specific test drivers. Through this process, we generate and execute massive adversarial test suites.

Protocols running in production often involve several distinct actors which can result in deep protocol errors. We construct abstract formal protocol descriptions in TLA+ in order to specify the system and its properties. We formalize desired protocol properties as safety invariants and liveness properties, and try to prove/disprove them using our in-house model checking techniques.

We generate test cases for the software that we audit directly from TLA+ specifications. This greatly augments manually created test cases with automatically generated ones derived from a formal model. These model-based testing activities include:

  • Construction of TLA+ models for deep testing of source code / APIs
  • Development of code-specific test drivers
  • Integration of model-based test suites into the customer CI

These techniques result in ​​a continuous and automatic monitoring process that searches for deviations between protocols and their implementation.

Logo for Apalache Apalache

Apalache is a symbolic model checker for TLA+ used to formally verifying distributed system protocols, which secure and transmit real-world value. Informal Systems has been actively developing Apalache with a focus on usability and integration with modern software development practices. Apalache is the brain-child of Igor Konnov and Josef Widder who leveraged years of academic research on formally verifying distributed systems to develop this powerful tool.

Learn More Github

Audit Inquiry
Audit Inquiry

Are you interested in our security audit services and what makes them unique from our competitors? Share with us information about your project and we’ll be in touch to explore how our audit services can make your system more secure.

Get in Touch