可信软件构造理论与方法研究

由于软件的运行环境越来越开放，规模不断增大，行为日益复杂，使得软件的可信性面临着严峻的挑战，如何构造可信软件受到了工业界和学术界越来越多的重视和关注。近年来，国内外对可信软件展开了广泛研究，但可信软件的构造仍然缺乏一套系统的成熟的理论和方法。本项目拟采用理论研究和实证研究相结合的方法，研究可信软件的系统化开发理论、方法与技术，设计并实现可信软件开发工具和运行支撑平台及环境。主要研究内容包括：1、可信软件开发过程模型，重点研究开发过程中的可信保障机制；2、面向可信软件的需求建模及基于行为的需求模型验证方法；3、可信软件体系结构设计、构件化实现及基于可信编译的程序代码生成方法；4、可信软件的测试与评估方法；5、可信软件开发工具的设计与实现以及开发平台的集成方案；6、面向国产家电嵌入式可信软件典型示范应用。

由于软件的运行环境越来越开放，规模不断增大，行为日益复杂，使得软件的可信性面临着严峻的挑战，如何构造可信软件受到了工业界和学术界越来越多的重视和关注。近年来，国内外对可信软件展开了广泛研究，但可信软件的构造仍然缺乏一套系统、成熟理论和方法。本项目采用理论研究和实证研究相结合的方法，研究可信软件的系统化开发理论、方法与技术，设计并实现可信软件开发工具和支撑平台。主要研究成果如下：.1、提出了一个基于可信链的可信软件开发过程模型，并提出了一整套可信软件构造方法和技术，研发了相应的开发工具，形成了较为完整的可信软件开发技术体系和应用平台。.2、在需求建模与验证阶段，提出了一种基于多视点和软件行为的需求建模方法和需求模型的检测方法，从而获得可信的需求模型。.3、在设计阶段，提出了一种体系结构多维可信关注点模型和一种高可信体系结构描述语言(DADL)，实现了从需求到设计模型的平滑过渡和精确跟踪，并提出了一个异常处理与验证框架。.4、在实现阶段，提出了三次编译，两次对比的编译器验证方法。该方法结合编译后代码可信性加强技术，保障了可信目标代码的生成。基于该技术自主研发的HRCC可信编译器得到大规模商业应用，并提出了不同体系结构下低能耗和耗损均衡的编译优化方法，降低缓存动态能耗达38%。.5、在测试与评估阶段，构建了一个面向云环境的系统行为采集与保护实验平台，其核心技术被华为有限公司采用；设计和实现了一个基于漏洞库的可信性评估工具。 .本项目获授权发明专利5项, 软件著作权5项，出版专著2部，发表SCI论文11篇，EI论文34篇。以陈国良和周巢尘两院士为正副组长的鉴定委员会认为该成果创新特色明显，整体达国际先进水平。本项目成果获得2014年湖北省科技进步一等奖。