論文の概要: Symmaries: Automatic Inference of Formal Security Summaries for Java Programs

• arxiv url: http://arxiv.org/abs/2512.20396v1
• Date: Tue, 23 Dec 2025 14:33:31 GMT
• ステータス: 翻訳完了
• システム内更新日: 2025-12-24 19:17:49.905181
• Title: Symmaries: Automatic Inference of Formal Security Summaries for Java Programs
• Title（参考訳）: Symmaries: Javaプログラムの形式的セキュリティサマリの自動推論
• Authors: Narges Khakpour, Nicolas Berthier,
• Abstract要約: Javaバイトコードプログラムの正式なセキュリティ仕様を構築するために、スケーラブルでモジュール化され、健全なアプローチを導入します。 要約は、メソッドのセキュリティ動作の抽象的な表現を提供する。 当社のアプローチは,セキュリティサマリー生成を自動化するSymariesというツールで実装されている。
• 参考スコア（独自算出の注目度）: 0.7305019142196582
• License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
• Abstract: We introduce a scalable, modular, and sound approach for automatically constructing formal security specifications for Java bytecode programs in the form of method summaries. A summary provides an abstract representation of a method's security behavior, consisting of the conditions under which the method can be securely invoked, together with specifications of information flows and aliasing updates. Such summaries can be consumed by static code analysis tools and also help developers understand the behavior of code segments, such as libraries, in order to evaluate their security implications when reused in applications. Our approach is implemented in a tool called Symmaries, which automates the generation of security summaries. We applied Symmaries to Java API libraries to extract their security specifications and to large real-world applications to evaluate its scalability. Our results show that the tool successfully scales to analyze applications with hundreds of thousands of lines of code, and that Symmaries achieves a promising precision depending on the heap model used. We prove the soundness of our approach in terms of guaranteeing termination-insensitive non-interference.
• Abstract（参考訳）: 我々は,Javaバイトコードプログラムの形式的セキュリティ仕様を,メソッド要約形式で自動構築する,スケーラブルでモジュール化された健全なアプローチを導入する。 要約は、メソッドのセキュリティ動作を抽象的に表現し、そのメソッドが安全に呼び出される条件と、情報フローの仕様、更新のエイリアスを含む。 このような要約は静的コード解析ツールによって消費され、またアプリケーションで再利用された際のセキュリティへの影響を評価するために、開発者がライブラリなどのコードセグメントの振る舞いを理解するのに役立つ。 当社のアプローチは,セキュリティサマリー生成を自動化するSymariesというツールで実装されている。 我々はSymariesをJava APIライブラリに適用し、そのセキュリティ仕様を抽出し、そのスケーラビリティを評価するために大規模な現実世界アプリケーションに適用した。 その結果、このツールは数十万行のコードでアプリケーションを解析するのに成功し、Symariesは使用したヒープモデルによって有望な精度を実現していることがわかった。 我々は,終端非感受性の非干渉を保証する観点から,我々のアプローチの健全性を証明する。

関連論文リスト

• Rethinking Testing for LLM Applications: Characteristics, Challenges, and a Lightweight Interaction Protocol [83.83217247686402]
  大言語モデル(LLM)は、単純なテキストジェネレータから、検索強化、ツール呼び出し、マルチターンインタラクションを統合する複雑なソフトウェアシステムへと進化してきた。 その固有の非決定主義、ダイナミズム、文脈依存は品質保証に根本的な課題をもたらす。 本稿では,LLMアプリケーションを3層アーキテクチャに分解する: textbftextitSystem Shell Layer, textbftextitPrompt Orchestration Layer, textbftextitLLM Inference Core。
  論文  参考訳（メタデータ） (2025-08-28T13:00:28Z)
• Exposing Go's Hidden Bugs: A Novel Concolic Framework [2.676686591720132]
  本稿では,Goプログラムを包括的に評価する新しい方法論であるZoryaを紹介する。 従来のテスト以上の脆弱性を明らかにするために、システミックに実行パスを探索することで、象徴的な実行には明確なメリットがある。 我々の解は、GhidraのP-Codeを中間表現(IR)として採用する。
  論文  参考訳（メタデータ） (2025-05-26T16:26:20Z)
• MARVEL: Multi-Agent RTL Vulnerability Extraction using Large Language Models [15.35860248847857]
  大きな言語モデル(LLM)は、このタスクの間、直接または既存のツールと連携するために使われてきた。 我々は、意思決定、ツールの使用、推論に対する統一的なアプローチのためのマルチエージェントLLMフレームワークであるMARVELを提案する。
  論文  参考訳（メタデータ） (2025-05-17T11:31:24Z)
• Secure Synthesis of Distributed Cryptographic Applications (Technical Report) [1.9707603524984119]
  我々はセキュアなプログラムパーティショニングを用いて暗号アプリケーションを合成することを提唱する。 このアプローチは有望だが、そのようなコンパイラのセキュリティに関する公式な結果はスコープに限られている。 我々は、堅牢で効率的なアプリケーションに不可欠な微妙さを扱うコンパイラのセキュリティ証明を開発した。
  論文  参考訳（メタデータ） (2024-01-06T02:57:44Z)
• The FormAI Dataset: Generative AI in Software Security Through the Lens of Formal Verification [3.2925005312612323]
  本稿では,脆弱性分類を伴う112,000のAI生成Cプログラムの大規模なコレクションであるFormAIデータセットを提案する。 すべてのプログラムには、型、行番号、脆弱な関数名を示すソースコード内の脆弱性がラベル付けされている。 ソースコードは112,000のプログラムで利用でき、各プログラムで検出された脆弱性を含む別のファイルが付属する。
  論文  参考訳（メタデータ） (2023-07-05T10:39:58Z)
• CodeLMSec Benchmark: Systematically Evaluating and Finding Security Vulnerabilities in Black-Box Code Language Models [58.27254444280376]
  自動コード生成のための大規模言語モデル(LLM)は、いくつかのプログラミングタスクにおいてブレークスルーを達成した。 これらのモデルのトレーニングデータは、通常、インターネット(例えばオープンソースのリポジトリから)から収集され、障害やセキュリティ上の脆弱性を含む可能性がある。 この不衛生なトレーニングデータは、言語モデルにこれらの脆弱性を学習させ、コード生成手順中にそれを伝播させる可能性がある。
  論文  参考訳（メタデータ） (2023-02-08T11:54:07Z)
• Realistic simulation of users for IT systems in cyber ranges [63.20765930558542]
  ユーザアクティビティを生成するために,外部エージェントを用いて各マシンを計測する。 このエージェントは、決定論的および深層学習に基づく手法を組み合わせて、異なる環境に適応する。 また,会話や文書の作成を容易にする条件付きテキスト生成モデルを提案する。
  論文  参考訳（メタデータ） (2021-11-23T10:53:29Z)
• Safe RAN control: A Symbolic Reinforcement Learning Approach [62.997667081978825]
  本稿では,無線アクセスネットワーク(RAN)アプリケーションの安全管理のためのシンボル強化学習(SRL)アーキテクチャを提案する。 我々は、ユーザが所定のセルネットワークトポロジに対して高レベルの論理的安全性仕様を指定できる純粋に自動化された手順を提供する。 ユーザがシステムに意図仕様を設定するのを支援するために開発されたユーザインターフェース(UI)を導入し、提案するエージェントの動作の違いを検査する。
  論文  参考訳（メタデータ） (2021-06-03T16:45:40Z)
• Evaluating the Safety of Deep Reinforcement Learning Models using Semi-Formal Verification [81.32981236437395]
  本稿では,区間分析に基づく半形式的意思決定手法を提案する。 本手法は, 標準ベンチマークに比較して, 形式検証に対して比較結果を得る。 提案手法は, 意思決定モデルにおける安全性特性を効果的に評価することを可能にする。
  論文  参考訳（メタデータ） (2020-10-19T11:18:06Z)
• SAMBA: Safe Model-Based & Active Reinforcement Learning [59.01424351231993]
  SAMBAは、確率論的モデリング、情報理論、統計学といった側面を組み合わせた安全な強化学習のためのフレームワークである。 我々は,低次元および高次元の状態表現を含む安全な力学系ベンチマークを用いて,アルゴリズムの評価を行った。 アクティブなメトリクスと安全性の制約を詳細に分析することで,フレームワークの有効性を直感的に評価する。
  論文  参考訳（メタデータ） (2020-06-12T10:40:46Z)

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

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