宇宙放射線に耐える暗号回路の網羅的な動作保証を実現

全入力2の256乗通り 暗号回路には0又は1の値をとる入力を複数個与える。例えば入力が4個ある場合、それぞれの入力は0又は1の2通りの値をとるため、入力できる全ての値（全入力）の総数は2の4乗通りとなる。同様に、入力が8個ある場合、全入力は2の8乗通りとなる。一般に、入力がn個ある場合、全入力は2のn乗通りとなる。セキュリティ強度を高くするほど、全入力の数は増える。本研究で設計した暗号回路は高いセキュリティ強度を実現するため、入力は256個であり、全入力が2の256乗通りとなる。2の256乗通り（約10の77乗通り）は、観測可能な宇宙に存在するとされる原子の数に匹敵する非常に大きな数である。 元の記事へ

NewSpace 2000年頃から始まり最近になって活発化した、従来型の政府主導とは異なった民間主導による（ベンチャー企業や異業種参入を含む）宇宙開発活動を表した言葉。その活動は、人工衛星やロケットの開発と運用、衛星通信やリモートセンシング等のサービス提供、宇宙探査やスペースデブリ除去、エンターテインメント、有人飛行など多岐にわたる。際立った特徴の一つは、商用ベースに乗せることが求められるためにコストダウンや事業スピード向上への要求が強く、新規技術導入にも柔軟な点である。 元の記事へ

NASA Formal Methods アメリカ航空宇宙局（NASA）が主催する、システムの信頼性を数学的に保証する形式手法（Formal Methods）分野の歴史ある国際会議である。NASA、他の政府機関、学界、産業界の研究者と技術者が参加し、理論と実務の連携を促進する場となっている。宇宙、航空、ロボット工学及びその他のNASA関連のクリティカルシステムなど、わずかなバグや誤動作が人命に関わる大事故やミッションの失敗といった甚大な損失に直結するシステムの信頼性保証に関する課題を特定し、解決策を提示することを目的としている。 元の記事へ

人工衛星等の打上げ及び人工衛星の管理に関する法律に基づく基準等に関するガイドライン 本ガイドラインは、内閣府宇宙開発戦略推進事務局が発行している4つのガイドラインを指す。その中の一つ「人工衛星の打上げ用ロケットの型式認定に関するガイドライン」の6.5.2節「信頼性及び多重化」に「また、重要なシステム等に関する信号の送受信については、妨害や乗っ取りの被害にあわないよう、適切な暗号化等の措置を講ずること。」と記載されている。 元の記事へ

形式検証（Formal Verification） ハードウェアやソフトウェアが設計通りに正しく動作するかを、テスト実行だけに頼らず、数学的な理論に基づいて検証する技術であり、形式手法（Formal Methods）と呼ばれる研究分野の代表的な技術である。通常のテストではすべての入力に対する動作を確認することは困難だが、形式検証では数学的な性質を用いて動作の正しさを厳密に保証できる。本成果のように、2の256乗通り（約10の77乗通り）の入力をもつ暗号回路の動作保証において重要な技術である。 元の記事へ