ハードウェアトロイおよび敵対的攻撃に対する脆弱性の自動検知
現代の世界は複雑な電子システムに依存しています。コネクテッド自律走行車両(Connected Autonomous Vehicles - CAV)、医療機器、航空宇宙、スマートフォン、防衛システム、原子力発電所ならびにその他の重要インフラ、5Gネットワーク、IoTデバイス、そしてクラウドコンピューティングなど、これらはすべて敵対的攻撃に耐え、人々の安全とプライバシーを守れなくてはなりません。
これまで、セキュリティエンジニアリングはソフトウェアとシステムレベルの問題に重点を置いてきました。しかしながら、ますます多くのリスクと攻撃にハードウェアが関わっていることを示す十分な証拠があります。比較的簡単なプロセッサを使用している組み込みシステムも例外ではありません。悪意を持ったアクターは、不埒な目的のためにハードウェアトロイや脆弱性を悪用するシナリオを組み立てることがあります。
セキュアなシステムを基礎から構築するには、ハードウェア保証(Hardware Assurance - HwA)がきわめて重要となります。OneSpinはICインテグリティへのホリスティックなアプローチにより、機能正確性と安全性だけではなく信頼性とセキュリティも検証するソリューションを提供します。
自動化された信頼性評価
IC開発プロセスのあらゆる段階において、ハードウェアトロイや悪意あるロジックが挿入される危険があります。最新の、高度に構成変更可能なハードウェアは、バックドア、時限爆弾、パフォーマンス劣化やキルスイッチなどの恰好の隠れ場所を提供します。改ざんのリスクは、もはや無視することはできません。しかし、SoCインテグレーションの前に内製またはサードパーティ製半導体IP(3PIP)を人手でレビューすることはコストがかかりすぎ、非効率的です。また機能的プリシリコン検証は信頼性の懸念には対応できません。
OneSpinは信頼性評価データおよびレポートを自動的に生成するソリューションを提供します。ハードウェアの知識が限定的な監査担当者、IPのインプリメンテーションの詳細になじみのないエンジニア、そして信頼性保証エキスパートが、これらのソリューションを使用して客観的かつ効率的アプローチにより疑わしいロジックを検知し、信頼性を評価することができます。
トロイが存在しない証明
プリシリコン検証はIPの機能正確性を確認するもので、IPが仕様通りに、すべきことをすることを保証します。一方、トロイが存在しないことは、IPが仕様以外のことをしないという厳密な証明によってしか確認できません。
OneSpinのGapFreeVerification™ はIPのRTLモデル内に機能的バグと隠れた悪意ある機能のどちらも存在しないことを網羅的に証明します。このプロセスにより、信頼のおける実行可能な仕様が生成されます。また仕様の抜けや不整合も検知します。RISC-VプロセッサコアなどクリティカルなIPに対しては、プリパッケージされたSystemVerilogアサーション(SVA)を実行可能な仕様として使ったアプリも用意されています。詳細については、GOMACTech 2019で発表された論文、Complete Formal Verification of RISC V Processor IPs for Trojan-Free Trusted ICs を参照してください。
OneSpinのEC-RTL™、EC-ASIC™ ならびに EC-FPGA™ はフォーマルシーケンシャル等価性チェック(EC)を使用して設計の2つの表現を比較します。ECは合成や配置配線などによる設計の変換により、偶発的あるいは悪意ある変更が入り込んでいないことを証明します。
セキュリティ検証
敵対者はコーナーケースのハードウェアバグや予期せぬ悪用シナリオを用いて攻撃ベクターを構築するかもしれません。DoS攻撃、権限エスカレーション、サイドチャネル、およびその他の攻撃により、保護対象のアセット、たとえば暗号化キーなどの機密性、整合性、あるいは可用性が損なわれる恐れがあります。
セキュリティは、IC開発を構成する要素として、ハードウェア開発ライフサイクル全体をカバーしならなければなりません。HRoT(Hardware Root of Trust)ならびにその他のセキュリティIPまたは機能は、厳格に検証しなければなりません。ハードウェアのセキュアなリージョンとセキュアでないリージョンが適切に分離されているかどうかをチェックすることもきわめて重要です。
OneSpinのセキュリティソリューションは複雑なIPやSoCに含まれるセキュリティに関連したハードウェアの脆弱性を探し出す独自のテクノロジを活用しています。OneSpinのテクノロジは、認証されていないインターフェイスやトランザクションと保護されたアセット、マイクロアーキテクチャおよびインプリメンテーションレベルのサイドチャネル等との間の情報の経路を検知する、あるいはその不存在を徹底的に証明する効率的なプロセスを実現しています。
自動車のサイバーセキュリティとISO/SAE 21434
自動車と他の車両、インフラ、クラウド(V2X)を接続し、セキュリティおよびセーフティクリティカルな機能を実行する複雑な電子システムは、多数の物理的あるいは遠隔地からの攻撃の機会を生み出しています。自動車のサイバーセキュリティは、安全性を確保しIPとデータを保護する上できわめて重要です。自動車メーカーならびにサプライチェーンは、セキュアなハードウェアおよびソフトウェアコンポーネントに基づいてセキュアなシステムを開発および維持する、包括的で標準化されたシステムを必要としています。これから発行されるサイバーセキュリティ規格ISO/SAE 21434 Road vehiclesはSAE J3061に代わるもので、このニーズへの対応が約束されています。
ISO/SAE 21434標準は、セキュリティとは既存のシステムやコンポーネントの上に構築できるものではなく、セキュリティバイデザインの設計プロセスが必要である、ということを認識しています。脅威分析とリスクアセスメント(TARA)はこの規格の重要な部分であり、またシステムおよびそのセキュリティ要件をモデル化し、ハードウェアおよびソフトウェアコンポーネントへの依存関係を追跡し、リスク評価を実施する専用ツールを使って自動化することのできるアクティビティでもあります。itemis 社が提供するウェブサイトでは、ISO/SAE 21434標準の包括的な概要を提供しています。ew of the ISO/SAE 21434 standard.
OneSpinは車載ICよびIPのセキュリティ要件違反を特定する独自のソリューションを提供しています。
More information…
OneSpin’s Operational SVA enables formal verification enthusiasts to develop high-level, non-overlapping assertions that capture end-to-end transactions and requirements in a concise, elegant way.
»Learn more…The OneSpin 360 Design Verification (DV) product line leverages the most advanced, high-performance formal technology as the basis for a range of verification solutions, from automated design analysis to advanced property checking.
»Download the flyer…OneSpin’s Quantify measures the quality of a formal verification test bench. It provides precise, actionable information on what parts of the design-under-test (DUT) are verified, and it highlights RTL code that could still hide bugs.
»Download the data sheet…OneSpin 360 DV-Verify adds coverage-driven assertion-based verification (ABV) to the DVInspect platform.
»Download the data sheet…Design verification has a lot in common with human hygiene practices. The goal of both activities is to remove all dirt, grime, and bugs through an active process of establishing good hygiene.
»Download the white paper…Fault-tolerant hardware development is no longer a niche and presents new challenges. Many engineers face the daunting task of having to examine countless faulty variants of their design in order to integrate and verify multiple safety mechanisms within complex Systems-on-Chip (SoCs).
»Download the white paper…Get in touch!
Learn more about trust and security verification with OneSpin!
John Hallman, Product Manager Trust and Security