論文の概要: Certified Compilation in the TELEPERM XS Nuclear Safety I&C Platform
- arxiv url: http://arxiv.org/abs/2609.34871v1
- Date: Mon, 28 Sep 2026 10:55:53 GMT
- ステータス: 翻訳完了
- システム内更新日: 2026-10-03 02:01:42.138325
- Title: Certified Compilation in the TELEPERM XS Nuclear Safety I&C Platform
- Title（参考訳）: TELEPERM XS核安全I&Cプラットフォームにおける認証コンパイル
- Abstract要約: Framatomeが確立したTELEPERM XS(TXS Core)製品ファミリは、これらすべてのアプリケーションをカバーするデジタルI&Cシステムプラットフォームである。
ソフトウェア生産ツールチェーンの異なる段階における検証の役割を説明し、形式的なコンパイルプロセスに注目し、製品の安全ケースに対するCompCert認定コンパイラの貢献について議論する。
- 参考スコア（独自算出の注目度）: 47.887181993435824
- License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
- Abstract: The large safety instrumentation & control (I&C) systems in civil nuclear power plants (NPPs) are mainly safe-shutdown systems (reactor protection) or limitation and control systems. Framatome's established TELEPERM XS (TXS Core) product family is a digital I&C system platform to cover all these applications. We illustrate the role of verification in the different stages of the software production toolchain, focus on the formal compilation process, and discuss the contribution of the CompCert certified compiler to the safety case of the product. Scrutinizing the object code produced by this compiler has exhibited suboptimal run-time performance in a certain simple but recurring generated code pattern. We explain how formal methods allow us to address this issue in the compiler while simultaneously reducing its trusted computing base (TCB), thereby strengthening the safety case rather than merely preserving it.
- Abstract（参考訳）: 原子力発電所(NPP)の安全装置制御システム(I&C)は主に安全シャットダウンシステム(リアクター保護)または制限制御システムである。
Framatomeが確立したTELEPERM XS(TXS Core)製品ファミリは、これらすべてのアプリケーションをカバーするデジタルI&Cシステムプラットフォームである。
ソフトウェア生産ツールチェーンの異なる段階における検証の役割を説明し、形式的なコンパイルプロセスに注目し、製品の安全ケースに対するCompCert認定コンパイラの貢献について議論する。
このコンパイラによって生成されたオブジェクトコードを精査すると、特定の単純だが繰り返し発生するコードパターンで、最適以下の実行時間性能を示す。
本稿では,形式的手法によってコンパイラのこの問題に対処できると同時に,信頼性の高い計算基盤(TCB)を同時に削減し,単に保存するのではなく,安全性を向上する方法について説明する。
関連論文リスト
- HazardAuditor: From Executable Threats to Safer Computer-Use Agents [50.06351661912873]
既存のガードモデルは静的なプロンプトと応答をターゲットとしている。
既存の安全プラットフォームは、正規化された監督ではなく、ガードモデルで学ぶ必要がある評価判断を生成する。
両ギャップを埋める実行基盤フレームワークであるHazardAuditorを紹介します。
論文 参考訳（メタデータ） (2026-09-14T07:09:33Z) - RealSec-bench: A Benchmark for Evaluating Secure Code Generation in Real-World Repositories [58.32028251925354]
LLM(Large Language Models)は、コード生成において顕著な能力を示しているが、セキュアなコードを生成する能力は依然として重要で、未調査の領域である。
我々はRealSec-benchを紹介します。RealSec-benchは、現実世界の高リスクなJavaリポジトリから慎重に構築されたセキュアなコード生成のための新しいベンチマークです。
論文 参考訳（メタデータ） (2026-01-30T08:29:01Z) - A.S.E: A Repository-Level Benchmark for Evaluating Security in AI-Generated Code [49.009041488527544]
A.S.Eは、AI生成コードのセキュリティを評価するためのリポジトリレベルの評価ベンチマークである。
現在の大規模言語モデル(LLM)は、セキュアなコーディングに苦戦している。
大きな推論予算は、必ずしもより良いコード生成につながるとは限らない。
論文 参考訳（メタデータ） (2025-08-25T15:11:11Z) - CyFence: Securing Cyber-Physical Controllers via Trusted Execution Environment [45.86654759872101]
サイバー物理システム(CPS)は、サイバー攻撃により多くの負荷を掛けて、技術進化と接続性の向上を経験してきた。
セマンティックチェックを追加することで,サイバー攻撃に対する閉ループ制御システムのレジリエンスを向上させる新しいアーキテクチャであるCyFenceを提案する。
我々はCyFenceをアクティブブレーキデジタルコントローラからなる実世界のアプリケーションとして評価し、異なるタイプの攻撃を無視可能なオーバーヘッドで軽減できることを実証した。
論文 参考訳（メタデータ） (2025-06-12T12:22:45Z) - HOACS: Homomorphic Obfuscation Assisted Concealing of Secrets to Thwart Trojan Attacks in COTS Processor [0.6874745415692134]
ハードウェアトロイの木馬に対する秘密資産の機密性を確保するためのソフトウェア指向の対策を提案する。
提案したソリューションは、サプライチェーンエンティティを信頼する必要はなく、IC設計の分析や修正を必要としない。
我々は,AES(Advanced Encryption Standard)プログラムで秘密鍵を保護するために提案手法を実装し,詳細なセキュリティ分析を行った。
論文 参考訳（メタデータ） (2024-02-15T04:33:30Z) - SECOMP: Formally Secure Compilation of Compartmentalized C Programs [2.5553752304478574]
C言語の未定義の動作は、しばしば破壊的なセキュリティ脆弱性を引き起こす。
本稿では,機械チェックによるC言語のコンパイラSECOMPを紹介する。
このような強い基準が主流のプログラミング言語で証明されたのは、これが初めてです。
論文 参考訳（メタデータ） (2024-01-29T16:32:36Z) - HasTEE+ : Confidential Cloud Computing and Analytics with Haskell [50.994023665559496]
信頼性コンピューティングは、Trusted Execution Environments(TEEs)と呼ばれる特別なハードウェア隔離ユニットを使用して、コテナントクラウドデプロイメントにおける機密コードとデータの保護を可能にする。
低レベルのC/C++ベースのツールチェーンを提供するTEEは、固有のメモリ安全性の脆弱性の影響を受けやすく、明示的で暗黙的な情報フローのリークを監視するための言語構造が欠如している。
私たちは、Haskellに埋め込まれたドメイン固有言語(cla)であるHasTEE+を使って、上記の問題に対処します。
論文 参考訳（メタデータ） (2024-01-17T00:56:23Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。