开源静态分析工具Amarna：专为Cairo程序设计的漏洞检测利器

Cairo语言概述

为何需要Cairo？

Cairo与Noir、Leo等语言同属"可证明程序"语言体系，其核心价值在于：

计算外包场景中，工作者机器运行程序后生成有效性证明
验证者仅需验证证明而无需重新计算
典型工作流包含：函数编写→证明生成→证明验证三阶段

Cairo编程模型三大支柱

共享证明器(SHARP)：为用户提交的程序轨迹生成STARK证明
证明验证合约：验证程序执行证明的有效性
事实注册合约：存储程序事实（程序哈希与输出的绑定关系）

关键语言特性

一次性内存写入：内存单元一旦写入不可修改
assert双重语义：对未初始化变量执行赋值，对已初始化变量执行相等断言
非确定性跳转：结合提示(hint)实现控制流跳转

代码示例分析

Pedersen哈希验证

 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
12


# validate_hash.cairo
%builtins output pedersen

func main{output_ptr:felt*, pedersen_ptr : HashBuiltin*}():
    alloc_locals
    local input
    %{ ids.input = 4242 %}  # 通过Python提示赋值
    
    let (hash) = hash2{hash_ptr=pedersen_ptr}(input, 1)
    serialize_word(hash)  # 输出：152430969320712850019719...
    return ()
end

编译运行流程：

1
2


$ cairo-compile validate_hash.cairo --output compiled.json
$ cairo-run --program=compiled.json --print_output --layout small

事实注册机制

1
2
3
4


def compute_fact(program_hash, program_output):
    fact = Web3.solidityKeccak(['uint256', 'bytes32'],
                             [program_hash, Web3.solidityKeccak(['uint256[]'], [program_output])])
    return hex(int.from_bytes(fact, 'big'))

高危语言特性

1. 提示(Hints)风险

直接执行任意Python代码（包括系统命令）

1
2
3
4


%{
   import os
   os.system('whoami')  # 实际执行系统命令
%}

验证者无法感知提示存在（不影响程序哈希）

2. 递归与约束不足

当数组长度为0时，恶意证明者可操控输出：

 1
 2
 3
 4
 5
 6
 7
 8
 9
10


func sqr_array(array: felt*, length: felt) -> (new_array: felt*):
    alloc_locals
    let (local res_array) = alloc()
    %{  # 恶意提示可注入任意数据
        if ids.length == 0:
            memory[ids.res_array] = [1,3,3,7] 
    %}
    _inner_sqr_array(array, res_array, length)
    return (res_array)
end

3. 非确定性跳转漏洞

1
2
3
4


func are_equal(x, y) -> (eq):
    %{ memory[ap] = ids.x == ids.y %}  # 证明者可操控该条件
    jmp equal if [ap] != 0  # 危险跳转
    ...

Amarna静态分析工具

核心架构

基于Lark解析器构建AST分析器
三级规则体系：
1. 本地规则（单文件分析）
2. 采集规则（跨文件数据收集）
3. 后处理规则（全局模式检测）

10大检测规则

规则类型	检测目标	严重性
算术运算	有限域运算溢出风险	高危
未检查返回值	忽略关键函数返回值	高危
非常量断言	相同常量的不一致使用	中危
死存储	未使用的变量赋值	低危
调用者地址检查	get_caller_address返回值验证	中危

典型检测场景

1
2
3
4
5
6
7
8


# 算术溢出检测
let (res, overflow) = uint256_add(x, y)
# Amarna会标记未检查overflow的调用

# 未使用参数检测
func transfer(amount, unused_param):  # 标记unused_param
    assert amount > 0
    return ()

未来规划

增加数据流分析能力
集成更多Cairo特定模式检测
社区贡献机制完善

特别警示：Cairo提示系统允许执行任意Python代码，严禁运行不可信Cairo程序！