运行时目标模型中的变化率与聚合建模

### 运行时目标模型中的变化率与聚合建模 #### 1. 变化与聚合目标 Kubernetes用例催生了一种新颖的目标分类法，引入了两种新的目标类型：微分目标（Differential goals）和积分目标（Integral goals），这些新目标类型目前即使在复杂的时态逻辑（如CTL和LTL）或最先进的模型检查器中也未得到支持。 - **微分目标**：许多用例场景涉及逐步增加或减少供应的目标，这些都是关于微分或变化率的陈述。从目标语言扩展的底层语义来看，在每条路径上，在指定的上下界之间（例如使用UNTIL和UNLESS时态运算符指定），某个数值变量的变化率应等于、不超过或不小于某个值。用 $D(F, start, end) \ op \ k$ 表示函数 $F$ 的变化率在条件 $start$ 为真的第一个状态到条件 $end$ 为真的第一个状态之间的区间结束时满足与常量 $k$ 的不等式 $op$。若 $F$ 的变化率无条件成立，则省略 $start$ 和 $end$。例如，存储容量以每分钟不超过2GB的速率恢复可形式化为： $D(StorageCapacity, attackMitigated \land reducedStorage \land now - 2min, now) \leq 2$ - **积分目标**：类似于用微分指定目标，也可以用定积分指定目标，例如在某些上下界之间的停机总时长应等于（或不小于、不大于）某个值。用 $I(F, start, end) \ op \ k$ 表示函数 $F$ 的定积分在条件 $start$ 为真的第一个状态到条件 $end$ 为真的第一个状态之间的所有状态中满足与常量 $k$ 的不等式 $op$。例如，IP电话服务在检测到DOS攻击到完全恢复正常运行期间的总停机时间不应超过2小时，可形式化为： $I(notAvailable(IPTelephony), attackDetected, operationsRestored) \leq 2$ #### 2. 扩展形式化 - **Ext - LTL**：在线性时间设置下，作为LTL的扩展。设 $H$ 为状态历史，对于 $H$ 中的 $s_i$，设 $s_m$ 和 $s_n$ 是该历史中的状态，$m \leq i \leq n$，$s_m$ 是条件 $start$ 为真的第一个状态，$s_n$ 是 $s_i$ 之后条件 $end$ 为真的第一个状态。则 $(H, s_i) \models D(F, start, end) \ op \ k$ 当且仅当 $\frac{| F_n - F_m |}{| n - m |} \ op \ k$；$(H, s_i) \models I(F, start, end) \ op \ k$ 当且仅当 $\#S_F \ op \ k$，其中 $\#S_F$ 表示在 $start$ 和 $end$ 条件之间 $F$ 为真的状态数量。 - **Ext - CTL**：在分支时间设置下，作为CTL的扩展。Ext - CTL表达式的积分和微分目标是在相应的Ext - LTL表达式前加上 $A$ 和 $E$，具有通常的路径上的全称和存在量化语义。 #### 3. 滑动窗口目标 还可以提出微分和积分目标的变体，如滑动窗口微分和积分目标。以积分目标为例，要确保服务总停机时间在过去24小时内不超过2小时，可形式化为 $I^-(notAvailable(IPTelephony), 24) \leq 2$。一般来说，滑动窗口积分目标写为 $I^-(F, w) \ op \ k$，等价于积分目标 $I(F, t_0 - w, t_0) \ op \ k$，其中滑动窗口宽度为 $w$ 个时间单位，结束时间为 $t_0$。滑动微分目标定义类似：$D^-(F, w) \ op \ k$ 表示 $D(F, t_0 - w, t_0) \ op \ k$。 #### 4. 网络安全用例与目标模型 - **Kubernetes框架**：Kubernetes管理应用程序部署和运行的节点集群，节点可以是物理或虚拟机，包含多个Pod，每个Pod由多个容器组成。Kubernetes支持基本的自我修复、手动和自动（基于资源）扩展、应用程序/容器的管理升级和回滚等功能。但信息和决策处于低级水平，通过探针查询Kubernetes状态和监控信息，通过效应器对Kubernetes配置采取行动，将信息和决策提升到目标级别，可基于更高级别的目标和态势感知对框架进行额外控制。 - **目标模型**： - **目标分类**：基于i*框架的目标分解概念，结合Tropos4AS中的依赖和抑制关系。有三种主要目标类别：Achieve - goals在指定条件下一次性满足；Maintain - goals在指定条件在一段时间内保持时满足；Perform - goals（或Manual Goals）通过执行相关活动满足。 - **目标生命周期**：以Active状态为中心，Suspended状态允许目标暂时不被考虑，后续可重新激活，Dropped状态表示目标被丢弃。触发关系导致一个目标的实现引发向不同上下文的转换，在每个上下文中，可能适用不同的目标集。 - **目标元模型**：包含i*