文献

J-GLOBAL ID：202002279817538598   整理番号：20A2515345

InSpectre:形式的解析によるマイクロアーキテクチャ脆弱性の破壊と固定【JST・京大機械翻訳】

InSpectre: Breaking and Fixing Microarchitectural Vulnerabilities by Formal Analysis

著者 (3件)： Guanciale Roberto (KTH Royal Institute of Technology, Strockholm, Sweden) ,  Balliu Musard (KTH Royal Institute of Technology, Stockholm, Sweden) ,  Dam Mads (KTH Royal Institute of Technology, Stockholm, Sweden)
資料名： ACM Proceedings  (ACM Proceedings)
号： CCS ’20  ページ： 1853-1869  発行年： 2020年 
JST資料番号： D0698C  資料種別： 会議録 (C)
記事区分： 原著論文  発行国： アメリカ合衆国 (USA)  言語： 英語 (EN)

抄録/ポイント： 最近のSpectre攻撃は,現在のコンピュータマイクロアーキテクチャの基本的なセキュリティを実証した。攻撃は,プロセスのメモリコンテンツに関する任意の情報を抽出するために,パイプライン化,アウトオブオーダ,および推測のような特徴を使用する。高性能パイプライン化アーキテクチャに意味がある,順序外および推測的挙動の形式を表すことができる包括的な形式的マイクロアーキテクチュラルモデルはまだ現れていない。このようなモデルは,脆弱性の存在と非存在性,および形式的に確立された対策の健全性を可能にするので,非常に有用である。本論文は,単一コアプロセッサを目標とするそのようなモデルを提示する。モデルは意図的に非常に一般的であり,実際のCPUのモデルを定義するためのインフラストラクチャを提供する。それは,すべての既知のSpectre脆弱性を支えている微小構造特徴を組み込んだ。既存と新しい脆弱性のセキュリティを解明し,提案した対策の有効性を形式的に解析するために,モデルを使用した。特に,Spectre v4の新しい変種,推測的フェッチに対する脆弱性,および順序外実行に対する脆弱性を含む3つの新しい(潜在的)脆弱性を発見し,一定時間および連続命令を含む既存の対策の有効性を解析した。Please refer to this article’s citation page on the publisher website for specific rights information. Translated from English into Japanese by JST.【JST・京大機械翻訳】

シソーラス用語： 記憶装置 ,  微細構造 ,  パイプライン演算 ,  インフラストラクチャー ,  有効性 ,  *計算機アーキテクチャ ,  パイプライン処理 ,  コンピュータ ,  セキュリティ ,  健全性 ,  コンテンツ
準シソーラス用語： *マイクロアーキテクチャ ,  脆弱性 ,  フェッチ , 【Automatic Indexing@JST】

著者キーワード (7件)： 対策 ,  形式モデル ,  マイクロアーキテクチャ ,  注文外 ,  推測 ,  検証 ,  脆弱性

分類 (2件)： 制御方式  (JC02030K) ,  ディジタル計算機方式一般  (JC02010O)

タイトルに関連する用語 (4件)： 解析 ,  マイクロアーキテクチャ ,  脆弱性 ,  破壊