Page 220 - 《软件学报》2025年第10期
P. 220
张建标 等: 面向联盟链的智能合约行为可信验证机制 4617
(3) 单个合约的行为集 B, 其中行为 α 由所有行为单元 a 连接而成;
P(X), 预期行为规则集规定了合约行为符合预期时的规则, 其中 X α 所需满足的
(4) 预期行为规则集 是行为
安全条件.
定义 1. 合约行为定义为主体使用函数对客体进行操作, 如公式 (1).
A = {action = (s) applies ( f) to (obj) in (env)|s ∈ subjects, f : functions, obj : objects, env : environment} (1)
其中, subjects 为主体集, functions 为函数集, objects 为客体集, environment 为环境状态. 其中主体主要指合约, 函
数集主要指合约内置的函数操作 (初始化, 调用, 删除等), 客体集主要指区块链账本或外部库等, 环境主要包括沙
箱等, 合约行为定义为合约通过内置的函数对区块链账本进行读或写操作. 合约行为的表现形式定义为系统调用
序列. 因此, 对于每个行为单元来说, 主体是系统调用, 客体是文件, 操作是系统调用对文件进行读写等, 环境指内
存环境等.
定义 2. 合约行为序列定义为合约在某一行为发生过程中所触发的系统调用序列, 如公式 (2).
α = a 1 ,a 2 ,...,a n a i ∈ system call (2)
其中, α 代表智能合约的一个行为, a 1 ,a 2 ,...,a n 表示这一行为执行过程中所触发的系统调用组成的序列. 合约的功
能是通过有序的代码段来实现的, 若代码执行的顺序不正确, 该功能就会出错. 因此合约的某一特定功能, 其行为
序列是固定的. 系统调用在检测行为是否符合预期方面具有较好的特性, 只需要通过系统调用序列与预期的差异
来判定一个合约是否可信. 系统调用是智能合约向区块链系统发出的访问资源的请求, 例如发送交易、读写数据、
获取时间戳等, 是合约行为的最小粒度, 它可以提供最细致和完整的行为信息, 因此可以通过比较系统调用序列与
预期的差异来判定合约行为的可信. 智能合约代码一般体量较小, 适合通过系统调用描述合约行为过程, 因此, 本
文以系统调用作为合约的最小行为单元, 以系统调用序列构建合约行为.
定义 3. 行为可信的定义为行为符合预期, 如公式 (3).
∀i = 1,2,...,n, ∀a i ∈ α, Actual(s 0 ,α,a i ) = Expected(s 0 ,α,(P(a i ),a i )) (3)
其中, Actual(s 0 ,α,a i ) 表示行为 α 的实际执行结果, Expected(s 0 ,α,(P(a i ),a i )) 表示在满足预期行为规则的条件下,
α 中的任意系统调用均满足预期行为规则, 即合约行为符
行为 α 的预期执行结果. 如果等式成立, 则表示对于行为
P(X) 的满足性决
合预期, 因而是可信的. 合约的行为是否可信是由作为其行为单元的系统调用针对预期行为规则
定的. 合约行为可信不仅讨论每一个行为单元的条件满足性, 还要考虑其执行顺序, 以及合约自身完整性、执行环
境等是否满足条件.
3.2 整体架构
智能合约行为可信验证机制的整体架构, 如图 2 所示. 主要包括预处理和主动监控机制两部分, 其中预处理包
括控制流图生成、行为特征提取两个模块, 主动监控机制包括合约行为控制、合约行为度量、合约行为判定这 3
个模块.
本文的可信验证机制建立在合约的初始状态可信的安全假设之上.
(1) 控制流图生成模块构建合约的控制流图, 并将其发送给行为特征提取模块.
(2) 行为特征提取模块以控制流图为输入, 输出合约的预期行为规则及基准值并发送到主动监控机制.
(3) 合约行为控制模块拦截合约运行时的系统调用实现对合约的运行时监控, 并根据判定结果实施控制.
(4) 合约行为度量模块依据度量策略对控制机制返回的行为信息度量, 并将度量结果发送到判定模块.
(5) 合约行为判定模块根据可信基准库和度量结果对合约行为进行综合判定.
可信策略管理中心: 对区块链策略制定、下发、维护存储等集中管理的平台, 区块链策略包括但不仅限于节
点访问控制、身份验证等.
行为基准库: 主要提供可信基准值数据, 包括但不仅限于智能合约源码、合约控制流图、预期行为规则等基
准值数据. 本文行为基准库的获取在确保可信的共识节点上进行合约运行过程监测, 并对合约运行过程加载的静
态数据进行完整性度量, 度量完成后将度量值存储到行为基准库中.

