软件学报安全攸关软件系统建模与验证专题

1、软件学报安全攸关软件系统建模与验证专题文章整体分类1基于形式化方法的航空电子系统检测 方法：模型检测 质量：一致性系统结构设计的资源是否满足需求中性能指标的配置要求，即：系统结构对应的资源能否满足配置（静态检测）；可用性系统的执行环境是否能保证系统任务的正常执行（动态检测）。 模型：系统结构、资源、任务的形式化建模 检测标准：一致性a.配置文件一致性：软件配置项是否满足需求（不同级别配置文件是否一致）；b.系统环境状态适配性（环境即资源，当前状态能否满足性能指标）。可用性生成的“检测用例”。 实例：航空电子系统仿真平台基于形式化方法的航空电子系统检测航空电子系统静态建模1. API：输入/输出

2、+约束；2. 性能指标PI：资源属性名+数量；3. 配置文件CONF：文件属性+属性值；4. 软件配置项CSCI：1+2+3；5. 分系统SS：1+2+3+4；6. 航空电子系统ES：1+2+3+5.功能建模组件关系建模基于形式化方法的航空电子系统检测 动态建模：窗口树、任务执行过程状态图基于形式化方法的航空电子系统检测 检测过程2基于时间抽象状态机的AADL模型验证 方法：模型检测 实际工作：AADL（系统体系结构设计与分析语言）TASM（时间抽象状态机） 质量：依赖于TASM Toolset和UPPAAL 模型：AADL图形化模型 检测标准：任务的参数描述（表格） 实例：导航、制导与控制系

3、统GNC的AOCS子系统（控制计算机/姿势与轨道控制系统） 工具：AADL2TASM基于时间抽象状态机的AADL模型验证 思路：1.分别对AADL和TASM语法进行抽象，然后给出映射关系，并基于ML的元语言形式定义2者的转换语义规则；2.系统AADL建模AADL2TASMTASM ToolSet分析完整性、一致性、时间行为和资源行为仿真UPPAAL检测死锁、安全性、活性、实时性。3基于时间STM的软件形式化建模与验证方法 方法：模型检测 质量：可信性（时间和逻辑属性） 模型：TSTM给STM加了时间和语义约束（STM状态迁移矩阵，一种基于表结构的状态机建模方法，前端为表格形式，后端是严格的形式

4、化定义） 检测标准：用时序逻辑语言TCLT定义的所需满足的性质。 实例：列车控制系统3基于时间STM的软件形式化建模与验证方法 本文方法：1.软件TSTM建模，刻画软件的行为特征；2.属性的TCTL描述3.检测方法：基于界限模型检测（BMC）技术的时间计算树逻辑（TCTL）模型检测方法模型和待验证属性的否定形式进行合取，构建BMC公式，BMC公式的求解问题归约为逻辑公式的可满足性判定，即：SAT/SMT实例。4设备驱动程序可靠性和正确性保障方法与技术研究进展 综述性论文 质量：驱动程序的可靠性和正确性。 程序故障隔离与恢复、正确性分析和验证、设计建模与复杂性控制。5基于数据链的软件故障定位方法

5、 方法：代码分析 质量：程序的数据流相关的逻辑故障定位（程序设计逻辑故障，定位到方法内的代码） 模型：数据链每个变量上的定义操作状态轨迹及其之间的依赖关系。 分析对象：程序代码 检测方法：1.先用现有方法将逻辑故障定位到方法；2.再用本文方法中方法内定为变量故障疑似度分析：a.对故障疑似方法建立数据链；b.用a的数据链构建概率数据链模型。c.疑似度排序 实验对比6一种面向列车控制系统中安全攸关场景的测试用例自动生成方法 本文工作：扩展了活动图，加入了a.事件驱动机制；b.时间约束. 覆盖准则：a.循环只执行一次；b.不同的并发分支并发执行（同时向前执行一步）；c.所有简单路径被覆盖（从a、b两

6、条准则得到的活动图执行路径）。 本文测试用例生成方法：1.扩展活动图建模，并找出其中的简单路径；2.明确被测系统的边界；3.执行简单路径，并沿路收集外部环境向被测系统发送的事件，作为测试输入，被测系统向外部环境的输出作为结果序列。4.测试用例=环境传给被测系统的信息（特定时间）+被测系统的观察结果+时间上需满足的约束。 实例：地铁列车控制系统7多处理器实时系统可调度分析的UPPAAL模型 方法:模型检测 （偏硬件，主要数UPPAAL的使用） 质量：可调度性系统必须满足的时间要求。 模型：UPPAAL模型 性质：时间自动机建模可调度性相关的模块（实时任务、运行平台、调度管理） 检测：UPPAAL

7、检测 实验：对象智能手机GSM系统的21个任务 本文贡献：给出了多处理器实时系统可调度分析的模板8多分支单变量循环程序的终止性分析 方法：代码分析 质量：带多个分支的单变量循环程序的终止性问题（系统中有无死循环，是正确性的基础）（可信计算） 主要结果： 称由迭代函数 F 和循环条件形成的区域 I 所构成的循环程序 P(F,I)在实数域是不可终止的,如果存在一点 x0,使得 ( ) F x I i 0 0 i+ = .这里,Fi=FDFDDF 表示函数的复合.如果那样的 x0 不存在,则称循环P(F,I)在实数域上可终止. 定理 1. 令 f :R6R 为一维连续映射.I 为一闭区间.循环程序P

8、1 While xI dox:=f(x)是不可终止的充分必要条件为迭代映射是不可终止的充分必要条件为迭代映射 f 在闭区间在闭区间 I 上有不动点上有不动点. 实例实例 应用应用： 对多分支单变量多项式循环程序，可通过实代数工具验证定理中条件是否成立；对多分支单变量多项式循环程序，可通过实代数工具验证定理中条件是否成立； 判定不动点是否落入到循环条件形成的区域问题，可转为半代数系统，通过实代数工具求解。判定不动点是否落入到循环条件形成的区域问题，可转为半代数系统，通过实代数工具求解。9面向安全攸关系统中小概率事件的统计模型检测 方法：基于机器学习的统计模型检测算法统计模型检测SMC评估系统模型

9、满足属性约束的概率区间机器学习（用于生成更多样本） 质量：可靠性（在相对较少的样本数量下，预测、评估小概率事件的发生概率） 本文框架：输入：a.目标系统的可执行模型（随机混成自动机模型SHA）；b.属性约束的概率有界线性时态逻辑（PBLTL公式）；c.统计精度参数。输出：在有限的资源约束下，系统模型a满足属性约束b的概率区间。2个模块：学习型模型检测器+自适应统计分析器 实例：基于通信的列车控制系统学习型模型检测器学习型模型检测器输入：系统模型a+有界线性时态逻辑公式输出：用经典模型检测算法判断单个样本trace是否满足属性约束，得到统计分析样本Trace分割与特征提取分割与特征提取目的：找到

10、一个合适的时间点,使其前段 Trace 在尽可能短的条件下最大程度地包含对预测有用的信息,以便 SVM 预测后段 Trace 的信息.思想：条件概率。假设在 A 事件发生的情况下,B 事件更有可能发生,如果 P(A)P(B),则先在模拟Trace 的过程中找到 A 事件的发生点,在此前提下向后进行多次模拟,以提高捕获到 B 事件的可能性.基于属性约束和随机行为的特征提取方法：1.确定需要提取的特征变量;2.根据特征变量提取训练集中 Trace 的具体特征.SVM:机器学习模型，用于预测生成新的样本。如果样本可信，则使用预测结果，并开始下一次模拟；不可信，则进入后段仿真器，模拟出完整的Trace

11、，检测其结果。自适应统计分析器自适应统计分析器将的结果作为统计分析样本，执行统计模型检测，判定现有样本是否满足精度要求，满足这结束，否则返回生成更多样本trace.SPRT顺序概率比检验；BHT贝叶斯假设检验；BIET贝叶斯区间估计检验。10面向航天嵌入式软件的形式化建模方法 研究对象：周期性控制系统的需求获取、表示、分析验证 方法：模型检测（分析所建的需求模型） 本文思路：1.航天需求描述语言SPARDL形式化建模方法用一系列模式来体现嵌入式控制系统的行为特征，每个模式可以周期性地执行一系列过程。核心是模式图，描述模式和模式间的变迁。2.时序性表示给出了ITL（基于区间逻辑的性质规范语言）性

12、质模板。3.从SPARDL自动生成C代码（给了原理），并快速仿真。 实例：某深空探测信号软件，用于钻探取土（没有给出任何数据）个人：SPARDL数用于描述需求的2层语言，上层是模式图，下层是对应的形式化描述。概率模型检测概率模型检测概率模型检查把性质 p 在模型的一次执行(一条路径)上是否成立视为一个服从两项分布的随机变量.概率模型检查主要考虑以下两个问题:给定模型 M 和性质 p,1) 估算在模型 M 的任意一条路径 t 上,p 成立的可能性,即参数估计;2) 判断上述可能性是否大于给定的阈值,即假设检验.11同步数据流语言高价运算消去的可信翻译两种语言差距较大：Luster*有时钟同步、数

13、据流、并发及数据流对象，其变量和表达式都表示一个流数据（给定类型的值序列+一个时钟）；Clight有顺序控制流特征。高阶运算：一个对数组或输入参数列表进行循环计算的过程。12一种基于特征矩阵的软件脆弱性代码克隆检测方法 方法：代码检测 质量：脆弱性（如缓冲区溢出、内存多次释放、指针误用等） 本文思想：建立一个已发现的脆弱性代码数据库,从代码的相似度层面进行检测,查找某个软件系统出现的脆弱性代码在其他软件中的分布情况,就可以检测出更多的脆弱点.提出多类脆弱性检测模型模型CVdetector 实验数据对比10 维向量(stmtexp,decl,incr,cond,assign,mul,add,fun_call,fname,fpara)13一个及其检测的Micro-Dalvik虚拟机模型 形式化虚拟机模型，对指令集和运行时状态进行了形式化，然后推理证明该虚拟机的正确性。14信息物理融合系统控制软件的统计模型检验 方法：模型检测 质量：系统功能的正确性 本文内容：基于时间自动机，模块化描述实时多任务系统，然后提出一种利用统计模型检验技术，分析系统功能正确性。 模型：调度器、周期性任务、偶发任务、的时间自动机模型。 检测标准：人工分析出的错误条