論文の概要: 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のバグを発見し、修正しました。

関連論文リスト

• CERBERUS: Crack Evaluation & Recognition Benchmark for Engineering Reliability & Urban Stability [0.0]
  CERBERUSは、インフラストラクチャの亀裂やその他の欠陥を検出するためのAIモデルをトレーニングし、評価するために設計されたベンチマークである。 クラックイメージジェネレータとUnityで構築された現実的な3D検査シナリオが含まれている。 その結果,合成データと実データを組み合わせることで,実画像の性能が向上することがわかった。
  論文  参考訳（メタデータ） (2025-06-27T04:52:52Z)
• LASA: Enhancing SoC Security Verification with LLM-Aided Property Generation [7.52190283487474]
  形式的プロパティ検証(FPV)は、設計の振る舞いをモデル化し、検証する機能を提供する。 現在のプラクティスでは、そのようなプロパティを作成するためにかなりの手作業が必要で、時間がかかり、コストがかかり、エラーが発生します。 本稿では,LLMと検索拡張生成(RAG)を活用して非空きセキュリティ特性を創出する新しいフレームワークであるLASAを提案する。
  論文  参考訳（メタデータ） (2025-06-22T01:21:03Z)
• VERINA: Benchmarking Verifiable Code Generation [47.9771074559674]
  大規模言語モデル(LLM)は、ソフトウェア開発にますます統合されている。 検証可能なコード生成は、この制限に対処するための有望なパスを提供する。 現在のベンチマークでは、エンドツーエンドの検証可能なコード生成がサポートされていないことが多い。
  論文  参考訳（メタデータ） (2025-05-29T06:12:52Z)
• Training Language Models to Generate Quality Code with Program Analysis Feedback [66.0854002147103]
  大規模言語モデル(LLM)によるコード生成は、ますます本番環境で採用されているが、コード品質の保証には失敗している。 実運用品質のコードを生成するためにLLMにインセンティブを与える強化学習フレームワークであるREALを提案する。
  論文  参考訳（メタデータ） (2025-05-28T17:57:47Z)
• VeriThoughts: Enabling Automated Verilog Code Generation using Reasoning and Formal Verification [28.196015311346024]
  本稿では、推論に基づくVerilogコード生成用に設計された新しいデータセットであるVeriThoughtsを紹介する。 我々は,生成したハードウェア記述の品質と正確性を評価するために,形式的検証手法に基づく新しいベンチマークフレームワークを構築した。 We present a suite of small-scale model based for Verilog generation。
  論文  参考訳（メタデータ） (2025-05-16T21:33:14Z)
• 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)

関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。

指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。