论文部分内容阅读
随着软件在信息系统中发挥日益重要的作用,人们对软件可靠性和安全性等可信性质的要求也愈来愈高。为此,近年来国内外纷纷有针对性地提出了可信软件与可信环境构建的相关研究计划。如美国的《国家软件发展战略(2006--2015)》将开发高可信软件放在首位,美国自然科学基金会在加州大学伯克利分校建立了科学与技术研究中心TRUST,其目标是为设计、构建和运行可信信息系统建立新的科学与技术基础。同时,我国也于2007年启动了“可信软件基础研究”重大研究计划,该计划从可信软件的设计、开发、应用等问题出发展开理论研究,目前已经支持了数十项课题,并取得了丰硕的研究成果。但是迄今为止,软件设计和开发主要依赖于开发人员的知识和经验,自动化程度不高。由于软件设计及开发人员难免犯错误,导致软件本身在设计和开发时可能有很多潜在的安全问题,在软件被使用时,这些安全问题可能成为可供攻击者入侵或破坏软件运行的安全漏洞。因此,软件安全性分析和测试是保证和提高软件安全性的关键和必不可少的手段。与此同时,尽管有些软件安全性功能测试对软件安全性有直接影响,但软件安全性功能测试与软件非功能性安全指标(例如隐私性、完整性和容错性等)之间的定性定量关系并不清楚。因此,根据软件功能安全性分析和测试结果建立一个综合性软件安全评价模型就是一个亟待解决的科学问题。因故,本文围绕可信软件安全性测评的基础理论问题,借助形式化与概率统计数学等理论,重点研究软件系统的隐蔽信道搜索、并发进程间的隐私性分析和基于功能性测试结果获取非功能性安全属性等可信软件安全性评估理论及技术研究。本研究所采用的思想和方法强调对软件的安全性进行分析和评估,在其理论方法上具有创新性,对进一步深化软件安全性测评理论具有重要的理论意义与实践价值。具体内容包括:(1)针对现有DIFC系统的由于不合理的标签机制导致的隐蔽信道问题:在隐蔽信道的识别和分析方面,基于有向图联通理论,提出了一种针对DIFC系统的隐蔽信道检测模型;并基于回溯算法的思想,提出两个隐蔽信道检测算法。在隐蔽信道的限制和消除方面,通过对现有的标签机制加入的互斥机制,可以有效解决现有DIFC系统的隐蔽信道问题。(2)针对并发程序进程间的隐私性分析问题,以Hoare逻辑理论和经典无干扰理论为基础,提出一种并发进程间无干扰分析模型,将并发程序抽象为逻辑独立的进程单元,在进程单元正确性的基础上对进程间的干扰性进行分析。方面把并发程序功能正确性证明分化为对程序中所有并发进程的形式化验证,以达到复杂程序简单化证明的目的;另一方面根据并发程序的特点,在进程的功能正确性验证的基础上进行并发进程间的无干扰性分析。(3)针对软件安全性功能测试与软件非功能性安全指标(例如隐私性、完整性和容错性等)之间的定性定量关系困难,首先通过软件安全性原始测试数据矩阵模型对测试数据进行标准化处理:其次通过软件测试结果样品差异判断模型来保证原始数据矩阵的完备性;最后以主成分分析理论为基础,计算分析得出被测软件的多种功能性测试方法和技术结果数据可以使用少数几个非功能性综合安全指标来解释软件的安全性,并能够对这些测试技术和方法在这些指标中的贡献值来分析其在整个测试过程中的重要性,从而为下次测试过程中的资源分配提供指导,并能提供该软件安全性指标的一些量化数据给安全性评估模型。(4)针对软件安全性测评的问题。结合(1)、(2)和(3)的结果,以多属性效用理论为基础,提出了一种可信软件的安全性评测模型,能够让软件运行环境对软件安全性的影响加入到软件是否安全当中;同时,该模型可以为软件安全性测评提供一个量化的安全性指标,通过比较两次安全性分析和测试间的量化安全性指标,能够反映软件的安全性变化。