文献

J-GLOBAL ID：202202220030948031   整理番号：22A0691442

Verbatim++:導関数による検証,最適化,および意味的に豊富な語彙化【JST・京大機械翻訳】

Verbatim++: verified, optimized, and semantically rich lexing with derivatives

著者 (3件)： Egolf Derek (Northeastern University, USA) ,  Lasser Sam (Tufts University, USA) ,  Fisher Kathleen (Tufts University, USA)
資料名： ACM Proceedings  (ACM Proceedings)
号： CPP 2022  ページ： 27-39  発行年： 2022年 
JST資料番号： D0698C  資料種別： 会議録 (C)
記事区分： 原著論文  発行国： アメリカ合衆国 (USA)  言語： 英語 (EN)

抄録/ポイント： レクサとパーサは,それらがソフトウェアシステムの内部と外部世界の間の境界にしばしば座るので,攻撃者にとって魅力的なターゲットである。形式的に検証されたレクサは,これらのシステムの攻撃表面を減らすことができ,より安全なものにする。この方向における一つの最近のステップは,Brzzozowski誘導体の概念に基づく検証済みレクサであるVerbatimの開発である。2つの限界はツールの有用性を制限する。最初に,その実行時間は,その入力ストリングの長さにおいて二次である。第2に,レクサは単純な「タグとストリング」表現でトークンを生成し,それはより表現的なトークン表現で操作するパーザと統合するツールの能力を制限する。本研究では,ツールの元の正当性保証を保存しながら,これらの限界を克服するVerbatimに対する一連の拡張を示した。レクサはJSONベンチマークに対して,最適化の組み合わせを通して効果的に線形性能を達成し,これは以前には検証されていない。また,Verbatimの強化版は,ユーザがカスタム意味行動で語彙仕様を強化でき,これらの行動を用いて意味的に豊富なトークン,すなわち,任意のユーザ定義型を持つ値を運ぶトークンを生成する。すべての拡張を実行し,Coq Proof Assistantを用いて検証した。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】

著者キーワード (4件)： Brzozowski誘導体 ,  形式的検証 ,  語彙分析 ,  意味行動

分類 (3件)： 計算機システム開発  (JD02010R) ,  データ保護  (JD01020V) ,  オペレーティングシステム  (JD03020J)

タイトルに関連する用語 (4件)： 導関数 ,  検証 ,  最適化 ,  意味