发明名称 一种基于图尔敏模式的软件安全性论证方法
摘要 本发明公开了一种基于图尔敏模式的软件安全性认证方法。该方法以需要认证的软件安全性目标为核心,提供支持目标成立的事实证据,质疑时,给出赋予事实证据支持目标成立的正当理由及用于强化正当理由权威性陈述的支援;如目标不是完全成立,则需明确目标实现程度的限定词;给出阻止从正当理由得出目标成立的反驳,从而实现以软件安全性目标为核心的安全性认证方法。本发明是一种更自由更宽泛的软件安全性论证方法,能更直接更清晰地表明软件安全性目标是如何满足的,同时能更有效地促进开发方开展安全性保障工作的积极性,从而更主动地提高了软件安全性。
申请公布号 CN102779253A 申请公布日期 2012.11.14
申请号 CN201210232486.2 申请日期 2012.07.05
申请人 北京航空航天大学 发明人 曾福萍;张大健;王栓奇;陆民燕
分类号 G06F21/00(2006.01)I 主分类号 G06F21/00(2006.01)I
代理机构 代理人
主权项 一种基于图尔敏模式的软件安全性论证方法,其特征在于包含以下步骤:(1)提出软件安全性论证目标(Claim),即试图在软件安全性论证中证明为已经满足的结论,并进一步明确软件安全性目标的辅助信息(Auxiliary Info)。(2)提供支持软件安全性论证目标的事实证据(Data),并进一步明确事实证据的辅助信息。事实证据一般为与软件安全性工程相关的一些活动的记录或产生的数据,如安全性分析结果、测试数据等。如果受到质疑,则转入步骤3,否则转入步骤5。(3)给出赋予该‘事实证据’具有导出‘软件安全性论证目标’结论的资格的推论规则,即“正当理由(Warrants)”,并进一步明确正当理由的辅助信息。如果受到质疑,则转入步骤4,否则转入步骤5。(4)明确正当理由背后起保证作用的支援(Backing),用于强化正当理由权威性的支援性陈述。(5)给出“软件安全性目标”实现程度的限定词(Qualifier)。(6)如果存在,给出阻止从正当理由得出目标成立、具有保留机能的陈述的例外情况或反驳(Rebuttal)。
地址 100191 北京市海淀区学院路37号