传统的安全机制和现代信息系统所需要的安全服务之间存在着一系列的矛盾, 如提供安全服务的安全机制的静态性和安全服务需求的动态性之间的矛盾, 以及安全保护机制部署的固定性和信息系统运行环境的动态性之间的矛盾.信息系统规模的不断扩大, 复杂性不断增加, 性能不断提高, 对安全保护机制的性能提出越来越高的要求, 使得采用单纯的硬件或软件都无法解决这些问题.这促使网络安全研究人员积极考虑采用可重构思想解决安全计算中的一系列棘手问题.2007年, 美国发布的《联邦网络空间安全及信息保障研究与发展计划(CSIA)》中曾明确指出, 可重构和可升级的安全系统是下一代先进系统和体系结构的主要研究领域之一.将可重构计算思想应用到安全系统建设和管理中, 构建可重构安全系统, 为信息安全开辟了全新的研究领域, 是信息安全发展的重要发展方向.

可重构安全计算是指以可重构硬件和软件为基础构建起来的可变安全计算架构, 能够根据计算环境或安全需求的变化, 调整内部组织结构和数据通路, 动态生成最适合当前安全需求和环境参数的软硬件计算架构为之服务, 从而达到增强安全适应性、提高安全系统性能和提高防御能力的目的.可重构安全计算具有以下几个特点:①构成系统基本元素是安全重构元; ②安全需求和环境参数具有变化性; ③能够根据安全需求或环境参数变化动态自动生成最适合当前计算环境的重构配置; ④能够验证重构配置的正确性、可达性和安全性.可重构安全计算系统根据安全需求的变化用搭积木的方式将本地或分布于网络中的软硬件安全重构元有机组织起来, 动态自动的配置成适应于安全需求变化的等级化安全服务, 向用户提供灵活高效的安全业务.

本文根据可重构安全计算的特点, 用直觉主义逻辑对可重构安全系统进行建模和表达, 提出了一种基于直觉主义逻辑扩展的动态自动可重构安全计算系统.其基本思想是:建立一个直觉主义逻辑扩展推理系统, 能够对安全需求和安全重构元进行建模和表达, 以证明携带重构元的实现代码的方式自动生成重构配置.为了便于用户描述安全重构元, 设计了面向问题的安全重构元描述方法, 并给出了基于映射关系的描述向逻辑语言的转换规则.最后, 以IPSec协议为例, 阐述了可重构安全计算系统重构配置的自动推理合成过程.

1 重构机理及逻辑语言SSPE 1.1 重构机理

重构配置的合成涉及3个层面的内容:面向问题的安全重构元描述、面向自动合成的逻辑语言和可执行的程序代码.面向问题的安全重构元描述设计目标是建立安全重构元和描述重构请求, 便于高效地转换为逻辑语言; 逻辑语言是系统的核心, 是推理的基础, 其上的语义证明查找算法决定了配置生成的效率; 可执行的程序代码是重构的结果, 即所说的重构配置.

图 1描述了动态自动的可重构安全计算系统的重构机理, 它表达了从安全需求请求到动态自动生成可执行重构程序代码的过程.

重构配置生成的推理过程分为3个阶段完成.

● 第1个阶段是安全重构元和安全需求请求建立阶段, 用户将与重构目标计算有关的安全重构元和安全需求用SRCS建模, 设Q是安全重构元的逻辑描述集合, X_i, Y_j是安全重构元的接口变量, 安全需求请求以一种面向问题的描述方式表示, 如Q↦X₁∧…∧X_n→Y₁∧…∧Y_m, 解释为:

$ {\text{Compute}}\;{Y_1} \wedge \ldots \wedge {Y_m}\;{\text{from}}\;{X_1} \wedge \ldots \wedge {X_n}\;{\text{when}}\;Q; $

● 第2个阶段是逻辑推理阶段, 推理系统将安全需求请求描述转换成逻辑语言SSPE下的直觉主义逻辑公理集合T, 若公式T↦∃ψ(X₁∧…∧X_n→Y₁∧…∧Y_m)对于每一个可解问题是可以构造证明的, 说明存在一个合法重构配置可以满足安全需求, ψ即是要求解的重构配置, 它以一种易于转换为某种现有编程语言的形式表示;

● 第3个阶段是重构配置提取阶段, 将第2阶段生成的重构配置ψ转换为可执行的程序代码.

1.2 扩展的SSP逻辑

可重构安全系统建模的逻辑基础是直觉主义逻辑^[1], 直觉主义逻辑也称为构造性逻辑, 是指在证明时必须是构造性证明.证明即是构造是直觉主义最基本的概念.在经典逻辑中, 命题的解释是它断言的某种性质的真假意义, 即命题的真值.而在直觉主义逻辑中, 命题的解释是它断言的某种性质的可构造性, 即命题所断言的性质的实际构造的实现.Kleene最早将证明项(一个预编程模块)与直觉主义逻辑推理公式结合起来^[2], 建立了编程语言与直觉主义逻辑的关系; Mint和Tyugu提出了程序自动合成方法SSP^[3], 提出了面向问题的逻辑描述方法和合成推理规则SSR, 实现了程序的自动合成, 该理论在一些编程工具中已经得到有效实践, 如Cocovila^[4], PRIZ^[5]等.

然而, 将SSP理论直接应用于可重构安全计算系统存在以下问题:首先, 安全重构元的实现是一个预编程模块, 作为公理的构造它是已知的, 但是预编程模块在执行过程中可能需要进行错误处理ERROR, 而SSP不能支持错误处理; 其次, SSP推理规则不支持分支选择结构, 而这种情况在重构处理过程中是显然存在的.因此, 我们需要对SSP理论进行改进, 引入错误处理ERROR和析取合成规则, 称这个逻辑语言为扩展SSP即SSPE.

1.2.1 SSPE逻辑公式

SSPE是SSP的扩展, 具有良好的表达能力和较高的合成效率, 非常适合描述和表达可重构安全计算系统的问题.SSPE的公式只有以下3种形式:

① 命题变量:a:A, 其中, A是命题变量, a是命题变量A对应的一个对象实例;

② 非条件计算声明公式:

$ \bigcap\limits_{i = 1}^n {{A_i}} \supset \bigcup\limits_{j = 1}^m {{B_j}\{ \lambda {a_1}...{a_n} \cdot f\} } . $

该公式表示了一个可构造的数据依赖关系λa₁…a_n·f:对于给定的输入a₁…a_n, 产生可能的输出$\vee _{j = 1}^m{b_j}$.这里, B_j可能具有形式$\wedge _{j = 1}^{{l_i}}{B_{ij}}$, λ表示法见文献[3].

③ 条件计算声明公式:

$ \wedge _{k = 1}^m{X_k} \wedge \wedge _{i = 1}^n{S_i} \supset \vee _{j = 1}^k{Y_j}\{ \lambda {x_1}...{x_n}{g_1}...{g_n} \cdot f\} . $

该公式表示一个带有子任务S_i的可构造的数据依赖关系lx₁…x_ng₁…g_n·f:对于给定的输入x₁…x_ng₁…g_n, 其中, g_i表示S_i的计算结果, 产生可能的输出$\vee _{j = 1}^k{y_j}$.这里, Y_j可能具有形式$\vee _{j = 1}^{{l_i}}{y_{ij}}$.S_i表示为一个具有未知实现e_i的非条件计算声明形式:

$ \bigcap\limits_{j = 1}^{{n_i}} {{U_{ij}}} \supset {V_i}\{ \lambda {u_1}...{u_n} \cdot {e_i}\} . $

下面通过例1说明如何用SSPE公式来描述可重构安全计算系统.

例1:IPSec协议的Outbound处理过程表示成安全重构元组合形式, 如图 2所示.

图 2是该应用的一个高阶工作流模型^[6], 从中提取出3个安全重构元Classify, Encrypt和Authenticate和一个控制变量loop1.Classify是包过滤安全重构元, 负责查找SPD, 对进入的IP包进行过滤; Encrypt是加密安全重构元, 对经过过滤的包进行加密处理; Authenticate是认证安全重构元, 对数据包进行认证处理; loop1是控制变量.

Ippacket, Ippacket-C, Ippacket-R, Ippacket-E, Ippacket-A, S是命题变量, S是一个子任务, IPpacket-R⊃IPpacket-A {λu, φ}, 其中, φ是S的未知实现.则IPSec协议的SSPE逻辑描述如下.

●  IPpacket⊃IPpacket-C{λa, classify};

●  IPpacket-R⊃IPpacket-E{λr, encrypt};

●  IPpacket-E⊃IPpacket-A{λe, authenticate};

●  IPpacket-E∧(IPpacket-R⊃IPpacket-A{λu, φ})⊃result{loop1(e, λu, φ)}.

“{}”里边的部分表示公式的构造, 在可重构安全计算系统中, 一个安全重构元的构造对应的是一段预编程代码.

1.2.2 SSPE合成规则

SSPE合成规则是推理的依据, 利用合成规则可以计算出安全重构元之间的合成关系如串行、并行、分支或迭代.重构请求是推理系统证明的目标, 重构请求的响应过程就是基于SSPE合成规则在公理集T上找到一个满足重构请求的安全重构元组合的推理过程.

定义 1.重构请求RR(reconfiguration request)表示为

$ \bigcap\limits_{i = 1}^m {{X_i}} \supset \bigcup\limits_{j = 1}^n {{Y_j}\{ \psi \} }, $

其中, X_i, Y_j为命题变量, X_i表示已知的前提条件, Y_j为希望计算的结果; ψ是使公式$\wedge _{i = 1}^m{X_i} \supset \vee _{j = 1}^n{Y_j}$成立的一个构造, 这个构造是安全重构元的一种组合关系, 即重构配置.

设Γ, Σ表示无序的公式列表L₁, …, L_k, 是推理的前提假设.为了表达方便将“{}”表示的构造部分放在主蕴含式的前面.SSPE合成规则有:

1) 蕴含引入规则SSPE1:

$ \frac{{{\mathit{{\mathit{\Gamma}}}}, u:A \mapsto m:B}}{{ \mapsto \{ \lambda u.m\} :\underset{\raise0.3em\hbox{$\smash{\scriptscriptstyle-}$}}{A} \supset B}}; $

2) 串行结构合成规则SSPE2:

$ \frac{{{\mathit{\Gamma}} \mapsto m:\underset{\raise0.3em\hbox{$\smash{\scriptscriptstyle-}$}}{A} \supset B \wedge \underset{\raise0.3em\hbox{$\smash{\scriptscriptstyle-}$}}{C} ;{\mathit{\Gamma}} \mapsto n:B \wedge \underset{\raise0.3em\hbox{$\smash{\scriptscriptstyle-}$}}{W} \supset G}}{{{\mathit{\Gamma}} \mapsto \{ m;n\} :\underset{\raise0.3em\hbox{$\smash{\scriptscriptstyle-}$}}{A} \wedge \underset{\raise0.3em\hbox{$\smash{\scriptscriptstyle-}$}}{W} \supset G \wedge \underset{\raise0.3em\hbox{$\smash{\scriptscriptstyle-}$}}{C} }}; $

3) 迭代结构合成规则SSPE3:

$ \frac{{ \mapsto F:(\underset{\raise0.3em\hbox{$\smash{\scriptscriptstyle-}$}}{A} \supset B) \wedge \underset{\raise0.3em\hbox{$\smash{\scriptscriptstyle-}$}}{C} \supset D;{\mathit{\Gamma}}, \underline {u:A} \mapsto m:B;\underline { {\mathit{\Sigma }} \mapsto n:C} }}{{{\mathit{\Gamma}}, {\mathit{\Sigma }} \mapsto \{ \lambda \underset{\raise0.3em\hbox{$\smash{\scriptscriptstyle-}$}}{u} .m, \underset{\raise0.3em\hbox{$\smash{\scriptscriptstyle-}$}}{n} \} :D}}; $

4) 分支结构合成规则SSPE4:

$ \frac{{ \mapsto m:\underset{\raise0.3em\hbox{$\smash{\scriptscriptstyle-}$}}{W} \supset A \vee B;\underline {{\mathit{\Gamma}} \mapsto n:W} ;{\mathit{\Sigma }}, u:A \mapsto {n_1}:C;\Delta, w:B \mapsto {n_2}:C}}{{{\mathit{\Gamma}}, {\mathit{\Sigma }}, \Delta \mapsto \{ case \; m \;\underset{\raise0.3em\hbox{$\smash{\scriptscriptstyle-}$}}{n} \; of \; in{l^B}u \Rightarrow {n_1}|in{r^A}w \Rightarrow {n_2}\} :C}}; $

5) 终止消除规则SSPE5:

$ \frac{{{\mathit{\Gamma}} \mapsto m: \bot }}{{{\mathit{\Gamma}} \mapsto \{ abor{t^c}m\} :C}}; $

6) 量词∀消除规则SSPE6:

$ \frac{{{\mathit{\Gamma}} \mapsto m:\forall x.A}}{{{\mathit{\Gamma}} \mapsto \{ mt\} :[t/x]A}}; $

7) 量词∃消除规则SSPE7:

$ \frac{{{\mathit{\Gamma}} \mapsto m:\exists x.A;{\mathit{\Gamma}}, u:[a/x]A \mapsto [a/x]n:C}}{{{\mathit{\Gamma}} \mapsto \{ let\langle x, u\rangle = \min n\} :C}}. $

SSPE合成规则是由SSP基本推理规则推导而来, 其完备性证明参见文献[3].

2 面向问题的等级化安全重构元描述

安全重构元作为可重构安全计算系统的基本元素, 是搭建系统的“积木”.安全重构元描述处于自动推理系统的第1个级别, 其主要目的是提供一种便于用户理解的方式建立安全重构元和表达安全需求, 并且能够高效地转换为第2级别上的逻辑语言.本节依据已建立的SSPE逻辑系统设计了安全重构元描述方法, 以下简称SRCS(security reconfigurable component specification).

定义 2(安全重构元(security reconfigurable component, 简称SRC)).安全重构元是具有独立功能、与上下文紧密相关、接口具有统一描述规范、能够提供多种不同等级安全服务、具有逻辑推理能力的软件实体.安全重构元可以形式化地描述为一个四元组〈ID, MetaInterface, Function, Detail〉, 其中:ID是安全重构元的唯一标识; MetaInterface是元接口, 描述了安全重构元接口变量和接口变量之间的内部数据依赖关系以及安全重构元之间的绑定关系等, 是推理的基本依据; Function是功能模块集合, 表示安全重构元数据依赖关系的具体实现; Detail是安全重构元的描述信息, 包括功能、安全属性、可靠性等.

定义 3(元接口 MetaInterface). MetaInterface是一个五元组〈MI, InterfaceVariable|constant|Metavariable, Binding, Relation, SecProperlist〉, 其中,

●  MI是元接口名字;

●  InterfaceVariable是接口变量, 包括安全重构元的输入变量和输出变量, 其描述形式如下:

$ InterfaceVariable:: = Indentifier::Specifier. $

其中, Indentifier是接口变量的唯一名字, 对应于逻辑中一个命题变量; Specifier是接口变量的类型, 类型可以是编程语言中的任意基本类型, 也可以是元接口或安全重构元标识:

$ Specifier:: = int\left| \ldots \right|float|MetaInterface|SRC. $

●  Constant是常量, 对应于逻辑中的断言.其描述形式:

$ Constant:: = InterfaceVariable\{ val\} . $

其中, val是目标程序语言中的常量;

●  Metavarible是元变量, 元变量是一种特殊的接口变量, 元变量的值由安全重构元实例或元接口实例指派, 其形式如下:

$ Metavarible:: = Metavarible = (MetInterfacename|SRCname). $

其中, MetInterfacename是元接口标识, SRCname是安全重构元标识, 实例的具体实现则在合成过程中进行计算.元变量可能出现在Binding和Relation中;

●  Binding是接口变量之间的绑定关系, 其描述形式:

$ \begin{array}{l} Name:: = Indentifier\left\lfloor {.Name} \right\rfloor ; \hfill \\ Binding:: = Name = Name. \hfill \\ \end{array} $

表示两个接口变量的实现必须具有相同的值.其中, Name可以是名字标识Indentifier也可以是复合名字.例如, Encrypt.IPpacket表示接口变量Encrypt的接口变量IPpacket;

●  Relation表示接口变量之间的数据依赖关系, 对应于逻辑中的一个公理.

Relation描述了安全重构元能够提供的所有的计算能力, 通常用蕴含式表示:

$ Relation:: = \\ [IndentifierList[, SubtaskList]] \to Indentifier[|Alternatives]|ERROR\{ realization\} . $

其中,

$ \begin{array}{l} IdentifierList:: = Identifier[, IdentifierList]; \hfill \\ Alternatives:: = Identifier[|Alternatives]; \hfill \\ SubtaskList:: = Subtask[, SubtaskList]. \hfill \\ \end{array} $

蕴含符号左部代表输入参数, 可以是接口变量或子任务, IdentifierList是的接口变量列表, SubtaskList代表子任务列表.蕴含符号右部代表输出参数, 可以是接口变量Identifier或其他可选参数Alternatives, 也可能是ERROR, ERROR是一个常量, 表示错误处理.realization对应一个实现程序.Relation表达了当所有的输入参数已知或是可计算时, 它的实现realization是可用的, 输出形式为蕴含式右部的参数列表.

●  SecProperties是安全属性, 它描述了安全重构元的提供的安全服务类型和安全等级.其形式如下:

$ \begin{array}{l} SecProperty(type, levelx) \hfill \\ type \in \{ confidentiality, integrity, non{\text{- }}repudiation, access control, authentication\} \hfill \\ levelx \in [0, n], n \in N \hfill \\ \end{array} $

根据ISO7498的定义, 安全服务类型包括机密性(confidentiality)、完整性(integrity)、抗抵赖性(non- repudiation)、访问控制(access control)、认证(authentication)这5种, 每种类型的安全重构元划分成若干等级, 用levelx表示, 其中, levelx∈[0, n], n∈N, 若干不同种类、不同级别的安全重构元组合而成的安全服务形成多样的安全保障等级.

定义 4(子任务 Subtask). Subtask是一个没有实现部分的Relation函数, 子任务不能独立存在, 一般作为关系Relation的前置条件出现在蕴含式的左部.其形式如下:

$ Subtask:: = [IdentifierList] \to Identifier\{ \varphi \} . $

IdentifierList是输入接口变量列表, 可以为空; Identifier是输出接口变量; φ表示子任务未知的实现.

定义 5(重构请求).重构请求定义了一个待求解的安全重构元组合描述y, 其形式化描述如下:

$ \begin{array}{l} RR:: = MetaInterfaceList \mapsto [Assumptions] \to [MetaInterfaceList.]Identifier\{ \psi \}, \hfill \\ MetaInterfaceList:: = MetaInterfaceName[, MetaInterfaceList], \hfill \\ Assumptions:: = [MetaInterfaceName.]Identifier[, Assumptions], \hfill \\ \end{array} $

其中, MetaInterfaceList↦[Assumptions]作为安全重构元组合ψ的输入; MetaInterfaceList是元接口标识列表, 它保证了参与查询评估的元接口数量的有限性, 是推理的前提; Assumptions是参与重构过程的输入参数列表, 是已知的或可计算的, 参数可以是元接口变量, 也可以是子任务Subtask; [MetaInterfaceList.]Identifier安全重构元组合ψ的输出是接口变量列表.

定义 6(控制变量 Control).控制变量^[6]是一个实现函数, 用于表示重构运算过程中的循环、选择、递归等控制操作, 其形式如下:

$ Control:: = [InputParameterList\left] \to \right[OutputParameterList]\{ control\} . $

其中,

$ \begin{array}{l} InputParameterList:: = InputParameter[, InputParameterList], \hfill \\ OutputParameterList:: = OutputParameter[, OutputParameterList]. \hfill \\ \end{array} $

InputParameterList是控制变量的输出参数列表, 可以是接口变量也可以是子任务; OutputParameterList是输出参数列表.

下面我们以上述例1中的IPSec协议为例, 说明安全重构元的描述方法.

以安全重构元Encrypt为例, 其SRCS描述如下:

其中, IPpacket-R, IPpacket-E为接口变量; Auth是元变量, Auth=(Authenticate)表示为元变量Auth赋予一个Authenticate实例; Auth.IPpacket-E=IPpacket-E是绑定关系, 表示当前安全重构元Encrypt与一个Authenticate实例具有一个共享接口变量IPpacket-E; IPpacket-R→IPpacket-E{Encrypt}是一个数据依赖关系Relation, 其含义为“Encrypt是已知可构造的, 若命题变量IPpacket-R可构造, 则IPpacket-E是可计算的”; SecProperty(confidentiality, level2)表示安全重构元Encrypt的安全属性, 其安全类型是confidentiality, 安全等级为level2.

控制变量loop1的SRCS描述如下:

$ Loop1::Classify. IPpacket-C \wedge Encrypt.IPpacket-R \\ \to Authenticate.IPpacket-A\{ \varphi \} \to result\{ Loop1\} . $

其中, 蕴含式左部包含一个子任务Subtask::IPpacket-R→IPpacket-A{φ}, Loop1控制该子任务的重复执行.

3 基于映射关系的逻辑语义转换

本节提出了基于映射关系的SRCS向SSPE的逻辑语义转换方法, 详细阐述了各类表达式如接口变量与常量、绑定、关系、安全属性等的转换规则.

为了保证逻辑系统上证明查找算法的有效性以及可终止性, 我们假设安全重构元满足以下属性:设MI是一个安全重构元, 若(x₁, x₂, …, x_k)是构成该重构元的基本元素, 则MI是可计算的当且仅当:

$ MI \to {x_1}, {x_2}, \ldots, {x_k} \wedge {x_1}, {x_2}, \ldots, {x_k} \to MI. $

3.1 符号定义

为了阐述方便, 先规定一些符号的含义.

●  τ表示目标编程语言的有效类型集合;

●  C表示组件(名字)集合;

●  S表示接口变量和常量的集合;

●  O表示对象前缀集合.对象前缀确保不丢失信息的展开元接口, 它是一个复合名字, 如Encrypt.En.其构造方式如下:假设系统当前对象前缀为IPsec, 要展开一个元接口Encrypt::MI, 则添加名字Encrypt到当前对象前缀IPsec, 使用IPsec.Encrypt作为对象前缀来展开元接口Encrypt::MI, 则元接口中接口变量常量转换为逻辑语言时都需要添加当前对象前缀IPsec.Encrypt, 如IPsec.Encrypt.En, 从而保证了每一个接口变量常量在展开描述过程中具有一个唯一的名字;

●  a, b表示描述语言SRCS的合法语法结构, 其具体语法依赖于它们出现的上下文, 既可以是简单名字也可以是复合名字, 还可以是一个子任务描述或是公理主蕴含式的左部或右部;

●  v表示接口变量和常量的名字的集合;

●  r表示接口变量和常量的实现集合;

●  Val表示目标编程语言的常量集合;

●  M表示由公理实现的模型的名字集合;

●  SP表示安全属性集合;

●  id表示一个恒等函数, 这个函数是可以重载的, 适合需要的类型.

3.2 映射函数

定义 7(语义函数 L^P).设Sexp是一个有效的SRCS描述表达式, O是对象前缀的集合, 设LForm代表逻辑语言SSPE的有效公式.SRCS描述表达式的逻辑语义由以下函数定义:

$ {L^P}:sexp \to (O \to LForm). $

该公式表示从SRCS描述表达式到逻辑语言SSPE的映射关系.

定义 8(展开函数 Unfold). Unfold是关于一个元接口名子MI和对象前缀O的函数, 用于产生一个SSPE逻辑公式集合, Unfold函数将语义函数L^P应用于给定元接口的每一个描述表达式sexp:

$ Unfold(MI, O) = \{ {L^P}\left[\kern-0.15em\left[{sexp} \right]\kern-0.15em\right](O)sexp \in sp(MI)\} . $

其中, sp是一个辅助函数, 用于产生元接口MI的SRCS描述表达式集合.

3.3 逻辑转换规则

下面具体定义SRCS中各类表达式的逻辑语义.

转换规则 1.设o, o∈O是当前对象前缀, v是接口变量, 且v::S, 若S∈τ, 则r_s:o.v, r_s表示o.v的实现, “:”代表实现; 若S∉τ, 则r_s:o.v∪Unfold(S, o.v), Unfold(S, o.v)表示元接口S的SRCS描述表达式使用新的对象前缀o.v, 其形式如下:

$ {L^p} [\kern-0.15em[ v::S ]\kern-0.15em] (o) = \left\{ {\begin{array}{*{20}{l}} {{r_s}:o.v, \;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\; {\text{ if }}S \in \tau } \\ {{r_s}:o.v \cup unfold(S,o.v),{\text{ otherwise}}} \end{array}} \right. $

转换规则 2.设o, o∈O是当前对象前缀, v是一个接口常量, 且v::S{val}, 则:

$ {L^P}\left[\kern-0.15em\left[{v::S\{ val\} } \right]\kern-0.15em\right](o) = {L^P}\left[\kern-0.15em\left[{v::S} \right]\kern-0.15em\right](o) \cup {L^P}\left[\kern-0.15em\left[{ \to v\{ val\} } \right]\kern-0.15em\right](o). $

转换规则 3.设o, o∈O是当前对象前缀, (C)是一个元变量, l表示公理蕴含式的左部, r表示公理蕴含式的右部, 则:

$ {L^P} [\kern-0.15em[(C)]\kern-0.15em] (o) = \left\{ {\begin{array}{*{20}{l}} {\forall wC(w), {\text{ if }}p = l} \\ {\exists wC(w), {\text{ if }}p = r} \end{array}} \right. $

转换规则 4.设o, o∈O是当前对象前缀, flalsity表示错误处理, 则:

$ {L^P}\left[\kern-0.15em\left[{falsity} \right]\kern-0.15em\right](o) = F. $

转换规则 5.设o, o∈O是当前对象前缀, [control]是控制变量, 则:

$ {L^P}\left[\kern-0.15em\left[{[control]} \right]\kern-0.15em\right](o) = control. $

转换规则 6.设o, o∈O是当前对象前缀, a=b是元接口的一个绑定关系, id是一个恒等函数, 则:

$ \begin{array}{l} {L^P} [\kern-0.15em[a = b]\kern-0.15em] (o) = {L^P} [\kern-0.15em[a \to b\{ id\}]\kern-0.15em] (o) \cup {L^P} [\kern-0.15em[b \to a\{ id\}]\kern-0.15em] (o) \hfill \\ {L^P} [\kern-0.15em[a \to b\{ id\}]\kern-0.15em] (o) = id:{L^P} [\kern-0.15em[a \to b]\kern-0.15em] (o) \hfill \\ \end{array} $

转换规则 7.设o, o∈O是当前对象前缀, m是一个公理的实现, 则:

$ {L^P} [\kern-0.15em[a \to b\{ m\}]\kern-0.15em] (o) = \left\{ {\begin{array}{*{20}{l}} {m:{L^P} [\kern-0.15em[a \to b]\kern-0.15em] (o), \;\;\;\;\;\;\;\;\;\;\;\;\;{\text{ if }} \;m\; {\text{is constructor}}} \\ {(r_S^o, m):o \wedge {L^P} [\kern-0.15em[a \to b]\kern-0.15em] (o), {\text{ otherwise}}} \end{array}} \right. $

公理蕴含式也满足下列转换规则:

$ \begin{array}{l} {L^P} [\kern-0.15em[MI \mapsto a \to b]\kern-0.15em] (o) = {L^P} [\kern-0.15em[a \to b]\kern-0.15em] (o.MI) \hfill \\ {L^P} [\kern-0.15em[\to a]\kern-0.15em] (o) = T \supset {L^P} [\kern-0.15em[a]\kern-0.15em] (o) \hfill \\ {L^P} [\kern-0.15em[a \to b]\kern-0.15em] (o) = {L^l} [\kern-0.15em[a]\kern-0.15em] (o) \supset {L^r} [\kern-0.15em[b]\kern-0.15em] (o) \hfill \\ {L^P} [\kern-0.15em[a \to b\{ val\}]\kern-0.15em] (o) = val:{L^P} [\kern-0.15em[a \to b]\kern-0.15em] (o) \hfill \\ {L^P} [\kern-0.15em[a, b]\kern-0.15em] (o) = {L^P} [\kern-0.15em[a]\kern-0.15em] (o) \wedge {L^P} [\kern-0.15em[b]\kern-0.15em] (o) \hfill \\ {L^P} [\kern-0.15em[a|b]\kern-0.15em] (o) = {L^P} [\kern-0.15em[a]\kern-0.15em] (o) \vee {L^P} [\kern-0.15em[b]\kern-0.15em] (o) \hfill \\ \end{array} $

转换规则 8.设o, o∈O是当前对象前缀, SecProperty(type, levelx)是元接口安全属性, 则:

$ {L^P}\left[\kern-0.15em\left[{SecProperty(type, levelx)} \right]\kern-0.15em\right](o) = o.Secproperty(type, levelx). $

举例:以上述例1中IPsec协议安全重构元Encrypt为例, 将其转换为逻辑语言SSPE如下:

$ \begin{array}{l} \begin{array}{*{20}{l}} {//Extend axioms} \\ {r:Encrypt} \\ {id:\forall x.Encrypt(x) \supset Encrypt} \\ {id:Encrypt \supset \exists x.Encrypt(x)} \\ {//Interface variables} \\ {{X_1}:Encrypt.IPpacket-R} \\ {{X_2}:Encrypt.IPpacket-E} \\ {{X_3}:Encrypt.Auth} \\ {//Metavariables:Auth = (Authenticate)} \\ {Id:\forall x.Authenticate(x) \supset Encrypt.Auth} \\ {Id:Encrypt.Auth \supset \exists x.Authenticate(x)} \\ {//Binding:Auth.IPpacket-E = IPpacket - E} \\ {Id:Encrypt.Auth.Ippacket - E \supset Encrypt.IPpacket - E} \\ {id:Encrypt.IPpacket - E \supset Encrypt.Auth.Ippacket - E} \\ {//Relation:IPpacket - R \to IPpacketE\{ Encrypt\} } \\ {Encrypt:Encrypt.IPpacketR \to Encrypt.IPpacket - E} \\ {//SecProperty:SecProperty(confidentiality, level2)} \end{array} \hfill \\ \Pr :Encrypt.SecProperty(confidentiality, level2) \hfill \\ \end{array} $

其中, 扩展公理Extend Axioms用于引入一个Encrypt安全重构元实例, id:∀x.Encrypt(x)⊃Encrypt和id:Encrypt⊃∃x.Encrypt(x)是等价关系Encrypt=(Encrypt)的展开式; X₁, X₂和X₃分别是接口变量Encrypt.Ippacket-R, Encrypt. IPpacket-E和Encrypt.Auth的别名; 元变量Auth=(Authenticate)引入一个Authenticate安全重构元实例; 绑定关系Auth.IPpacket-E=IPpacket-E展开为两个等价式Id:Encrypt.Auth.Ippacket-E⊃Encrypt.IPpacket-E和id:Encrypt. IPpacket-E⊃Encrypt.Auth.Ippacket-E; Encrypt:Encrypt.IPpacket-R→Encrypt.IPpacket-E是公理展开式, Encypt是数据依赖关系的具体实现, 对应编程语言中一个函数模块; SecProperty(confidentiality, level2)是安全属性.

4 动态自动重构配置生成

所谓动态自动重构, 是指给定一个重构请求, 系统可以通过逻辑的智能推理, 自动地计算出满足重构请求的配置, 这个过程不需要人工介入.Q是安全重构元逻辑描述集合, 要得到一个由Q可计算的安全需求请求Q↦X₁∧…∧X_n→Y₁∧…∧Y_m, 首先, 用户对问题通过SRCS进行建模和表达, 逻辑语言转换器自动将SRCS转换为逻辑语言SSPE, 产生安全重构元逻辑描述集合Q, 推理系统将安全需求逻辑描述和Q转换成逻辑语言SSPE下的直觉主义逻辑公理集合T, 若公式T↦∃ψ(X₁∧…∧X_n→Y₁∧…∧Y_m)对于每一个可解问题是可以构造证明的, 说明存在一个合法重构配置可以满足安全需求, 其中, ψ即是要求解的重构配置.

下面以上述IPSec协议重构为例, 给出可重构安全计算系统重构目标自动合成过程:

设重构目标为IPpacket→result{φ}.该例中有3个安全重构元Classify, Encrypt和Authenticate, loop1是控制变量, 其SRCS描述如图 3所示.

将各安全重构元按照第3节所述方法展开得到逻辑表达式集合Q, Q与安全需求(重构请求)及推理系统规则构成直觉主义逻辑公理集合T, 限于篇幅, 这里我们只给出与推理有关的公理集(*), 如下:

根据SSPE推理规则, 推导过程如下:

从图 4我们看到, 推理过程构成一颗推理树, 其中, 叶子结点代表公理, 中间结点代表推理规则, 重构配置在推导过程中逐步生成.首先得到{Encrypt; Authenticate}, 然后得到{loop(Encrypt; Authenticate)}, 最后得出:

$ \varphi = \{ Classify;loop(Encrypt;Authenticate)\} . $

合成方法能够计算一种应用的多种不同构型, 也能计算一个安全重构元集合上能够被满足的所有重构请求, 即这个集合上的构型变化能力, 这些工作会在下一步工作中深入研究.

5 相关研究

目前, 能够提供高灵活性、适应性和可扩展性安全服务的可重构安全计算系统, 已成为安全研究领域的热点问题^[7].一些学者从可重构安全计算系统软硬基础平台出发研究重构方法, 麻省理工大学Eddie博士提出了基于数据转发层面的可重构路由开发平台Click系统^[8], Click系统配置文件完全由手工编写, 不能适应新网络安全环境下动态多变的安全需求.该系统通过用户手工编写配置文件将系统中各重构组件有机结合起来, 实现路由器的功能重构.Paul等人^[9]提出一种可重构SSL/TLS安全处理体系, 所有的加密、哈希函数、密钥交换算法以比特文件的形式存储在SD卡上, 利用FPGA平台的部分重构能力, 可动态地执行嵌入式系统中的应用.该方法只对安全系统的局部实施重构, 重构能力非常有限.文献[10]提出一种高性能的实现IPSec协议和SSL协议加速的网络安全处理器系统体系NSP.使用基于特定域描述指令集的可编程并行密码引擎阵列, 控制流将数据包分段并将其配置到密码引擎阵列, 有效提高系统的吞吐率.这些研究说明在有限的可重构软硬件资源上实现复杂的安全系统是有可能的.

一些学者对可重构安全计算系统的体系结构展开研究, 文献[11]基于SDN(软件自定义网络)/NFV(网络功能虚拟化)体系架构, 提出通过组合虚拟安全服务模块来构建安全服务链(security service chain, 简称SSC)的思想, 但是并没有给出安全服务链接组合的具体方法.文献[12]提出FRESCO安全架构, 其以安全模块组合的方式生成安全服务, 但仅给出了功能上的验证.文献[13]提出通过网络功能单元的组合实现节点对应用需求的自适应匹配.

还有一些学者在重构机理方面展开研究, 文献[14]提出了基于构件的层次化可重构网络体系结构以及基于进程代数的重构原则、模型和功能实体的重构方法, 实现了构件过程的自主性、反应性和主动性.但是该体系采用静态功能候选集模板实现重构配置的生成, 其灵活性依赖于功能候选集模板的配置, 重构构件之间不能实现灵活的自动组合, 主动性具有局限性.文献[15]将可重构系统定义为构件及构件上的运算集合, 建立可重构系统代数模型, 提出了可重构安全服务之间相互转换的代数运算方法.该方法能够计算特定构件集合上的构型变化能力和对构件的可替换性进行验证, 但该方法没有考虑安全需求的变化性, 不能根据需求变化灵活计算重构构型.文献[16]提出一种可同时支持软件构件和硬件构件的参数化可重构构件模型, 基于此模型, 提出了混合可重构系统上构件设计空间的快速搜索算法.该方法同样基于静态功能候选集模板, 其灵活性受限制.文献[17]提出一种软件自定义网络的安全服务链动态组合机制, 建立了基于向量空间和整数规划的组合模型, 利用人工智能方法实现快速的配置生成.但是该方法的安全服务链是根据安全服务功能编排模板构建的, 缺乏灵活性.

以上这些研究虽然能够提高系统的灵活性、适应性和扩展性, 但是可重构系统的配置生成方法主要采取手动配置或者是基于重构配置模板的半自动匹配方式来实现, 而人工介入方式易增加系统的脆弱性.可重构安全计算系统作为一种灵活的主动防御机制, 应该具有动态自动适应安全需求和环境参数变化的能力, 避免人工介入的导致脆弱性, 同时考虑安全服务等级和效能属性, 为当前安全需求提供最合适的安全服务, 而这方面当前鲜少有人研究.为此, 本文重点研究了可重构安全计算系统的动态自动配置生成方法, 主要借鉴了程序自动合成理论.Mints与Tyugu提出一种基于直觉主义逻辑^[3]的程序自动合成理论SSP, 将属性与属性之间的函数约束关系描述为直觉主义逻辑公式, 利用逻辑推理规则能够自动合成程序, 并将SSP应用于仿真软件、工程计算软件和安全监测等领域^[18].文献[19]将直觉主义逻辑的推理能力应用于语义Web领域, 实现了Web服务的自动组合.我们有理由相信, 基于直觉主义逻辑的程序自动合成理论同样可以应用于可重构安全计算系统的重构配置自动生成.

本文的主要贡献在于提出了一种有效的可重构安全计算系统的建模和表达方法, 能够动态自动生成适应安全需求和效能属性变化的重构配置, 为用户提供具有高灵活性、适应性和可扩展性的安全服务, 为进一步研究可重构安全计算系统构型变化能力和验证安全服务的正确性和安全性打下基础.

6 总结

本文对可重构安全系统的自动重构机理进行了深入的理论研究.在程序自动合成理论SSP的基础上, 给出了一种从面向安全重构元的问题描述语言到可执行的重构配置程序的有效方式, 提出了一种改进的逻辑语言SSPE和安全重构元建模语言SRCS, 以及SRCS到SSPE的逻辑语义转换规则.SSPE与SSP不同的是:SSP理论的研究对象是程序的最小数据类型, 而SSPE的研究对象是安全重构元.SSP理论不能完全适应可重构安全计算系统的建模和表达, 因此我们对SSP中的公式, 即条件和非条件计算声明语句以及推理规则进行了改进, 引入了分支结构和错误处理的消除规则, 并通过实例证明了SSPE的可行性和正确性.SSPE存在一个主要问题是安全重构元展开后可能产生的公理数量庞大, 需要在设计高效的自动查询评估算法方面做进一步研究.