夜雨聆风
◎ 科技日报记者 张强
连日来，“时代楷模”、国防科技大学计算机学院研究员王戟的先进事迹经媒体广泛报道后，在社会各界引发热烈反响。很多人由此认识了这位坐在轮椅上的科研工作者。
作为国内高可信软件技术领域的主要开拓者，王戟早在2003年便发表了我国在该领域最早的系统性论文《高可信软件工程技术》，为该方向的研究奠定了重要基石。
王戟近照。孔祥库 摄
什么是高可信软件？它是如何保证软件“极低缺陷率”的？其重要性和战略意义又体现在哪里？
第一问：什么是高可信软件？
对于高可信软件，王戟这样解释：“软件信息系统也会‘生病’，高可信软件的重要作用就是给它们‘看病’。”
国防科技大学计算机学院教授文艳军介绍，高可信软件是通过程序分析和验证技术确保极高可靠安全性与保密安全性的软件，其核心特征是通过形式化方法替代传统测试手段，为国家安全、军用装备等相关领域提供严格保障。
“用通俗的语言概括，高可信软件就是用来‘诊断’别人的软件，是给软件‘看病’‘挑错’的软件。它是‘软件医生’。”文艳军说。
文艳军表示，高可信软件追求的“可信”，主要包括功能正确、性能达标、安全、可靠等核心要求。主要包含两层含义：一是可靠安全性，确保软件运行时具备设计要求的功能，避免引发危险或灾难；二是保密安全性，保障数据与信息的保密性、完整性、可用性及真实性。
“高可信软件还包括质量特别好、可以高度信任的软件。普通用户日常使用的软件一般不是高可信软件，但用户经常用的银行APP这类软件一般有严格质量保证，也可被算作高可信软件。”文艳军说。
第二问：高可信软件是如何保证软件“极低缺陷率”的？
“高可信软件不等同于‘没有Bug的软件’。有的高可信软件可能有Bug，但Bug极少，能被应用场景允许和接受。”国防科技大学计算机学院教授陈立前说，有没有Bug不是高可信软件本身所关注的，它主要是可以像“做CT”一样给那些关键软件系统进行全身扫描、精准诊断，找出深层次隐藏的漏洞和隐患。
要确保软件“零缺陷”或“极低缺陷率”，形式化方法就起到了关键作用。
图片来源：视觉中国
王戟长期深耕模型检测、抽象解释、符号执行和定理证明等形式验证技术，以数学化的严格推演为软件“零缺陷”筑牢根基。2015年，王戟力主推动中国计算机学会成立形式化方法专委会。2019年，王戟被推举为形式化方法专委会主任。
陈立前介绍，所谓形式化方法，是一种基于数学和逻辑的技术，用于精确描述、开发和验证计算机软硬件系统的行为和性质，旨在用数学符号来研究软件的正确性，以提高其可靠性和安全性。简而言之，它就是用数学的方法保证软件的可靠性。
第三问：高可信软件的重要性和战略意义体现在哪里？
“程序员在设计软件的时候，都希望软件的功能和性能和我们所预期的一样。这就是高可信软件技术存在的意义。”王戟说。
因此，高可信软件主要应用于对安全性要求极为严苛的安全攸关系统，覆盖高速列车、航空航天、核反应堆控制等国计民生领域，以及医疗设备、关键军事信息与控制系统等国防安全核心领域。
“这些系统中的任何一处错误，都可能酿成灾难性后果——轻则造成重大财产损失，重则危及生命安全，或导致军事机密泄露。高可信软件的价值，正在于从源头阻断此类风险。”陈立前介绍，高可信软件可通过两种方式实现更高安全保障。一是程序分析，静态扫描源代码以发现潜在缺陷，强化编程规约；二是程序验证，使用数学演绎证明代码严格符合需求规约，例如嵌入式操作系统验证、算法形式化验证等。
“近年来，高可信软件的应用边界正在向AI安全治理新领域拓展，例如用于自动驾驶、机器人等的可信保障。”文艳军说。
专业视角为你解读更多新闻热点
戳下图↓↓↓
编辑：郭炘蔚
