日本国立研究开发法人信息通信研究机构（NICT）网络安全研究所提出了了支撑宇宙通信安全性的加密电路设计与验证一体化的新理论。这是一套兼顾提升宇宙辐射耐受性、减少元器件数量，将加密电路设计与验证融为一体的全新理论；即便电路因辐射防护等需求变得结构复杂，该理论也在全球首次对所有可输入值的正常动作提供了数学保证。
该成果有助于提升加密电路硬件设备的可靠性并降低成本，相关论文在NASA的国际会议NFM2025（NASA Formal Methods 2025）上荣获优秀奖（Honorable Mention）。
图1 支撑宇宙通信安全性的研究开发（供图：信息通信研究机构）
随着人造卫星被大量发射用于学术及商业用途，日本于2018年11月15日正式实施了《人造卫星发射及人造卫星管理相关法律》。
依据该法律制定的相关基准指南要求，在对人造卫星发射火箭型号认证及飞行许可时，针对重要系统的信号收发，必须采取加密等适当措施，防范通信遭受干扰与劫持攻击。
作为保障宇宙通信安全的核心技术，NICT一直在研发可防范航天器被劫持、保护传输数据的加密通信技术。
宇宙通信同时对高速化、大容量化提出需求，因此用硬件实现加密处理至关重要。然而，在硬件安装中，既要提升辐射耐受性以防止宇宙辐射引发误动作，又要在设计上想办法精简元器件数量以降低功耗与元件成本，致使电路结构日趋复杂。
与此同时，所设计的加密电路需保证对所有输入均正常运行，但如果追求高安全等级，输入组合可多达2 256（约10的77次方）种，逐一进行验证是不现实且不可能的。
网络安全研究所此次确立的加密电路设计与验证一体化的新理论，不再将电路设计与验证分离，而是将设计阶段的优化思路直接衔接应用于验证环节，将全部输入条件下的运行正确性作为数学属性进行形式化验证，从而能够从理论层面上保障电路运行。
通过应用该理论，全球首次在高安全等级前提下，使电路具备宇宙辐射耐受能力，相较于国际标准中广泛使用的构成，将电路规模缩减至约70%，并且实现了对所有2256种输入的动作保证。这种全覆盖动作保证的形式化验证，使用普通的计算机（单CPU内核）也可在约17小时内完成。
该成果有望应用于民营航天器通信服务、对地观测、灾害监测等社会基础设施服务领域，可在低功耗、低成本的设备上有效抑制误动作与网络劫持风险，为提升整体可靠性做出贡献。
原文：《科学新闻》
翻译：JST客观日本编辑部
【论文信息】
期刊：NASA Formal Methods (NFM 2025), Lecture Notes in Computer Science, Vol.15682, pp.236-253. Springer, 2025.
论文：Formal Verification of Composite Field Multipliers for Information-Theoretically Secure Radio Communication in Spacecraft Control
作者：Morioka, S., Obana, S., Yoshida, M.
DOI：10.1007/978-3-031-93706-4_14
URL: doi.org/10.1007/978-3-031-93706-4_14
