Radiant：Solana程序的混合执行 - Inversive Labs
- inversive
- 发布于 2025-12-23 14:36
- 阅读 22
Radiant 是一个用于 Solana 程序的二进制级符号执行框架，它结合了具体执行和符号执行，通过双引擎架构实现。Radiant 能够进行有针对性的基本块探索和跨 CPI 符号执行等操作，可以用于分析 Solana 程序的安全性，尤其是在多程序交互和复杂状态机的情况下。
Radiant: 用于 Solana 程序的 Concolic Execution
本文介绍了 Radiant，一个用于 Solana 程序的二进制级别的 concolic execution 框架。
目录
简介
Radiant 是一个用于 Solana 程序的高级测试框架，它利用 concolic execution，这是一种结合了具体执行和符号执行的混合方法。
Radiant 将程序输入字段和账户状态建模为具体值或符号变量。给定一个目标代码位置，它使用符号执行来确定哪些输入值能够执行到达该位置的执行路径。
动机
安全审计员在分析智能合约时，会将多种技术结合起来，包括人工代码审查以理解程序逻辑、模糊测试以系统地测试代码库以及对关键属性进行形式化验证。每种技术都有其独特的优势。人工审查利用了人类的洞察力和推理能力，模糊测试则通过实验来探索行为，而形式化方法则提供了数学上的严谨性。
Radiant 使用 concolic execution 增强了这个工具包，concolic execution 是一种将具体执行与符号执行相结合的技术。但为什么要使用 concolic execution 而不是纯粹的符号执行呢？
Solana 的架构提出了一个独特的挑战，程序是无状态的，并且对作为输入传递的帐户进行操作。一个交易可以包括几十个账户，每个账户都有任意的数据和状态。将所有内容都符号化，很快就会变得不切实际。大量的符号变量可能会使约束求解器不堪重负，并使分析变得难以处理。
Radiant 的 concolic 方法通过从表示具有实际账户数据、余额和程序状态的部署的具体执行上下文开始来解决这个问题。从这个具体的基线开始，可以选择性地将特定值标记为符号。可能只是指令参数，或者帐户数据中的特定字段。这种选择性的符号化使分析保持专注和易于处理，同时仍然能够进行有针对性的路径探索。
当与模糊测试结合使用时，这种方法尤其强大。模糊测试在探索大规模的程序状态空间方面表现出色，但很难到达被条件语句隔离的深度嵌套代码路径。Radiant 通过解决符号化值的约束来生成到达特定代码位置的精确输入来解决这个问题。
工作原理
要理解 Radiant 的方法，首先需要认识到传统测试方法的局限性。考虑一下应用于给定 Solana 程序的典型测试场景：
上面的控制流图 (CFG) 显示了运行不同测试时采用的执行路径。每个测试都会探索给定程序逻辑中的某些分支和基本块。
虽然多个测试增加了代码覆盖率，但它们仍然遵循由特定测试输入决定的可预测路径。这种方法通常会错过潜伏在未探索的执行路径中的边缘情况。
考虑这样一种情况：由于先前块由于意外状态变化导致的错误计算，某个错误在特定的基本块中表现出来。
有目标的符号执行
Radiant 通过启用有目标的基本块探索来解决这个问题。 遵循自下而上的方法，Radiant 可以显式地定位要到达的特定基本块，而不是希望随机输入会偶然发现有问题的代码路径。
可以通过多种方法选择目标基本块：
- 人工分析：安全审计员识别可疑的代码模式并直接定位这些块
- 自动方法：启发式或静态分析工具识别潜在的易受攻击的块
- 混合策略：自动探索多个目标，同时排除已知安全或不相关的代码区域
选择目标基本块后，Radiant 会执行符号执行以发现到达该基本块所需的条件：
-
符号变量引入：Radiant 将选定的输入字段和帐户状态视为符号变量而不是具体值
-
路径探索：随着执行的进行，每当遇到符号程序计数器 (PC) 时（通常是表示取决于符号变量的条件语句的分支指令），控制流就会发散
-
并行路径分析：每个发散的路径都以符号方式并行探索，构建路径约束以捕获到达每个分支所需的条件
-
目标达成：当符号执行到达目标基本块时，Radiant 已经积累了到达该代码所需的所有路径约束
-
具体化：最后，Radiant 求解这些约束并具体化符号值，从而生成确定性地触发目标基本块的具体输入值
这从根本上讲就是像 angr 和 Manticore 这样的二进制级别符号执行框架在传统二进制文件上的操作方式。
这些工具使安全研究人员和开发人员能够分析复杂的执行路径，并生成触发特定代码路径的具体输入。
架构
Radiant 的架构由通过调试器桥协调的两个并行执行引擎组成：
Solana 运行时模拟器
架构的左侧通过 Solana 运行时模拟器 提供具体执行。 Radiant 利用 LiteSVM，这是一个轻量级的 Solana 虚拟机，以其原生 sBPF（Solana Berkeley Packet Filter）字节码格式执行程序。 该组件使用具体值运行实际的程序指令，同时保持准确的运行时状态，包括帐户数据、指令上下文和程序执行流程。
符号执行引擎
右侧包含符号执行引擎，该引擎围绕污点跟踪引擎构建。 该引擎包括 IL 解释器（中间语言解释器），该解释器对程序的提升表示进行操作。
Radiant 建立在 radius2 的修改版本之上，这是一个强大的符号执行框架，它利用 radare2 的 ESIL（可评估字符串中间语言）作为其中间语言。
这项工作直接建立在我们对 radare2 的 sBPF 架构贡献之上，我们专门开发这些贡献是为了实现对 Solana 程序的高级二进制分析。 我们在 r2con 2025 上介绍了这项工作，展示了在 radare2 中实现 sBPF 支持的过程。
调试器桥
调试器桥 用作两个引擎之间的协调层，通过集成到修改后的 solana-sbpf 版本中的 GDB stub 服务器 实现。 此实现支持 Solana VM 和符号执行引擎之间的标准 GDB 远程串行协议通信。
该桥使用两阶段架构运行：
- 部署：运行一个具有嵌入式 GDB 服务器的
LiteSVM实例，该服务器侦听连接。 - 符号执行：使用
radare2连接到 GDB 服务器，从内存中读取具体上下文，并将其传递给radius2以进行符号执行。 只要radius2需要额外的具体上下文，此过程就会间歇性地重复。
通过 GDB 协议，Radiant 可以：
- 在特定程序计数器位置设置断点
- 控制执行流程
- 按需读取内存和寄存器状态
- 将具体执行与符号执行上下文同步
这种双引擎架构支持 concolic execution。 修改后的 solana-sbpf 运行时通过其 GDB 接口提供程序和事务的具体上下文，而 radare2 提取此上下文，并且 radius2 利用它来构建路径探索所需的符号约束。
理想情况下，符号执行会利用基于编译器的中间表示形式（例如 LLVM IR），这些表示形式提供明确定义的语义和强大的工具支持。 但是，现有的基于 LLVM 的符号执行框架缺乏对 sBPF 的 ISA 和 SIMD 扩展的成熟支持。 我们没有在基于 LLVM 的框架中从头开始构建 sBPF 支持，而是选择使用 radare2 的 ESIL（可评估字符串中间语言），该语言已经通过我们先前的贡献为 sBPF 分析奠定了基础。
此选择需要验证。 我们需要确保我们的 ESIL 指令模型准确地表示 sBPF 语义。 为了实现这一点，我们利用调试器桥来实现差异模糊器，该模糊器比较 ESIL 解释器和实时调试器会话之间的执行跟踪。
通过模糊指令并比较它们在两个环境中对寄存器和内存的影响，我们能够以合理的置信度验证我们的 ESIL 模型正确捕获 sBPF 语义，从而提高了对符号执行结果的信心，即使未使用编译器 IR。
示例演练
让我们用一个实际的例子来演示 Radiant：发现触发 Solana 程序中的 panic condition 的确切输入值。
注意：此示例使用简化的程序来清楚地说明 Radiant 的符号执行功能。 实际的 Solana 程序涉及明显更复杂的逻辑，但适用相同的方法。
目标程序
考虑以下 Solana 程序：
##[program]
pub mod hello_world {
use super::*;
pub fn initialize_fn(ctx: Context<InitializeContext>, input: u8) -> Result<()> {
msg!(
"Hello World address: {}",
ctx.accounts.hello_world_account.key()
);
let hello_world_store = &mut ctx.accounts.hello_world_account;
hello_world_store.input = input;
if input > 200 && input < 210 {
panic!("This number is magic")
}
Ok(())
}
}该程序接受一个 u8 输入参数，并且仅当该值落在 201-209 的狭窄范围内时才会发生 panic。 传统的模糊测试最终会发现这一点，但是符号执行可以系统地找到所有有效输入。
理解 snapshot_pc 和 target_pc
在运行 Radiant 之前，我们需要识别两个关键的程序计数器位置：
-
snapshot_pc：Radiant 在此处获取程序状态的快照并开始符号执行的程序计数器。
-
target_pc：我们要到达的特定基本块，在本例中为 panic 语句。 Radiant 探索的所有执行路径旨在满足到达此目标所需的约束。
注意：如果
snapshot_pc设置为 0，则 Radiant 会自动将其填充到指令函数入口点或程序入口点，使其完全确定，无需手动二进制分析。
该图说明了符号执行如何从快照点开始，并在符号上下文中探索多个路径，直到到达目标基本块。
Radiant 测试配置
测试设置涉及两个主要组成部分：
1. Radiant 测试配置 (tests/test.rs):
use radiant_test::*;
use std::collections::HashSet;
use crate::setup::*;
##[test]
fn test_example() -> Result<()> {
let snapshot_pc = 0x100007018;
let target_pc = 0x1000078d8;
let (config, deployment_thread) = setup::config(
snapshot_pc,
target_pc,
20,
true,
false
);
let mut test = RadiantTest::new(config)?;
let result = test.run(SymbolizeSpec::InstructionData {
length: 1
})?;
let solutions = result.into_bytes();
println!("\n[+] Found {} solutions", solutions.len());
for (i, sol) in solutions.iter().enumerate() {
let value = sol[0];
println!(" Solution #{}: {} (0x{:02x})", i + 1, value, value);
assert!(value > 200 && value < 210,
"Solution {} is outside valid range (201-209)", value);
}
Ok(())
}该测试指定快照和目标程序计数器，然后对指令数据的最后一个字节（u8 输入参数）进行符号化，同时考虑到考虑到指令鉴别符的位移。
2. 程序部署 (src/deployment.rs):
pub fn call_initialize_fn(&mut self, input: u8) -> Result<()> {
println!("\n[*] Calling initialize_fn...");
let (hello_world_account_pda, _bump) = self.deployed.find_pda(&[b"hello_world_seed"]);
let mut data = vec![0x12, 0xbb, 0xa9, 0xd5, 0x5e, 0xb4, 0x56, 0x98];
data.push(0u8);
let instruction = Instruction {
program_id: self.deployed.program_id,
accounts: vec![\
AccountMeta::new(self.deployed.payer_pubkey(), true),\
AccountMeta::new(hello_world_account_pda, false),\
AccountMeta::new_readonly(system_program::ID, false),\
],
data,
};
let recent_blockhash = self.deployed.svm.inner.latest_blockhash();
let message = Message::new(&[instruction], Some(&self.deployed.payer_pubkey()));
let tx = Transaction::new(&[&self.deployed.payer], message, recent_blockhash);
self.deployed.enable_debug();
match self.deployed.svm.inner.send_transaction(tx) {
Ok(result) => {
println!("[+] initialize_fn successful!");
for log in &result.logs {
println!(" {}", log);
}
Ok(())
}
Err(e) => Err(anyhow::anyhow!("initialize_fn failed: {:?}", e)),
}
}部署代码构造交易，启用调试器接口，并执行程序到传递给 Radiant 进行符号执行的点。
使用 radare2 进行二进制分析
目前，查找正确的 snapshot_pc 和 target_pc 值需要二进制级别的分析。 我们扩展了流行的逆向工程框架 radare2，以支持具有增强反汇编功能的 sBPF 体系结构：
该屏幕截图演示了我们在 radare2 中实现的一些增强功能：
- 左侧面板：sBPF 反汇编显示字节码指令及其在二进制文件中的对应地址
- 右侧面板：中间语言 (IL) 表示，其中聚合的 Rust 源字符串直接嵌入在反汇编中
请注意 IL 输出如何包含 Rust 字符串和指针引用，在其中我们可以发现 panic 消息字符串（"This number is magic"），从而可以轻松地在二进制文件中找到目标基本块。 IL 还显示了从 sBPF 转换而来的条件逻辑，揭示了对应于源级别范围检查的比较 if (r6 <= 0x8)。
尽管仍有很多需要改进的地方，但这些增强功能弥合了高级 Rust 源代码和低级 sBPF 字节码之间的差距，从而可以识别程序计数器位置。
如前所述，我们在 r2con 2025 上介绍了这项工作，展示了在 radare2 中实现这些功能以进行 Solana 程序分析的过程。
演示
上面的演示显示 Radiant 发现触发 panic condition 的 201-209 范围内的所有输入值。 Radiant 的约束求解器并没有依靠随机模糊测试来最终达到这个狭窄的窗口，而是确定性地生成所有有效的解决方案。
结果
执行后，Radiant 输出：
[+] Found 9 solutions
Solution #1: 201 (0xc9)
Solution #2: 202 (0xca)
Solution #3: 203 (0xcb)
Solution #4: 204 (0xcc)
Solution #5: 205 (0xcd)
Solution #6: 206 (0xce)
Solution #7: 207 (0xcf)
Solution #8: 208 (0xd0)
Solution #9: 209 (0xd1)Radiant 系统地识别了满足约束 input > 200 && input < 210 的所有九个值，从而在没有手动猜测或详尽的模糊测试的情况下，完全覆盖了这个特定的执行路径。
跨 CPI 的 Concolic Execution
Radiant 的高级功能之一是跨程序调用 (CPI) concolic execution。 在 Solana 的可组合架构中，程序经常通过 CPI 调用其他程序，从而创建复杂的执行流程。
注意：以下示例使用简化的双程序交互来演示跨 CPI 技术。 实际的协议通常涉及更复杂的交互。
以仅可通过 CPI 访问的代码为目标
考虑这样一种情况：你的目标基本块存在于被调用程序中，但只能通过调用程序的 CPI 调用来访问：
该图说明了这个问题。 在左侧，我们有调用程序的控制流图，在右侧，我们有被调用程序的 CFG。 目标基本块（标有星号）位于被调用程序的执行路径中，只有在从调用程序进行 sol_invoke_signed_* CPI 调用后才能访问。
传统的符号执行框架会在这里遇到困难，它们通常会孤立地分析单个程序。 要到达被调用程序中的目标，你需要了解值如何通过 CPI 边界进行转换，并将约束向后传播到两个程序中。
示例
让我们检查一个包含两个程序的具体示例。 调用者在调用被调用者之前转换输入。
Callee 程序 (cpi_callee):
##[program]
pub mod cpi_callee {
use super::*;
pub fn increment(ctx: Context<Modify>, amount: u64) -> Result<()> {
let counter = &mut ctx.accounts.counter;
require!(
counter.authority == ctx.accounts.authority.key(),
ErrorCode::Unauthorized
);
if amount >= 660 && amount < 666 {
panic!("TARGET REACHED: amount falls in bounds");
}
if amount >= 666 && amount < 700 {
panic!("TARGET REACHED: amount falls in bounds 2");
}
counter.count = counter.count.checked_add(amount)
.ok_or(ErrorCode::Overflow)?;
counter.operation_count += 1;
msg!("Counter incremented by {}. New value: {}", amount, counter.count);
Ok(())
}
}被调用者有两个 panic condition：当 amount 在 [660, 666) 或 [666, 700) 中时。 对于此示例，我们的目标是第二个 panic condition，即在检查 if amount >= 666 && amount < 700 的行。
Caller 程序(cpi_caller):
##[program]
pub mod cpi_caller {
use super::*;
pub fn cpi_increment_counter(
ctx: Context<CpiModifyCounter>,
amount: u64,
) -> Result<()> {
let transformed_amount = amount.checked_add(123).unwrap();
let cpi_program = ctx.accounts.callee_program.to_account_info();
let cpi_accounts = cpi_callee::cpi::accounts::Modify {
authority: ctx.accounts.authority.to_account_info(),
counter: ctx.accounts.counter.to_account_info(),
};
let cpi_ctx = CpiContext::new(cpi_program, cpi_accounts);
cpi_callee::cpi::increment(cpi_ctx, transformed_amount)?;
Ok(())
}
}在通过 CPI 将输入传递给被调用者之前，调用者通过添加值 123 来转换输入。
Radiant 的跨 CPI 解决方案
Radiant 的跨 CPI concolic execution 通过跨程序边界跟踪符号值来工作：
-
符号值传播：当符号执行到达调用程序中的 CPI 调用点时，Radiant 会识别作为参数传递的符号变量。
-
CPI 边界转换：在
sol_invoke_signed_*边界，Radiant 将符号值从调用程序的上下文中转换为被调用程序的执行上下文。 -
Callee 探索：符号执行在被调用程序中继续，使用转换后的符号值探索路径。
-
约束传播：当在被调用程序中到达目标基本块（标有星号）时，Radiant 已累积了来自被调用程序的约束。 然后，这些约束通过 CPI 边界向后传播到原始调用程序输入。
-
统一约束求解：约束求解器评估来自两个程序的组合约束，从而生成满足整个跨程序执行路径的具体输入值。
实现
当 Solana 程序执行 CPI 系统调用（sol_invoke_signed_c 或 sol_invoke_signed_rust）时，Solana VM 会为被调用程序生成一个新的 VM 实例。 Radiant 通过多个调试会话连接到连续的 VM 实例来利用此架构：
调用程序和被调用程序都部署在同一个 LiteSVM 实例中。 执行调用程序 VM 时，GDB 服务器将在端口 9999 上启动。在符号执行期间，当 radius2 检测到 CPI 系统调用时，将为被调用程序生成第二个 VM 实例，并在端口 10000 上拥有自己的 GDB 服务器。Radiant 为被调用程序创建一个嵌套的 concolic execution 会话，并且满足两个程序中约束的解决方案会通过 CPI 边界传播回去。
跨 CPI 测试配置
Radiant 的跨 CPI 模式需要指定两个程序中的程序计数器位置：
##[test]
fn test_cross_cpi() -> Result<()> {
let ((caller_program_path, callee_program_path), deployment_thread) =
setup::setup_deployment();
let config = RadiantTestConfig::new(caller_program_path)
.cross_cpi_state(
0x100007ae0,
Some(0x100007d90),
0x100007c88,
0x100008bf8,
)
.callee_avoid(vec![])
.max_solutions(20)
.verbose(true);
let mut test = RadiantTest::new(config)?;
let result = test.run(SymbolizeSpec::InstructionData { length: 8 })?;
let solutions = result.into_bytes();
println!("\n[CROSS CPI] Found {} solutions", solutions.len());
for (i, sol) in solutions.iter().enumerate() {
if sol.len() >= 8 {
let amount = u64::from_le_bytes(sol[0..8].try_into().unwrap());
println!(" Solution #{}: amount = {} (0x{:x})", i + 1, amount, amount);
assert!(amount + 123 >= 666 && amount + 123 < 700,
"Callee solution {} is not in [666, 700)", amount);
}
}
Ok(())
}cross_cpi_state 配置指定：
- caller_snapshot_pc (0x100007ae0)：确定在 CPI 之前在何处快照调用程序的状态。 将此设置为 0 将自动使用调用程序的指令入口点。
- caller_target_pc (0x100007d90)：调用程序中的可选目标（或 None）
- callee_snapshot_pc (0x100007c88)：确定在 CPI 进入后在何处快照被调用程序的状态。 将此设置为 0 将自动使用被调用程序的指令入口点。
- callee_target_pc (0x100008bf8)：被调用程序中的目标基本块（panic 位置）
跨 CPI 结果
执行时，Radiant 会发现触发被调用程序 panic condition 的所有输入值：
输出显示完整的跨 CPI 分析过程：
- 部署阶段：调用程序和被调用程序都部署到同一个 SVM 实例，并通过 CPI 初始化计数器 PDA
- 交易准备：使用符号指令数据准备增量交易
- 跨程序符号执行：Radiant 跟踪符号值，因为它们通过 CPI 边界从调用程序传播到被调用程序
- 解决方案生成：发现了 20 个具体的解决方案，所有解决方案都满足
amount + 123落在 [666, 700) 范围内的约束
解决方案包括如下值：
- 解决方案 #1：金额 = 569 (0x239)，转换为 692
- 解决方案 #11：金额 = 557 (0x22d)，转换为 680
- 解决方案 #20：金额 = 564 (0x234)，转换为 687
每个解决方案都满足 amount + 123 落在 [666, 700) 范围内的约束，这演示了 Radiant 如何自动考虑调用程序的转换逻辑。
当审核由多个程序的交互产生的漏洞的可组合协议时，此功能变得很有价值。
附加功能
除了上面演示的核心符号执行功能之外，Radiant 还支持：
-
Solana 系统调用：Radiant 在符号执行期间处理 Solana 系统调用，从而可以分析依赖运行时功能（如帐户验证、加密操作和程序派生地址）的程序。
-
跨交易可组合性：来自一个交易的符号解决方案可以在后续交易中使用，并带有额外的符号值，从而可以分析多交易工作流程。
-
跨 CPI 符号执行：Radiant 使用跨 CPI 边界转换的约束上下文来使用符号解决方案，从而可以评估涉及程序组合的不变量。
-
未来的开源：我们计划在 Radiant 达到更高的成熟度并完善其功能后，将其开源。
结论
Radiant 将 concolic execution 引入 Solana 程序安全测试。 通过其双引擎架构将具体执行和符号执行相结合。
从有目标的基本块探索到跨 CPI 符号执行，该框架的功能解决了以符号方式分析可组合 Solana 程序的独特挑战。
随着 Solana 的生态系统继续变得越来越复杂，协议越来越依赖于多程序交互和复杂的 state machine，像 Radiant 这样的工具对于安全研究变得越来越重要。 此处提供的示例演示了基础，但该方法可扩展到实际的协议审核。
我们正在继续开发和完善 Radiant，并且我们期待在未来将其开源。
- 原文链接： inversive.xyz/blog/Radia...
- 登链社区 AI 助手，为大家转译优秀英文文章，如有翻译不通的地方，还请包涵～
