安全关键系统支撑及验证技术

作者: 时间:2017-06-27 点击数:

安全关键系统广泛应用于航空、航天、轨道交通、工业控制等国民经济重要领域,它对安全性具有极高的要求,例如A级安全级别航空机载软件要求出错的概率小于10-9。安全关键系统趋向于网络化、综合化和大规模,它必须综合考虑功能安全、信息安全和确定性等系统性质。国际上安全关键系统出现的安全事故层出不穷,包括航天飞行器坠毁、失联,空天网络中传输被窃听,卫星被跟踪等。针对上述挑战,实验室围绕安全关键系统的开发、认证和运行,采用数理化方法、形式化验证和高安全认证为手段,从网络传输层、核心系统层和应用系统层开展研究,分别突破了高速高强度空天传输加解密、基础软硬件的形式化验证和大规模应用系统的自动化测试等核心技术,取得了一系列原创性成果,具体如下:

1.空天信息安全传输支撑系统

空天信息交互的数据处理模式特殊,数据传输距离长,空间干扰环境复杂,天基平台资源紧缺,对空天信息安全传输提出高速、低耗、高安全等严苛的技术能力需求。长期以来,这成为空天信息安全能力提升的主要障碍。围绕这一问题,研究团队从原理方面引入动力学,并在理论、技术、工程层面开展创新研究,突破了系列空天信息安全瓶颈。

在原理方面,提出迭代型密码是一类动力学算子的学术观点,引入动力学方法研究代数密码。为此,将密码设计评测过程扭扩为一类代数与动力学融合的密码算子的稳定性问题,使得系统的稳定性与其统计分析方法与密码设计和安全评测过程密切关联,建立攻击模式下动力学密码稳态设计和安全评测体系,达到迭代状况可判断、迭代效果可调控,并最终实现理想密码。

在理论方面,建立了融合代数和动力学的密码评测和设计方法。着力解决离散和连续相关问题的转化、密码算子迭代的稳定性和效果以及从动态角度建立相应高安全性判据等核心问题。通过研究密码算子机器迭代过程与强混淆和快扩散之间的数学关系,建立了分组密码的均匀遍历分析方法、密码强度的熵度量理论和强密判据并完成了相关系列设计技术,显著提升密码的安全强度。成果通过国家密码权威机构测评:现有计算条件下无有效攻击方法。安全强度较国际公开密码算法标准指数级提升,并完成入库。

在技术和系统研制方面,面向空天信息安全需求,解决了高安全向高速低耗实现中的复杂度转化问题。在已经达到高密码强度的基础上,运用已得到的分析方法和度量判别条件,对密码系统整体进行冗余分析,并实现了高效加解密并行技术,在低资源条件下,显著提升数传速率。同时,利用簇分析原理,对强密高速密码算子的参数进行分簇研究,建立了异构多模式设定技术,可提供上百种高安全和信息共享兼顾的异构加密模式,基本解决了空天数传关键技术问题。将基于新原理的理论和技术落实到国家急需的核心军事装备中。目前,该安全技术已被列入我国航天某发展规划,研制完成了高速宇航级加密器和综合解密一体机等国家急需的安全装备,相关成果及装备已在多个重点型号11 颗高性能卫星中列装,目前还有多个重点型号的高性能卫星处于应用论证阶段。各卫星型号的总体、可见光、SAR、数传生产及地面研制单位等,对成果的速度、安全、图像品质、资源和可靠性等进行了应用评价,认为 “创新性地将现代数学的典型成果实质性应用于构建新密码体系”,“灵活低耗,性能稳定,大幅降低了宇航级资源消耗”,“首次实现空天数据高速传输和高安全的统一”等。该技术在网络空间安全的民用领域亦有重要推广价值。实验室作为以上成果的第一完成人单位获国家技术发明奖一等奖和国防技术发明一等奖

2.航空航天安全关键系统自动化测试技术

航空航天安全关键系统可信需求典型而迫切,其可信性评估具有测试依赖性,由于航空航天安全关键系统的高度复杂性,人工测试实际不可行,其结果不可靠,因此,安全关键系统测试和检测自动化是发展趋势。

在自动化测试理论模型研究方面,为建立通用测试语言及系统的理论基础,提出航天器自动化测试理论模型,从原理上证明该模型可计算,即航天器测试过程可自动化。基于自动化测试理论模型,提出通用航天器测试语言,该语言独立于测试设备、测试数据、被测航天器及其基本测试方法。支持测试用例、测试方法、测试过程等的统一描述,形成航天器自动化测试的形式体系和测试过程工作规范。

2012年12月北航与五院航天器自动化测试技术联合实验室正式成立。自动化测试应用于北斗导航系列3种类型12颗卫星测试。自动化检测系统填补了国内大型信息化武器装备系统软件检测的空白,已交付部队16套使用,直接经济效益达1938万元。自动化检测系统已应用于两大军种(空军、海军),覆盖现役预警机全部型号(KJ200KJ2000H200),保障了包括上海世博会、广州亚运会等重大场合的安保及部队多次重大演习和作战训练任务的圆满完成。实验室作为以上成果的第一完成人单位获国防科技进步二等奖和北京市科学技术三等奖。

3.安全关键操作系统形式验证技术

现代安全攸关系统大多采用计算机系统进行信息采集、处理和控制,而操作系统(OS)内核是计算机系统的核心软件,处于系统软件栈的最底层,内核出现的微小错误都可能产生系统失效,从而导致整个计算机系统的崩溃。同时,内核功能结构复杂,尤其是多核内核并发度高,开发与调试都十分困难,一些隐藏的错误用通常的软件测试技术很难发现,而形式化方法可帮助软件开发人员发现其他方法不易发现的错误。因此,近年来采用形式验证技术提高操作系统内核的安全性成为学术界和工业界共同关注的热点之一。

实验室以遵循ARINC 653工业标准的OS内核为研究对象,开展符合Common Criteria认证要求的形式规约以及信息流安全验证技术研究,突破内核信息流安全表征、OS内核形式规约及安全性质的组合验证、安全保持的OS内核规约求精等关键技术,并构造符合CC EAL7的ARINC 653内核形式规约。

首先,对ARINC 653标准进行了完整的形式化建模,模型覆盖了标准定义的所有系统功能和57个系统接口,是公开资料中最完整的ARINC 653模型。其次,根据ARINC 653标准以及隔离内核的领域知识定义了90多条安全不变式,完成了1600多个定理的证明。通过形式验证发现了ARINC 653 P1-3标准的6个safety问题,这些问题被ARINC 653标准委员会认可,并将在新版本中进行修复。实验室成员受ARINC653标准委员会邀请,成为标准委员会委员,成为国内首个委员。

其次,对符合ARINC 653的OS内核进行了研究,在Isabelle/HOL定理证明器开发了其信息流安全模型、单核内核规约求精框架,并按照ARINC 653 P1-3标准开发了多个层次的形式规约。以形式规约为依据,对XtratuM、POK开源代码和VxWorks 653代码进行了确认。整个验证过程中,发现了ARINC 653 P1-3标准的5个security问题和上述内核代码中的8个security问题。为了研究多核OS内核的组合验证方法,对依赖-确保组合推理技术开展了研究。对seL4项目实现规约使用的Simpl规约语言进行了扩展,增加了并发特性的语句,形成CSimpl语言。在Isabelle/HOL中定义了CSimpl的依赖-确保组合推理规则,并证明了其可靠性,并以ARINC 653 P1-4多核标准的分区间采样通信为案例,进行了组合验证。

实验室与中航工业631联合承担工信部**科研项目“多核机载操作系统调试及验证技术”,对631所天脉II操作系统的需求进行了形式建模与分析工作,并发现了需求文档的10多个不一致性问题。实验室与北京神舟航天软件技术有限公司开展了神舟OS形式化验证方法、安全关键模型驱动软件开发工具的合作研究,相关成果得到了载人航天工程的认可,并获得2016年载人航天工程主办的软件工程新技术交流会优秀论文一等奖。

软件开发环境国家重点实验室 地址:北京市海淀区学院路37号北京航空航天大学新主楼G座
邮编:100191 联系电话:010-82338092 邮箱:nlsde@nlsde.buaa.edu.cn