論文の概要: 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コンパイラに拡張するために必要な,いくつかの証明工学のノベルティを含む,より大規模なセキュアなコンパイル証明の要素として使用する。
関連論文リスト
- RobustGEC: Robust Grammatical Error Correction Against Subtle Context
Perturbation [64.2568239429946]
本稿では,GECシステムのコンテキストロバスト性を評価するためのベンチマークであるRobustGECを紹介する。
現状のGECシステムには, 文脈摂動に対する十分な堅牢性がないことが明らかとなった。
論文 参考訳(メタデータ) (2023-10-11T08:33:23Z) - Certifying LLM Safety against Adversarial Prompting [75.19953634352258]
大規模言語モデル(LLM)は、入力プロンプトに悪意のあるトークンを追加する敵攻撃に対して脆弱である。
我々は,認証された安全保証とともに,敵のプロンプトを防御する最初の枠組みである消去・チェックを導入する。
論文 参考訳(メタデータ) (2023-09-06T04:37:20Z) - HDCC: A Hyperdimensional Computing compiler for classification on
embedded systems and high-performance computing [58.720142291102135]
この研究は、HDC分類メソッドの高レベルな記述を最適化されたCコードに変換する最初のオープンソースコンパイラである、ネームコンパイラを紹介している。
nameは現代のコンパイラのように設計されており、直感的で記述的な入力言語、中間表現(IR)、再ターゲット可能なバックエンドを備えている。
これらの主張を裏付けるために,HDC文献で最もよく使われているデータセットについて,HDCCを用いて実験を行った。
論文 参考訳(メタデータ) (2023-04-24T19:16:03Z) - 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) - Flexible Correct-by-Construction Programming [2.8798933523190327]
CbC と CbC-Block と TraitCbC を比較した。
CbCは、ソフトウェアを構造化されたインクリメンタルな方法で開発することで、正確性を保証する。
我々は、CbCと同様のプログラミングガイドラインを両方のアプローチで提供し、十分に構造化されたプログラムへと導く。
論文 参考訳(メタデータ) (2022-11-28T12:28:38Z) - Securing Optimized Code Against Power Side Channels [1.589424114251205]
セキュリティエンジニアは、コンパイラの最適化をオフにしたり、ローカルでコンパイル後の変換を実行することで、コードの効率を犠牲にすることが多い。
本稿では,最適化されたセキュアなコードを生成する制約ベースのコンパイラであるSecConCGを提案する。
論文 参考訳(メタデータ) (2022-07-06T12:06:28Z) - 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) - Configuring Test Generators using Bug Reports: A Case Study of GCC
Compiler and Csmith [2.1016374925364616]
本稿では,バグレポートのコードスニペットを使用して,テスト生成のガイドを行う。
GCCの8つのバージョンでこのアプローチを評価します。
我々は,本手法がGCCの最先端テスト生成技術よりも高いカバレッジを提供し,誤コンパイル障害を引き起こすことを発見した。
論文 参考訳(メタデータ) (2020-12-19T11:25:13Z) - Extending C++ for Heterogeneous Quantum-Classical Computing [56.782064931823015]
qcorはC++とコンパイラの実装の言語拡張で、異種量子古典プログラミング、コンパイル、単一ソースコンテキストでの実行を可能にする。
我々の研究は、量子言語で高レベルな量子カーネル(関数)を表現できる、第一種C++コンパイラを提供する。
論文 参考訳(メタデータ) (2020-10-08T12:49:07Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト(すべての情報・翻訳含む)の品質を保証せず、本サイト(すべての情報・翻訳含む)を使用して発生したあらゆる結果について一切の責任を負いません。