論文の概要: How We Built Cedar: A Verification-Guided Approach
- arxiv url: http://arxiv.org/abs/2407.01688v1
- Date: Mon, 1 Jul 2024 18:01:07 GMT
- ステータス: 処理完了
- システム内更新日: 2024-07-03 19:42:31.566980
- Title: How We Built Cedar: A Verification-Guided Approach
- Title(参考訳): Cedarの作り方: 検証ガイドによるアプローチ
- Authors: Craig Disselkoen, Aaron Eline, Shaobo He, Kyle Headley, Michael Hicks, Kesha Hietala, John Kastner, Anwar Mamat, Matt McCutchen, Neha Rungta, Bhakti Shah, Emina Torlak, Andrew Wells,
- Abstract要約: 私たちは検証誘導開発(VGD)を使用して、表現力、高速、安全、分析可能な承認のための新しいポリシー言語であるCedarを構築します。
- 参考スコア(独自算出の注目度): 3.6811845473752616
- License: http://creativecommons.org/licenses/by/4.0/
- Abstract: This paper presents verification-guided development (VGD), a software engineering process we used to build Cedar, a new policy language for expressive, fast, safe, and analyzable authorization. Developing a system with VGD involves writing an executable model of the system and mechanically proving properties about the model; writing production code for the system and using differential random testing (DRT) to check that the production code matches the model; and using property-based testing (PBT) to check properties of unmodeled parts of the production code. Using VGD for Cedar, we can build fast, idiomatic production code, prove our model correct, and find and fix subtle implementation bugs that evade code reviews and unit testing. While carrying out proofs, we found and fixed 4 bugs in Cedar's policy validator, and DRT and PBT helped us find and fix 21 additional bugs in various parts of Cedar.
- Abstract(参考訳): 本稿では,Cedarの開発に使用したソフトウェアエンジニアリングプロセスである検証誘導開発(VGD)について述べる。
VGDでシステムを開発するには、システムの実行可能なモデルを書き、モデルに関する特性を機械的に証明すること、システムのプロダクションコードを書き、生産コードがモデルと一致することを確認するために差分ランダムテスト(DRT)を使い、生産コードの未モデル化部分のプロパティをチェックするためにプロパティベースのテスト(PBT)を使用する。
CedarのVGDを使って、高速で慣用的なプロダクションコードを構築し、モデルを正しく証明し、コードレビューやユニットテストを避けるための微妙な実装バグを見つけて修正することができます。
Cedarのポリシー検証ツールで4つのバグを発見し、修正しました。そしてDRTとPBTは、Cedarのさまざまな部分で21のバグを発見し、修正しました。
関連論文リスト
- Code Agents are State of the Art Software Testers [10.730852617039451]
ユーザ問題をテストケースに形式化するLLMベースのコードエージェントについて検討する。
私たちは人気のあるGitHubリポジトリに基づいた新しいベンチマークを提案し、現実世界の問題、地味なパッチ、ゴールデンテストを含む。
LLMは一般的に、コード修復用に設計されたCode Agentsを使って、関連するテストケースを生成するのに驚くほどうまく機能します。
論文 参考訳(メタデータ) (2024-06-18T14:54:37Z) - MoCo: Fuzzing Deep Learning Libraries via Assembling Code [13.937180393991616]
ディープラーニング技術は様々なアプリケーションシナリオを持つソフトウェアシステムに応用されている。
DLライブラリはDLシステムの基盤として機能し、その中のバグは予測不可能な影響をもたらす可能性がある。
そこで本研究では,組立コードによるDLライブラリのファジングテスト手法であるMoCoを提案する。
論文 参考訳(メタデータ) (2024-05-13T13:40:55Z) - Learning to Plan and Generate Text with Citations [69.56850173097116]
提案手法は, テキストの忠実性, 接地性, 制御性を向上させるために最近実証されたプランベースモデルの帰属性について検討する。
本稿では,異なるブループリントの変種を利用する帰属モデルと,質問をゼロから生成する抽象モデルと,質問を入力からコピーする抽出モデルを提案する。
論文 参考訳(メタデータ) (2024-04-04T11:27:54Z) - Patch2QL: Discover Cognate Defects in Open Source Software Supply Chain
With Auto-generated Static Analysis Rules [1.9591497166224197]
本稿では,SASTルールの自動生成によるOSSのコグネート欠陥の検出手法を提案する。
具体的には、プリパッチバージョンとポストパッチバージョンから重要な構文と意味情報を抽出する。
我々はPatch2QLというプロトタイプツールを実装し、それをC/C++の基本OSSに適用した。
論文 参考訳(メタデータ) (2024-01-23T02:23:11Z) - TrojanedCM: A Repository of Trojaned Large Language Models of Code [4.838807847761728]
TrojanedCMは、ソースコードのクリーンで有毒なモデルの公開リポジトリである。
2つのコード分類タスク(欠陥検出とクローン検出)とコード生成タスクに対して有毒なモデルを提供する。
リポジトリはまた、モデルのアーキテクチャとパラメータへの完全なアクセスを提供し、実践者がさまざまなホワイトボックス分析テクニックを調査できるようにする。
論文 参考訳(メタデータ) (2023-11-24T21:58:06Z) - SR-OOD: Out-of-Distribution Detection via Sample Repairing [48.272537939227206]
アウト・オブ・ディストリビューション(OOD)検出は、機械学習モデルの信頼性と堅牢性を保証するための重要なタスクである。
近年の研究では、生成モデルはOODサンプルに高い信頼度を割り当てることがしばしばあり、データのセマンティックな情報を捕捉できないことが示されている。
我々は,サンプル修復の利点を生かし,新しいOOD検出フレームワーク,SR-OODを提案する。
本フレームワークは,OOD検出における最先端な生成手法よりも優れた性能を実現する。
論文 参考訳(メタデータ) (2023-05-26T16:35:20Z) - Who Wrote this Code? Watermarking for Code Generation [53.24895162874416]
本稿では,機械生成テキストを検出するために,Entropy Thresholding (SWEET) を用いたSelective WatErmarkingを提案する。
実験の結果,SWEETはコード品質を著しく向上し,すべてのベースラインを上回ります。
論文 参考訳(メタデータ) (2023-05-24T11:49:52Z) - Execution-based Evaluation for Data Science Code Generation Models [97.96608263010913]
データサイエンスコード生成タスクの実行評価のための評価データセットであるExeDSを紹介する。
ExeDSにはJupyter Notebooksの534の問題が含まれており、それぞれがコードコンテキスト、タスク記述、参照プログラム、望ましい実行出力で構成されている。
表面形状評価スコアを高い精度で達成した5つの最先端コード生成モデルの実行性能を評価する。
論文 参考訳(メタデータ) (2022-11-17T07:04:11Z) - Auditing AI models for Verified Deployment under Semantic Specifications [65.12401653917838]
AuditAIは、解釈可能な形式検証とスケーラビリティのギャップを埋める。
AuditAIは、画素空間の摂動のみを用いた検証の限界に対処しながら、検証と認定トレーニングのための制御されたバリエーションを得られるかを示す。
論文 参考訳(メタデータ) (2021-09-25T22:53:24Z) - DAE : Discriminatory Auto-Encoder for multivariate time-series anomaly
detection in air transportation [68.8204255655161]
識別オートエンコーダ(DAE)と呼ばれる新しい異常検出モデルを提案する。
通常のLSTMベースのオートエンコーダのベースラインを使用するが、いくつかのデコーダがあり、それぞれ特定の飛行フェーズのデータを取得する。
その結果,DAEは精度と検出速度の両方で良好な結果が得られることがわかった。
論文 参考訳(メタデータ) (2021-09-08T14:07:55Z) - ControlFlag: A Self-Supervised Idiosyncratic Pattern Detection System
for Software Control Structures [1.370633147306388]
本稿では,自己教師型機械プログラミング(MP)システムであるControlFlagを紹介する。
ソフトウェア制御構造における慣用的パターン違反の検出を試みる。
ControlFlagはすでに、開発者によって承認され、修正されたCURLの異常を発見している。
論文 参考訳(メタデータ) (2020-11-06T22:19:05Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト(すべての情報・翻訳含む)の品質を保証せず、本サイト(すべての情報・翻訳含む)を使用して発生したあらゆる結果について一切の責任を負いません。