文献

J-GLOBAL ID：201202218652841409   整理番号：12A1243846

RockSalt:x86用のより良好,より高速,より強いSFI

RockSalt: Better, Faster, Stronger SFI for the x86

著者 (5件)： MORRISETT Greg (Harvard Univ.) ,  TAN Gang (Lehigh Univ.) ,  TASSAROTTI Joseph (Harvard Univ.) ,  TRISTAN Jean-Baptiste (Harvard Univ.) ,  GAN Edward (Harvard Univ.)
資料名： ACM SIGPLAN Notices (Association for Computing Machinery. Special Interest Group on Programming Languages)  (ACM SIGPLAN Notices (Association for Computing Machinery. Special Interest Group on Programming Languages))
巻： 47  号： 6  ページ： 395-404  発行年： 2012年06月 
JST資料番号： D0915A  ISSN： 0362-1340  資料種別： 逐次刊行物 (A)
記事区分： 原著論文  発行国： アメリカ合衆国 (USA)  言語： 英語 (EN)

抄録/ポイント： ネイティブクライアント(NaCl)はGoogle社によって提供された新しいサービスである。このNaClの中でセキュリティポリシーを強制するためにソフトウェアベース障害分離(SFI)が使われている。本論文において,筆者らはx86の部分集合に対する形式モデル及びRockSaltと呼ばれるNaCl用の新しく形式的に検証した検査器を提示した。本研究における主要な挑戦課題はx86の様な複雑なアーキテクチャに対するモデルの構築であった。この問題を扱うために,アーキテクチャの意味論を指定するためのドメイン固有言語(DSLs)を構築し,これらの言語をCoq内に埋込んだ。NaClのサンドボックスの様な単純だが現実のポリシーについての推論の体験は,本モデルが他の文脈においても有用であるとの保証を提供した。

シソーラス用語： *ソフトウェア障害 ,  *分離 ,  応用向き言語 ,  計算機アーキテクチャ ,  意味論 ,  セキュリティ ,  モデル ,  プログラミング言語 ,  制御
準シソーラス用語： Coq ,  *ドメイン固有言語 ,  ポリシー制御 ,  *形式モデル

分類 (4件)： 計算機システム開発  (JD02010R) ,  応用プログラミング言語  (JD03052Y) ,  数理言語学  (JB05000V) ,  データ保護  (JD01020V)