論文の概要: SECOMP: Formally Secure Compilation of Compartmentalized C Programs
- arxiv url: http://arxiv.org/abs/2401.16277v3
- Date: Tue, 23 Apr 2024 15:39:39 GMT
- ステータス: 処理完了
- システム内更新日: 2024-04-24 19:16:06.711822
- Title: SECOMP: Formally Secure Compilation of Compartmentalized C Programs
- Title（参考訳）: SECOMP: Cプログラムの形式的セキュアコンパイル
- Authors: Jérémy Thibault, Roberto Blanco, Dongjae Lee, Sven Argo, Arthur Azevedo de Amorim, Aïna Linn Georges, Catalin Hritcu, Andrew Tolmach,
- Abstract要約: C言語の未定義の動作は、しばしば破壊的なセキュリティ脆弱性を引き起こす。
本稿では,機械チェックによるC言語のコンパイラSECOMPを紹介する。
このような強い基準が主流のプログラミング言語で証明されたのは、これが初めてです。
- 参考スコア（独自算出の注目度）: 2.5553752304478574
- License: http://creativecommons.org/licenses/by/4.0/
- Abstract: Undefined behavior in C often causes devastating security vulnerabilities. One practical mitigation is compartmentalization, which allows developers to structure large programs into mutually distrustful compartments with clearly specified privileges and interactions. In this paper we introduce SECOMP, a compiler for compartmentalized C code that comes with machine-checked proofs guaranteeing that the scope of undefined behavior is restricted to the compartments that encounter it and become dynamically compromised. These guarantees are formalized as the preservation of safety properties against adversarial contexts, a secure compilation criterion similar to full abstraction, and this is the first time such a strong criterion is proven for a mainstream programming language. To achieve this we extend the languages of the CompCert verified C compiler with isolated compartments that can only interact via procedure calls and returns, as specified by cross-compartment interfaces. We adapt the passes and optimizations of CompCert as well as their correctness proofs to this compartment-aware setting. We then use compiler correctness as an ingredient in a larger secure compilation proof that involves several proof engineering novelties, needed to scale formally secure compilation up to a C compiler.
- Abstract（参考訳）: C言語の未定義の動作は、しばしば破壊的なセキュリティ脆弱性を引き起こす。
これは、開発者が大きなプログラムを、明確に指定された特権と相互作用を持つ相互に不確実なコンパートメントに構成できるものである。
本稿では,非定義な動作のスコープが,それに遭遇して動的に妥協するコンパートメントに制限されることを保証する,マシンチェックされた証明が付属する,コンパートナライズドCコードのコンパイラであるSECOMPを紹介する。
これらの保証は、敵の文脈に対する安全性の保存として形式化され、完全な抽象化に類似したセキュアなコンパイル基準が、主流プログラミング言語でこのような強い基準が証明されたのはこれが初めてである。
これを達成するために、クロスコンパートメントインターフェースによって指定されたように、プロシージャコールとリターンを介してのみ対話できる分離されたコンパートメントでCompCert検証されたCコンパイラの言語を拡張します。
我々は、CompCertのパスと最適化、およびそれらの正当性証明を、このコンパートメント対応の設定に適用する。
次に,コンパイラの正しさをCコンパイラに拡張するために必要な,いくつかの証明工学のノベルティを含む,より大規模なセキュアなコンパイル証明の要素として使用する。
関連論文リスト
- Context-aware Code Segmentation for C-to-Rust Translation using Large Language Models [1.8416014644193066]
大きな言語モデル(LLM)は、ルールベースのメソッドよりも自然で安全なコードを生成することで、この翻訳を自動化することを約束している。
大規模Cコードをコンパイル可能なRustコードに変換する際の成功率を改善するLLMベースの翻訳方式を提案する。
4キロのコードを含む20のベンチマークCプログラムの実験では、すべてのプログラムをコンパイル可能なRustコードに変換することに成功した。
論文 参考訳（メタデータ） (2024-09-16T17:52:36Z) - SNIP: Speculative Execution and Non-Interference Preservation for Compiler Transformations [0.15800607910450126]
投機的意味論に基づくコンパイラ変換における非干渉保存の問題に対処する。
我々は,すべてのソースプログラムに対して一様に保存を保証できる検証方法を開発した。
論文 参考訳（メタデータ） (2024-07-21T07:30:30Z) - FoC: Figure out the Cryptographic Functions in Stripped Binaries with LLMs [54.27040631527217]
削除されたバイナリの暗号関数を抽出するFoCと呼ばれる新しいフレームワークを提案する。
FoC-BinLLMは、ROUGE-LスコアでChatGPTを14.61%上回った。
FoC-Simは52%高いRecall@1で過去のベストメソッドを上回っている。
論文 参考訳（メタデータ） (2024-03-27T09:45:33Z) - 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) - Secure Synthesis of Distributed Cryptographic Applications (Technical Report) [1.9707603524984119]
我々はセキュアなプログラムパーティショニングを用いて暗号アプリケーションを合成することを提唱する。
このアプローチは有望だが、そのようなコンパイラのセキュリティに関する公式な結果はスコープに限られている。
我々は、堅牢で効率的なアプリケーションに不可欠な微妙さを扱うコンパイラのセキュリティ証明を開発した。
論文 参考訳（メタデータ） (2024-01-06T02:57:44Z) - SOCI^+: An Enhanced Toolkit for Secure OutsourcedComputation on Integers [50.608828039206365]
本稿では,SOCIの性能を大幅に向上させるSOCI+を提案する。
SOCI+は、暗号プリミティブとして、高速な暗号化と復号化を備えた(2, 2)ホールドのPaillier暗号システムを採用している。
実験の結果,SOCI+は計算効率が最大5.4倍,通信オーバヘッドが40%少ないことがわかった。
論文 参考訳（メタデータ） (2023-09-27T05:19:32Z) - Online Safety Property Collection and Refinement for Safe Deep
Reinforcement Learning in Mapless Navigation [79.89605349842569]
オンラインプロパティのコレクション・リファインメント(CROP)フレームワークをトレーニング時にプロパティを設計するために導入する。
CROPは、安全でない相互作用を識別し、安全特性を形成するためにコストシグナルを使用する。
本手法をいくつかのロボットマップレスナビゲーションタスクで評価し,CROPで計算した違反量によって,従来のSafe DRL手法よりも高いリターンと低いリターンが得られることを示す。
論文 参考訳（メタデータ） (2023-02-13T21:19:36Z) - C-rusted: The Advantages of Rust, in C, without the Disadvantages [0.0]
C-rustedは、言語、システム、およびユーザ定義リソースのオーナシップ、排他性、共有性を表現するために(部分的に)Cプログラムに注釈を付けることができる革新的な技術である。
注釈付きCプログラムは、ISO Cコードを処理することができるコンパイルツールチェーンの修正されていないバージョンで変換することができる。
論文 参考訳（メタデータ） (2023-02-10T15:48:09Z) - CryptSan: Leveraging ARM Pointer Authentication for Memory Safety in
C/C++ [0.9208007322096532]
CryptSanは、ARM Pointer Authenticationに基づくメモリ安全性アプローチである。
M1 MacBook Proで動作するLLVMベースのプロトタイプ実装について紹介する。
これにより、構造化されていないライブラリとの相互運用性とメタデータに対する攻撃に対する暗号化保護が組み合わさって、CryptSanはC/C++プログラムにメモリ安全性を適合させる実行可能なソリューションとなる。
論文 参考訳（メタデータ） (2022-02-17T14:04:01Z) - Towards Robustness Against Natural Language Word Substitutions [87.56898475512703]
単語置換に対するロバスト性は、意味論的に類似した単語を置換として、明確に定義され広く受け入れられる形式である。
従来の防衛方法は、$l$-ball または hyper-rectangle を用いてベクトル空間における単語置換をキャプチャする。
論文 参考訳（メタデータ） (2021-07-28T17:55:08Z) - Extending C++ for Heterogeneous Quantum-Classical Computing [56.782064931823015]
qcorはC++とコンパイラの実装の言語拡張で、異種量子古典プログラミング、コンパイル、単一ソースコンテキストでの実行を可能にする。
我々の研究は、量子言語で高レベルな量子カーネル(関数)を表現できる、第一種C++コンパイラを提供する。
論文 参考訳（メタデータ） (2020-10-08T12:49:07Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。