Is Cairo audited?

🙏 Help and Support
1

I am interested in learning how was Cairo audited, what vulnerabilities were surfaced and addressed, etc.

But having searched through multiple search engines and consulted multiple LLMs, I couldn’t find any public information / reports about Cairo’s audits still.

Is Cairo audited?

2

There are many ways to interpret this question as it’s quite broad, I’ll try to address a few

  1. Low level CASM constraints: do the constraints in the Cairo AIR when used in the STARK protocol actually reflect that semantics of the architecture. This was actually proven via lean, and is discussed in the following 2022 paper.
  2. Code correctness: several audit firms are offering Cairo audits. For example, you can find audits for the OpenZeppelin standards contracts Cairo-library by Zellic in their repo. Some of the lower level functionalities that are written in CairoZero had also undergone formal verification via lean, which you can read about in this recent paper.
  3. Compiler correctness: in fact we have two different compilers, Sierra –> CASM and Cairo–>Sierra. For the former, you can find related work in the paper from #2, as the CASM code for some libfuncs was shown to satisfy certain semantics. Given the pace of updates and complexity, the Cairo–>Sierra compiler has not been audited as of yet. Note that this is on par with other big projects such as solc, who hasn’t gone through (AFAICT) an end to end audit that generated code reflects the language semantics, but rather only ad-hoc audits of parts of the compilation flow.