Fugu-MT 論文翻訳(概要): What You Code Is What We Prove: Translating BLE App Logic into Formal Models with LLMs for Vulnerability Detection

論文の概要: What You Code Is What We Prove: Translating BLE App Logic into Formal Models with LLMs for Vulnerability Detection

arxiv url: http://arxiv.org/abs/2509.09291v1
Date: Thu, 11 Sep 2025 09:27:37 GMT
ステータス: 翻訳完了
システム内更新日: 2025-09-12 16:52:24.315025
Title: What You Code Is What We Prove: Translating BLE App Logic into Formal Models with LLMs for Vulnerability Detection
Title（参考訳）: BLE App Logic を LLM で形式モデルに翻訳して脆弱性検出
Authors: Biwei Yan, Yue Zhang, Minghui Xu, Runyu Pan, Jinku Li, Xiuzhen Cheng,
Abstract要約: 本稿では,BLEアプリケーションセキュリティ分析を意味翻訳問題として再編成する。脆弱性を直接検出するのではなく、トランスレータとして機能するために、大きな言語モデル(LLM)を活用しています。静的解析,プロンプト誘導型LLM翻訳,シンボル検証を組み合わせたシステムであるVerifiaBLEで,このアイデアを実装した。
参考スコア（独自算出の注目度）: 20.200451226371097
License: http://creativecommons.org/licenses/by/4.0/
Abstract: The application layer of Bluetooth Low Energy (BLE) is a growing source of security vulnerabilities, as developers often neglect to implement critical protections such as encryption, authentication, and freshness. While formal verification offers a principled way to check these properties, the manual effort of constructing formal models makes it impractical for large-scale analysis. This paper introduces a key insight: BLE application security analysis can be reframed as a semantic translation problem, i.e., from real-world code to formal models. We leverage large language models (LLMs) not to directly detect vulnerabilities, but to serve as translators that convert BLE-specific code into process models verifiable by tools like ProVerif. We implement this idea in VerifiaBLE, a system that combines static analysis, prompt-guided LLM translation, and symbolic verification to check three core security features: encryption, randomness, and authentication. Applied to 1,050 Android BLE apps, VerifiaBLE uncovers systemic weaknesses: only 10.2\% of apps implement all three protections, while 53.9\% omit them entirely. Our work demonstrates that using LLMs as structured translators can lower the barrier to formal methods, unlocking scalable verification across security-critical domains.
Abstract（参考訳）: Bluetooth Low Energy(BLE)のアプリケーション層は、セキュリティ上の脆弱性の増大の原因である。形式的検証はこれらの特性を確認するための原則的な方法を提供するが、形式的モデルを構築するための手作業は、大規模な解析には実用的ではない。本稿では,BLEアプリケーションセキュリティ分析を,実世界のコードから形式的モデルへの意味翻訳問題として再編成する。私たちは、脆弱性を直接検出するのではなく、BLE固有のコードをProVerifのようなツールで検証可能なプロセスモデルに変換するトランスレータとして機能するために、大きな言語モデル(LLM)を活用しています。静的解析,プロンプト誘導LLM翻訳,シンボル検証を組み合わせて,暗号化,ランダム性,認証の3つのコアセキュリティ機能をチェックするシステムであるVerifiaBLEにこのアイデアを実装した。 1,050のAndroid BLEアプリに適用されたVerifiaBLEは、システム上の弱点を明らかにしている。我々の研究は、LLMを構造化トランスレータとして使用することで、形式的なメソッドの障壁を減らし、セキュリティクリティカルなドメインにわたるスケーラブルな検証をアンロックできることを実証している。

関連論文リスト

Evaluating Language Model Reasoning about Confidential Information [95.64687778185703]
言語モデルが文脈的堅牢性を示すか、文脈依存型安全仕様に準拠する能力を示すかを検討する。我々は,ユーザ要求がいつ承認されたか,言語モデルが正しく判断できるかどうかを測定するベンチマーク(PasswordEval)を開発した。現在のオープンソースとクローズドソースのモデルでは、一見単純な作業に苦労しています。
論文参考訳（メタデータ） (2025-08-27T15:39:46Z)
LLMSymGuard: A Symbolic Safety Guardrail Framework Leveraging Interpretable Jailbreak Concepts [5.019114272620707]
この研究は、Sparse Autoencoders (SAE)を活用して解釈可能な概念を識別する新しいフレームワークである textbfLLMSymGuardを導入している。意味的に意味のある内部表現を抽出することで、LLMSymGuardは象徴的で論理的な安全ガードレールを構築することができる。
論文参考訳（メタデータ） (2025-08-22T12:13:38Z)
Learning to Detect Unknown Jailbreak Attacks in Large Vision-Language Models: A Unified and Accurate Approach [22.248911000455706]
本稿では、異常検出としてジェイルブレイク検出を定式化する、新しい教師なしフレームワークを提案する。 LoDは最先端の性能を達成し、平均的なAUROCは0.9951で、最強のベースラインよりも最小のAUROCは38.89%向上した。
論文参考訳（メタデータ） (2025-08-08T16:13:28Z)
ARMOR: Aligning Secure and Safe Large Language Models via Meticulous Reasoning [49.47193675702453]
大規模言語モデル(LLM)は、顕著な生成能力を示している。 LLMは、安全上の制約を回避できる悪意のある命令に弱いままである。推論に基づく安全アライメントフレームワークARMORを提案する。
論文参考訳（メタデータ） (2025-07-14T09:05:54Z)
Guiding AI to Fix Its Own Flaws: An Empirical Study on LLM-Driven Secure Code Generation [16.29310628754089]
大規模言語モデル(LLM)は、コードの自動生成のための強力なツールになっている。 LLMは、しばしば重要なセキュリティプラクティスを見落とし、安全でないコードを生成する。本稿では、安全性の低いコードを生成するための固有の傾向、自己生成する脆弱性ヒントによってガイドされた場合にセキュアなコードを生成する能力、フィードバックレベルが異なる場合に脆弱性を修復する効果について検討する。
論文参考訳（メタデータ） (2025-06-28T23:24:33Z)
Decompiling Smart Contracts with a Large Language Model [51.49197239479266]
Etherscanの78,047,845のスマートコントラクトがデプロイされているにも関わらず(2025年5月26日現在)、わずか767,520 (1%)がオープンソースである。この不透明さは、オンチェーンスマートコントラクトバイトコードの自動意味解析を必要とする。バイトコードを可読でセマンティックに忠実なSolidityコードに変換する,先駆的な逆コンパイルパイプラインを導入する。
論文参考訳（メタデータ） (2025-06-24T13:42:59Z)
Training Language Models to Generate Quality Code with Program Analysis Feedback [66.0854002147103]
大規模言語モデル(LLM)によるコード生成は、ますます本番環境で採用されているが、コード品質の保証には失敗している。実運用品質のコードを生成するためにLLMにインセンティブを与える強化学習フレームワークであるREALを提案する。
論文参考訳（メタデータ） (2025-05-28T17:57:47Z)
Vulnerability Detection: From Formal Verification to Large Language Models and Hybrid Approaches: A Comprehensive Overview [3.135279672650891]
本稿では,最先端のソフトウェアテストと検証に焦点をあてる。古典的な形式的手法、LLMに基づく分析、新しいハイブリッド手法の3つの主要なアプローチに焦点を当てている。 LLMによるインサイトとフォーマルリガーを統合することで,ソフトウェア検証の有効性とスケーラビリティが向上するかどうかを解析する。
論文参考訳（メタデータ） (2025-03-13T18:22:22Z)
Software Vulnerability and Functionality Assessment using LLMs [0.8057006406834466]
我々は,Large Language Models (LLMs) がコードレビューに役立つかどうかを検討する。我々の調査は、良質なレビューに欠かせない2つの課題に焦点を当てている。
論文参考訳（メタデータ） (2024-03-13T11:29:13Z)
CodeChameleon: Personalized Encryption Framework for Jailbreaking Large Language Models [49.60006012946767]
パーソナライズされた暗号化手法に基づく新しいジェイルブレイクフレームワークであるCodeChameleonを提案する。我々は、7つの大規模言語モデルに関する広範な実験を行い、最先端の平均アタック成功率(ASR)を達成する。 GPT-4-1106上で86.6%のASRを実現する。
論文参考訳（メタデータ） (2024-02-26T16:35:59Z)
CodeLMSec Benchmark: Systematically Evaluating and Finding Security Vulnerabilities in Black-Box Code Language Models [58.27254444280376]
自動コード生成のための大規模言語モデル(LLM)は、いくつかのプログラミングタスクにおいてブレークスルーを達成した。これらのモデルのトレーニングデータは、通常、インターネット(例えばオープンソースのリポジトリから)から収集され、障害やセキュリティ上の脆弱性を含む可能性がある。この不衛生なトレーニングデータは、言語モデルにこれらの脆弱性を学習させ、コード生成手順中にそれを伝播させる可能性がある。
論文参考訳（メタデータ） (2023-02-08T11:54:07Z)

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

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