論文の概要: 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のバグを発見し、修正しました。
関連論文リスト
- Verifying Non-friendly Formal Verification Designs: Can We Start Earlier? [2.1626093085892144]
本稿では,2つの主要なステップからなるメタモデリング技術に基づく自動手法を提案する。
まず、C++で書かれた未使用のアルゴリズム記述を、生成されたアサーションを使用して早期に検証する。
第2に、HLECとそのメタモデルパラメータを用いて、このアルゴリズム記述をシーケンシャルな設計に対して検証する。
論文 参考訳（メタデータ） (2024-10-24T06:09:40Z) - Automated Proof Generation for Rust Code via Self-Evolution [69.25795662658356]
私たちは、Rustコードの自動証明生成を可能にする、人間による証明の欠如を克服する新しいフレームワークであるSAFEを紹介します。
GPT-4oに比べて効率と精度が優れていた。
この進歩により性能が大幅に向上し、人間の専門家によるベンチマークで70.50%の精度が達成された。
論文 参考訳（メタデータ） (2024-10-21T08:15:45Z) - SWT-Bench: Testing and Validating Real-World Bug-Fixes with Code Agents [10.730852617039451]
ユーザ問題をテストケースに形式化するLLMベースのコードエージェントについて検討する。
我々は人気のあるGitHubリポジトリに基づいた新しいベンチマークを提案し、現実世界の問題、地味なバグフィックス、ゴールデンテストを含む。
コード修復用に設計されたコードエージェントは,テスト生成用に設計されたシステムの性能を上回っている。
論文 参考訳（メタデータ） (2024-06-18T14:54:37Z) - VersiCode: Towards Version-controllable Code Generation [58.82709231906735]
大規模言語モデル(LLM)は、コード生成において大きな進歩を遂げていますが、既存の研究は、ソフトウェア開発の動的な性質を説明できません。
バージョン別コード補完(VSCC)とバージョン別コードマイグレーション(VACM)の2つの新しいタスクを提案する。
VersiCodeについて広範な評価を行い、バージョン管理可能なコード生成が確かに重要な課題であることを示した。
論文 参考訳（メタデータ） (2024-06-11T16:15:06Z) - 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) - 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)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。