日本國立研究開發法人資訊通信研究機構（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
