Fugu-MT 論文翻訳(概要): Type-based information flow analysis for $π$-calculus with a dynamically extensible security lattice

論文の概要: Type-based information flow analysis for $π$-calculus with a dynamically extensible security lattice

arxiv url: http://arxiv.org/abs/2606.27059v1
Date: Thu, 25 Jun 2026 14:03:51 GMT
ステータス: 翻訳完了
システム内更新日: 2026-06-26 18:46:32.314567
Title: Type-based information flow analysis for $π$-calculus with a dynamically extensible security lattice
Title（参考訳）: 動的拡張性セキュリティ格子を用いた$π$-calculusの型ベース情報フロー解析
Abstract要約: 我々は,セキュリティ格子に新たなセキュリティレベルを動的に挿入可能な,セキュアな情報フローのための型システムを開発した。本システムは,Milner's pi-calculusに対して,小林の型に基づくセキュア情報フロー解析を拡張して定式化した。
参考スコア（独自算出の注目度）: 0.0
License: http://creativecommons.org/licenses/by-nc-nd/4.0/
Abstract: We develop a type system for secure information flow where new security levels can be created and inserted into the security lattice dynamically, i.e., even in the middle of an execution of a system. Our system is formalized by extending Kobayashi's type-based secure information flow analysis for Milner's pi-calculus, which is one of the most expressive models (or "languages") supporting both sequential and concurrent computations, with concise syntax, reduction-based semantics, and bisimulation equivalence as a robust formalization of secrecy as non-interference. The development required careful treatment of extensions of lattices themselves as well as deliberate generalization from the simple 2-element lattice (consisting of only High and Low) in the original system.
Abstract（参考訳）: 我々は,システム実行中であっても,新たなセキュリティレベルを動的に生成し,セキュリティ格子に挿入可能な,セキュアな情報フローのための型システムを開発する。本システムは,Milner's pi-calculusの型ベースのセキュア情報フロー解析を拡張し,簡潔な構文,縮小型セマンティクス,ビシミュレーション同値を非干渉としての秘密の堅牢な形式化として,逐次的および並行的な計算をサポートするモデル(あるいは「言語」)の1つである。この発展には、格子自体の拡張を慎重に扱うことが必要であり、また元の系における単純な2要素格子(高と低のみからなる)からの故意の一般化も必要であった。

関連論文リスト

Provably Secure Agent Guardrail [89.79561918065122]
既存の防衛アーキテクチャは経験的セマンティックガードレールと確率論的大モデル調整器に依存している。本稿では,論理的推論の基本的制約に基づくエージェントのための新しいセキュリティパラダイムを提案する。
論文参考訳（メタデータ） (2026-05-28T02:12:41Z)
HIPO: Instruction Hierarchy via Constrained Reinforcement Learning [57.40686733111483]
textscHIPOは、制約付きマルコフ決定プロセスとしてHIFを定式化する新しいアライメントフレームワークである。 textscHIPOはシステムプロンプトを単に入力コンテキストから厳密なアルゴリズム境界まで高める。
論文参考訳（メタデータ） (2026-03-17T06:12:41Z)
Just Ask: Curious Code Agents Reveal System Prompts in Frontier LLMs [65.6660735371212]
textbftextscJustAskは,インタラクションのみで効果的な抽出戦略を自律的に発見するフレームワークである。これは、アッパー信頼境界に基づく戦略選択と、原子プローブと高レベルのオーケストレーションにまたがる階層的なスキル空間を用いて、オンライン探索問題として抽出を定式化する。この結果から,現代のエージェントシステムにおいて,システムプロンプトは致命的ではあるがほぼ無防備な攻撃面であることがわかった。
論文参考訳（メタデータ） (2026-01-29T03:53:25Z)
Kernel-Based Learning of Safety Barriers [0.9367224590861915]
安全クリティカルなアプリケーションにおけるAIアルゴリズムの迅速な統合は、厳格な安全基準を満たす能力に対する懸念を高めている。従来の安全検証ツールでは、AI駆動システムのブラックボックスの性質に苦戦している。離散時間力学を用いたブラックボックスシステムの安全性検証と合成のためのデータ駆動方式を提案する。
論文参考訳（メタデータ） (2026-01-17T10:42:35Z)
LUCID: Learning-Enabled Uncertainty-Aware Certification of Stochastic Dynamical Systems [0.8574682463936006]
従来の形式的検証ツールは、不透明なブラックボックスAIコンポーネントと複雑なダイナミクスの両方を組み込んだシステムに直面したときに不足する。我々は,ブラックボックス埋め込み動的システムの安全性を証明するための検証エンジンであるLUCIDを紹介する。 LUCIDは、このようなシステムの安全性を定量化する最初のツールである。
論文参考訳（メタデータ） (2025-12-12T17:46:50Z)
Rule Encoding and Compliance in Large Language Models: An Information-Theoretic Analysis [0.0]
大規模言語モデル(LLM)に基づく安全クリティカルエージェントの設計には、単純なプロンプトエンジニアリング以上のものが必要である。本稿では,ルールエンコーディングが注意機構やコンプライアンス行動にどのように影響するかを包括的に情報理論で分析する。
論文参考訳（メタデータ） (2025-09-23T14:42:32Z)
The Alignment Trap: Complexity Barriers [0.0]
本稿は、AIアライメントは単に難しいだけでなく、基本的な論理的矛盾に基づくものである、と論じる。私たちは、すべての必要な安全ルールを列挙できないため、マシンラーニングを正確に使用しています。このパラドックスは、5つの独立した数学的証明によって確認される。
論文参考訳（メタデータ） (2025-06-12T02:30:30Z)
Advancing Neural Network Verification through Hierarchical Safety Abstract Interpretation [52.626086874715284]
我々は、安全でない出力の階層構造を検証する抽象的DNN検証と呼ばれる新しい問題定式化を導入する。出力到達可能な集合に関する抽象的解釈と推論を活用することにより,形式的検証プロセスにおいて,複数の安全性レベルを評価することができる。我々の貢献には、新しい抽象的安全性の定式化と既存のアプローチとの関係を理論的に探求することが含まれる。
論文参考訳（メタデータ） (2025-05-08T13:29:46Z)
Data-Driven Distributionally Robust Safety Verification Using Barrier Certificates and Conditional Mean Embeddings [0.24578723416255752]
問題を非現実的な仮定にシフトすることなく,スケーラブルな形式検証アルゴリズムを開発する。問題を非現実的な仮定にシフトさせることなく,スケーラブルな形式検証アルゴリズムを開発するためには,バリア証明書の概念を用いる。本稿では,2乗法最適化とガウス過程エンベロープを用いて効率よくプログラムを解く方法を示す。
論文参考訳（メタデータ） (2024-03-15T17:32:02Z)
Decrypting Nonlinearity: Koopman Interpretation and Analysis of Cryptosystems [0.05120567378386613]
本稿では,Diffie-Hellman鍵交換系とRivest-Shamir-Adleman暗号系を非線形力学系として見ることにより,暗号系に対する新たな視点を導入する。クープマン理論を適用することで、これらの力学系を高次元空間に変換し、解析的に同値な純粋線型系を導出する。
論文参考訳（メタデータ） (2023-11-21T16:38:48Z)
Iterative Sketching for Secure Coded Regression [66.53950020718021]
分散線形回帰を高速化する手法を提案する。具体的には、方程式の系の基礎をランダムに回転させ、次にサブサンプルブロックを回転させ、情報を同時に確保し、回帰問題の次元を小さくする。
論文参考訳（メタデータ） (2023-08-08T11:10:42Z)
Perfectly Secure Steganography Using Minimum Entropy Coupling [60.154855689780796]
カチン1998のステガノグラフィー情報理論モデルでは, ステガノグラフィーの術式は完全に安全であることが示されている。また, 完全セキュアな手順の中で, 最小エントロピー結合によって誘導される場合に限, 情報スループットが最大になることを示す。
論文参考訳（メタデータ） (2022-10-24T17:40:07Z)

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