科技日报记者 张强
连日来，“时代楷模”、国防科技大学计算机学院研究员王戟的先进事迹在社会各界引发热烈反响。很多人由此认识了这位坐在轮椅上的科研工作者。
作为国内高可信软件技术领域的主要开拓者，王戟早在2003年便发表了我国在该领域最早的系统性论文《高可信软件工程技术》，为该方向的研究奠定了重要基石。
备受公众关注的高可信软件是什么？王戟解释：“软件信息系统也会‘生病’，高可信软件的重要作用就是给它们‘看病’。”
国防科技大学计算机学院教授文艳军介绍，高可信软件是通过程序分析和验证技术确保极高可靠安全性与保密安全性的软件，其核心特征是通过形式化方法替代传统测试手段，为国家安全、军用装备等相关领域提供严格保障。
文艳军解释，高可信软件追求的“可信”，主要包括功能正确、性能达标、安全、可靠等核心要求。主要包含两层含义：一是可靠安全性，确保软件运行时具备设计要求的功能，避免引发危险或灾难；二是保密安全性，保障数据与信息的保密性、完整性、可用性及真实性。
那么，高可信软件是如何保证软件“极低缺陷率”的？
国防科技大学计算机学院教授陈立前说，高可信软件可以像“做CT”一样给那些关键软件系统进行全面扫描、精准诊断，找出深层次隐藏的漏洞和隐患。
确保软件“零缺陷”或“极低缺陷率”，形式化方法起到了关键作用。陈立前介绍，形式化方法是一种基于数学和逻辑的技术，用于精确描述、开发和验证计算机软硬件系统的行为和性质，旨在用数学符号来研究软件的正确性，以提高其可靠性和安全性。简而言之，它就是用数学的方法保证软件的可靠性。
王戟长期深耕模型检测、抽象解释、符号执行和定理证明等形式验证技术，以数学化的严格推演为软件“零缺陷”筑牢根基。
高可信软件主要应用于对安全性要求极为严苛的安全攸关系统，覆盖高速列车、航空航天、核反应堆控制等国计民生领域，以及医疗设备、关键军事信息与控制系统等领域。
“这些系统中的任何一处错误，都可能酿成灾难性后果——轻则造成重大财产损失，重则危及生命安全，或导致军事机密泄露。高可信软件的价值，正在于从源头阻断此类风险。”陈立前介绍，高可信软件可通过两种方式实现更高安全保障。一是程序分析，静态扫描源代码以发现潜在缺陷，强化编程规约；二是程序验证，使用数学演绎证明代码严格符合需求规约，例如嵌入式操作系统验证、算法形式化验证等。
“近年来，高可信软件的应用边界正在向AI安全治理新领域拓展，例如用于自动驾驶、机器人等的可信保障。”文艳军说。
网友评论
