Questa Secure Check

 

クリティカルな記憶素子へのセキュアパスを徹底検証

Questa Secure Checkは、セキュリティ面または安全面が絶対的に重要な記憶素子には特定のパスしか到達できないことを徹底的に検証する(つまり、DUTの「信頼性の根拠」に一点の曇りもないことをフォーマルに証明する)完全自動化ソリューションです。フォーマル検証の知識もプロパティ言語の知識も必要ありません。

ホワイトハットハッキングは拡張流用できない

モバイル支払処理に必要な個人暗号キーからセットトップボックスの加入者認証コード、軍事/宇宙航空用通信システム、ペースメーカに埋め込まれた治療パラメータにいたるまで、セキュリティ保護された記憶素子へのアクセス検証は非常に重要な難しい作業です。実際、自動車のECUあるいは医療用機器などのセーフティクリティカルなシステムでは、外部ハッカーからの攻撃だけでなく、バグや想定外の影響により重要なデータが破壊されることのないよう対策を講じておかなければなりません。

しかしながら、一般的な対処法には拡張性がありません。簡単に言うと、セキュアな記憶素子までのクリティカルパスを専門家が調査する方法は、回路が複雑化することで効果が急速に失われるのです。さらに、細心の注意を払って設計された制約付きランダムシミュレーション環境でも完全に網羅できるものではありません。

最後の手段として、標準的なフォーマル検証手法を実装しようとすると、面倒な手作業になってしまいます。数千にものぼるパスに対して1つ1つに手作業でアサーションを挿入する必要がありますが、通常のアサーションとフォーマル検証手法では、接続の有無はチェックできないのが現実です。

Questa Secure Check  

RTL記述、セキュアな記憶素子とパスの仕様をQuesta Secure Checkに入力すると、フォーマル検証が自動実行され、安全面とセキュリティ面が絶対的に重視される記憶素子には指定したパスしか到達していないことを徹底的に検証します。フォーマル検証の知識もプロパティ言語の知識も必要ありません。

ソリューション: Questa Secure Check

RTL記述と可読性の優れたスプレッドシート形式を使用して、安全面とセキュリティ面が絶対的に重視される記憶素子と正しいアクセスパスを指定します。その後、これらのファイルを入力としてQuesta Secure Checkに取り込むと、フォーマルベース検証が自動的に実行され、指定した素子に問題がないこと(つまり、RTL記述のモデルは「十分に信頼できる」こと)を網羅的にチェックします。外部から導入したことが明らかなIPと付随するパスを「ブラックボックス化」して、セキュリティ面が重視されるチャネルに限って検証することで、解析を高速化するとともにコンパイル/実行時間の最小化を図ります。検証結果は、設計の完全性の証明、また場合によっては仕様に対する違反を反証によって示します。

特長

  • セキュリティ/安全面が最重視されるデータの完全性を徹底検証
  • 機密データのレジスタからの不正読み出し、強制書き換え、間接的なデータ破壊を防止
  • セキュアなデータレジスタへの直接/間接パスをすべて自動的に特定/検証
  • ハッカーの攻撃対象となりそうな制御信号とデータパスを波形と回路図生成で正確に表示
  • セキュアデータがDUTを期待どおり安全に正しく通過できることを「証明トレース」波形で実証可能

利点

  • 網羅的でスケーラブルな検証
  • フォーマル検証やアサーションの知識なしで容易にセットアップ
  • 仕様とDUTの間の不整合は反証の波形と回路図により明確化
製品情報リクエスト