构件化嵌入式软件安全性分析方法研究

《构件化嵌入式软件安全性分析方法研究》由会员上传分享，免费在线阅读，更多相关内容在学术论文-天天文库。

1、中图分类号：TP311论文编号：102871614-B004学科分类号：081203博士学位论文构件化嵌入式软件安全性分析方法研究研究生姓名徐丙凤学科、专业计算机应用技术研究方向软件工程指导教师黄志球教授南京航空航天大学研究生院计算机科学与技术学院二О一四年三月万方数据万方数据NanjingUniversityofAeronauticsandAstronauticsTheGraduateSchoolCollegeofComputerScienceandTechnologyResearchonComponent-base

2、dEmbeddedSoftwareSafetyAnalysisMethodsAThesisinComputerScienceandTechnologyEngineeringbyXuBing-fengAdvisedbyProf.HuangZhi-qiuSubmittedinPartialFulfillmentoftheRequirementsfortheDegreeofDoctorofPhilosophyMarch,2014万方数据万方数据承诺书本人声明所呈交的博/硕士学位论文是本人在导师指导下进行的研究工作及取得的研究

3、成果。除了文中特别加以标注和致谢的地方外，论文中不包含其他人已经发表或撰写过的研究成果，也不包含为获得南京航空航天大学或其他教育机构的学位或证书而使用过的材料。本人授权南京航空航天大学可以将学位论文的全部或部分内容编入有关数据库进行检索，可以采用影印、缩印或扫描等复制手段保存、汇编学位论文。（保密的学位论文在解密后适用本承诺书）作者签名：日期：万方数据南京航空航天大学博士学位论文摘要随着嵌入式软件系统在汽车、核工业、航空等安全关键领域的广泛应用，其失效将会导致财产的损失、环境的破坏甚至人员的伤亡，使得保障软件安全性成为

4、系统开发过程中的重要部分。此外，嵌入式软件系统规模和复杂度的增加使其多采用构件化分布式架构。因此，针对构件化嵌入式软件系统进行安全性分析已成为现代嵌入式系统安全性保障的重要方法和研究热点。而传统的安全性分析方法主要应用在软件的需求分析阶段，在软件设计阶段仍缺乏有效的安全性分析方法和工具。形式化方法是一种基于严格的数学理论为软件和硬件系统提供精确规约、分析和验证的方法。对于具有高安全性需求的嵌入式系统，建立有效的形式化分析验证技术可以为安全性分析提供支持。因此，在嵌入式软件设计阶段的安全性建模中引入形式化方法对其进行分析

5、，得到软件安全性分析结果，可以有效提高嵌入式软件安全性。本文主要围绕构件化嵌入式软件系统设计阶段的安全性建模和分析问题展开研究。采用SysML和状态事件故障树建立安全性设计模型，对构件化嵌入式软件系统设计阶段模型的静态结构和动态失效行为两方面的安全性分析工作进行研究。主要工作包含以下几个方面：(1)针对构件化嵌入式软件静态结构的构件安全等级依赖问题，给出了分析构件之间安全等级依赖与安全认证目标之间一致性的方法。首先根据安全认证标准DO-178B分析软件构件安全等级依赖所必须达到的认证目标，其次采用SysML块定义图建立

6、带有安全等级信息的软件静态结构的安全性设计模型。由于SysML块定义图缺乏严格的形式语义，建立形式化模型块依赖图对SysML块定义图进行形式化语义描述。在此基础上给出算法用于分析构件安全等级依赖与认证目标之间的一致性。采用该方法对嵌入式软件系统静态结构的安全等级依赖关系进行分析，能够提高系统整体的安全性，并为安全认提供证据。(2)针对构件化嵌入式软件动态失效行为因果链中的最小割序集分析问题，采用状态事件故障树建立系统的失效行为因果链。由于状态事件故障树缺乏严格的形式语义，提出形式化模型卫式接口自动机对状态事件故障树行为

7、方面的形式化语义进行描述。在此基础上，给出卫式接口自动机的并行组合聚合框架用于生成状态事件故障树的形式化语义，并通过定义弱互模拟操作对组合过程中的状态空间进行约简。最后给出了基于该形式化语义的状态事件故障树最小割序集分析方法。分析结果可以为软件的测试用例生成以及模型检验提供支持。(3)针对构件化嵌入式系统动态失效行为的安全性参数分析问题，提出了软件失效行为的概率和时间特性分析方法。由于状态事件故障树能够同时描述构件化嵌入式系统的动态失效行为和概率特性，在状态事件故障树最小割序集分析的基础上，可进一步分析其概率时间参I万

8、方数据构件化嵌入式软件安全性分析方法研究数。为了描述状态事件故障树带概率信息的形式化语义，提出能够同时描述功能行为和概率信息的形式化模型接口交互马尔可夫链用于描述状态事件故障树的形式化语义。在此基础上，给出接口交互马尔可夫链的并行组合聚合框架用于获得状态事件故障树的形式语义，并通过定义接口交互马尔可夫链的弱互模拟操作对组合过程中的