Skip to main content

Azimuth

In physics and navigation, the angular distance between a reference point and a chosen point is called the azimuth.

Azimuth is a system that leverages LLMs and reinforcement learning to analyze smart contracts. Azimuth is designed to augment and accelerate the conventional smart contract audit. It describes the structure and intent of the target system, uncovers operational vulnerabilities, and gives auditors deeper coverage in less time.

Azimuth's broad goal is to calculate and interpret the distance between the developer's intent and the execution of the target. Neither "intent" nor "execution" are trivial to measure or communicate. This is the challenge but also the opportunity of developing Azimuth.

caution

Azimuth's implementation is under active development. This documentation is a snapshot of its structure. Please consider that the implementation may have changed since last update.

In this document, we use the term target to mean the smart contract(s) that Azimuth is analyzing.

How it works​

Azimuth operates in three distinct stages with one preparatory stage.

0. Preparation​

In Preparation, Azimuth compiles the target and collects any other information it can find such as documentation. This could also include data like events or transactions for deployed targets.

1. Exploration​

In Exploration, Azimuth seeks to learn as much as possible about the target. This is accomplished through many different means and resources. There are two reasons we execute this stage:

  1. To be able to describe the target adequately to the user. This is a fundamental output for an audit.
  2. To provide structured and usable information for downstream processes. Typically the input to the system is a git repo which contains source code and some documentation. We process that information and create derivatives which are useful for the system. In the case of a deployed contract, onchain data such as events and historical transactions can be processed. All of this information is distilled and indexed into a form that can be efficiently ingested and used by future stages.

Outputs:

  • Intent — A description of what the developers of the target intend the target to accomplish, independent of the execution of the target. This is typically derived from comments in the source code, variable names, and documentation. It is independent from execution because any difference between intent and execution would be an output of its own.
  • Invariants — Statements which should not vary in the case of the target. "Invariant" means the developers intend for the statement to not vary, not that it does not vary in execution—that's what Azimuth tests. Invariants are typically a low-level representation of intent. For example, the intent of a developer may be that their token legitimately accounts for user holdings. This can be partially represented by the invariant that "the sum of token holdings must be less than or equal to the total supply of the token."
  • Scope — A subset of the files submitted for analysis. Test files, documentation, and other files that do not contribute to the execution of the target are filtered out from consideration.

2. Proposal​

Given the intent and invariants of the target, Proposal seeks to identify locations in the source code where execution might conflict with the intent. This is fairly cheap as LLMs have a tendency to begin validating proposals quickly once they have been found, and we want to scope this stage to purely identifying possible issues.

There are three general types of proposals:

  1. Economic — Issues related to token economics, value flows, and incentive structures
  2. Structural — Issues in code architecture, access control, and state management
  3. Invariant — Violations of identified invariants

Each of these corresponds to a different prompt for an LLM agent that encourages exploration in the specific domain.

Outputs:

  • Each agent produces a list of proposals for further investigation.

2.5 Consolidation​

This short stage de-duplicates the proposals and filters out low severity proposals from the investigation stage. Since investigation is relatively expensive in terms of tokens and time, we limit investigation to the critical and high impact proposals. If there are no critical or high proposals, we move on to investigating medium impact proposals, but we still limit the total number of investigations that occur.

3. Investigation​

Investigation starts four investigation agents in parallel. Each agent is responsible for using 15 tools to validate or disprove the proposals from the previous stage.

Findings include likelihood, severity, and impact classification (critical, high, medium, low).

Integration​

We support Foundry and Hardhat repos which can connect through our GitHub integration. After connecting, scans can be triggered which yield results created by the workers described above.

Get started​

Contact TestMachine to discuss your use case and early access.