近日，美国白宫国家网络主任办公室（ONCD）发布一份题为《回到基础构件：通往安全软件之路》的报告。呼吁开发人员积极使用“内存安全的编程语言”，例如Rust、Python、Swift、C#、Java和Go等，同时强调了形式化方法在软硬件安全领域的重要性，提出形式化方法应当应用于软硬件开发的全过程。形式化方法作为一种严谨、精确的验证技术，将成为全球的发展趋势，其在未来软硬件安全发展中将占据核心地位。

报告地址：https://www.whitehouse.gov/wp-content/uploads/2024/02/Final-ONCD-Technical-Report.pdf

这是继美国国家安全局、网络安全和基础设施局（CISA）等之后，又一政府机构发起呼吁，而且这一次直接与“保护国家安全”挂钩。根据报告指出，该建议是美国总统拜登网络安全战略的一部分，是“确保网络空间基石安全”的举措。

在21世纪的今天，网络安全与信息技术发展已经成为全球关注的核心议题。早在数年前，美国政府就已经敏锐地意识到5G网络部署对国家安全的重要性，并将其列为首要任务。随着技术的快速迭代，软件定义一切的时代背景下，软硬件系统的复杂性和安全性需求呈现指数级增长，这催生了对更高级别的验证手段的需求，而形式化方法正是这种需求下的必然产物。

白宫ONCD发布这份报告意味着，从国家战略层面，美国正积极推动形式化方法在软硬件安全领域的普及与深化应用，欲使其成为一种强有力的工具，从而帮助软件开发人员避免多种软件漏洞。随着世界步入数字化进程的深水区，形式化方法作为确保网络空间安全的重要基石，其在软硬件开发及维护过程中的应用将更为普遍和深入。美国白宫的政策文件不仅凸显了这一趋势，也将有力推动全球范围内对形式化方法的重视与投入，共同构筑起面向未来的安全防线。

望安科技在此领域的规划与ONCD的建议不谋而合，望安科技长期以来一直专注于形式化验证的研究与实践，不仅成功实施了多项高安全等级认证项目，而且自主研发的产品和服务也在国内获得了广泛认可。美国发布的国家政策，进一步印证了望安科技在形式化验证领域的发展目标和路径是完全正确的。

但是，尽管如此，相较于美国等发达国家在该领域的高度重视，我国政府和产业界在形式化方面的投入和关注度仍有较大的提升空间。在此背景下，望安科技将继续秉承创新精神，加强与国内外同行的合作与交流，努力推进形式化验证技术在中国市场的普及与应用，助力国家在软硬件安全保障方面实现提升和跨越，共同构建更加安全、可靠的全球信息技术生态体系。