Fugu-MT 論文翻訳(概要): StarMalloc: A Formally Verified, Concurrent, Performant, and Security-Oriented Memory Allocator

論文の概要: StarMalloc: A Formally Verified, Concurrent, Performant, and Security-Oriented Memory Allocator

arxiv url: http://arxiv.org/abs/2403.09435v1
Date: Thu, 14 Mar 2024 14:29:01 GMT
ステータス: 処理完了
システム内更新日: 2024-03-17 13:28:07.653111
Title: StarMalloc: A Formally Verified, Concurrent, Performant, and Security-Oriented Memory Allocator
Title（参考訳）: StarMalloc: 形式的検証,コンカレント,パフォーマンス,セキュリティ指向メモリアロケータ
Authors: Antonin Reitz, Aymeric Fromherz, Jonathan Protzenko,
Abstract要約: 本稿では,より効率的な検証を可能にするために,依存型とモジュール抽象に依存したStarMallocの特定と検証方法を示す。 StarMallocはFirefoxブラウザを含む現実世界のプロジェクトで使用でき、10の最先端メモリアロケータに対して評価することができる。
参考スコア（独自算出の注目度）: 3.7554217682190365
License: http://creativecommons.org/licenses/by-nc-sa/4.0/
Abstract: In this work, we present StarMalloc, a verified, security-oriented, concurrent memory allocator that can be used as a drop-in replacement in real-world projects. Using the Steel separation logic framework, we show how to specify and verify StarMalloc, relying on dependent types and modular abstractions to enable efficient verification. As part of StarMalloc, we also develop several generic datastructures and proof libraries directly reusable in future systems verification projects. We finally show that StarMalloc can be used with real-world projects, including the Firefox browser, and evaluate it against 10 state-of-the-art memory allocators, demonstrating its competitiveness.
Abstract（参考訳）: 本稿では,セキュリティ指向の並列メモリアロケータであるStarMallocについて紹介する。スチール分離論理フレームワークを用いて、より効率的な検証を可能にするために、依存型とモジュール抽象に依存したStarMallocの特定と検証方法を示す。 StarMallocの一部として、将来のシステム検証プロジェクトで直接再利用可能ないくつかの汎用データ構造と証明ライブラリも開発しています。最終的に、StarMallocはFirefoxブラウザを含む現実世界のプロジェクトで使用でき、10の最先端メモリアロケータに対して評価でき、その競争力を示している。

関連論文リスト

SJMalloc: the security-conscious, fast, thread-safe and memory-efficient heap allocator [0.0]
ヒープベースのエクスプロイトは、アプリケーションのセキュリティに重大な脅威をもたらす。強化アロケータは現実世界のアプリケーションでは広く採用されていない。 SJMallocは、ヒープ上のアプリケーションのデータから離れて、そのメタデータを帯域外で保存する。 SJMallocは、GLibcsアロケータに比べて6%パフォーマンスが向上し、わずか5%のメモリしか使用していない。
論文参考訳（メタデータ） (2024-10-23T14:47:12Z)
Host-Based Allocators for Device Memory [1.2289361708127877]
割り当てアルゴリズムはホストメモリ上で実行されるが、デバイスメモリを割り当てるので、アロケータはアロケータが割り当てているメモリを読み取ることができない。これはつまり,ほぼすべてのアロケーションアルゴリズムにおいて,ユビキタスな概念である境界タグを使用できない,ということです。本稿では,この制約を回避するための代替アルゴリズムを提案する。
論文参考訳（メタデータ） (2024-05-11T19:28:37Z)
SeMalloc: Semantics-Informed Memory Allocator [18.04397502953383]
UAF(Use-after-free)は、メモリアンセーフ言語において重要な問題である。ヒープオブジェクトに関するより多くのセマンティクスをアロケータに渡すことで、トリニティをバランスさせる方法の1つを示します。 SeMallocでは、同じコールサイトから割り当てられたヒープオブジェクトと、同じ関数呼び出しスタックを介して、仮想メモリアドレスを共有することができる。
論文参考訳（メタデータ） (2024-02-02T21:02:15Z)
UniRef++: Segment Every Reference Object in Spatial and Temporal Spaces [92.52589788633856]
単一のアーキテクチャで4つの参照ベースのオブジェクトセグメンテーションタスクを統合するために、UniRef++を提案する。統一された設計により、UniRef++は幅広いベンチマークで共同でトレーニングすることができ、実行時に柔軟に複数のタスクを完了させることができる。提案する UniRef++ は RIS と RVOS の最先端性能を実現し,パラメータ共有ネットワークを用いて FSS と VOS の競合性能を実現する。
論文参考訳（メタデータ） (2023-12-25T12:54:11Z)
rCanary: Detecting Memory Leaks Across Semi-automated Memory Management Boundary in Rust [4.616001680122352]
Rustはコンパイル時の検証を通じてメモリ安全性を保証するシステムプログラミング言語である。本稿では,半自動境界を越えたリークを検出する静的,非自動,完全自動モデルチェッカーであるrCanaryを提案する。
論文参考訳（メタデータ） (2023-08-09T08:26:04Z)
MeMOT: Multi-Object Tracking with Memory [97.48960039220823]
私たちのモデルはMeMOTと呼ばれ、トランスフォーマーベースの3つの主要モジュールで構成されています。 MeMOTは広く採用されているMOTデータセット上で非常に競争力のあるパフォーマンスを観測する。
論文参考訳（メタデータ） (2022-03-31T02:33:20Z)
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)
Robust Object Detection via Instance-Level Temporal Cycle Confusion [89.1027433760578]
物体検出器の分布外一般化を改善するための補助的自己監視タスクの有効性を検討する。最大エントロピーの原理に触発されて,新しい自己監督タスクであるインスタンスレベル時間サイクル混乱(cycconf)を導入する。それぞれのオブジェクトに対して、タスクは、ビデオ内の隣接するフレームで最も異なるオブジェクトの提案を見つけ、自己スーパービジョンのために自分自身にサイクルバックすることです。
論文参考訳（メタデータ） (2021-04-16T21:35:08Z)
Efficient Regional Memory Network for Video Object Segmentation [56.587541750729045]
半教師付きVOS(Regional Memory Network, RMNet)のための新しいローカル-ローカルマッチングソリューションを提案する。提案するrmnetは、メモリとクエリフレームの両方における類似オブジェクトのあいまいさを効果的に緩和する。実験結果から,提案したRMNetは,DAVISおよびYouTube-VOSデータセットの最先端手法に対して良好に動作することが示された。
論文参考訳（メタデータ） (2021-03-24T02:08:46Z)
Kanerva++: extending The Kanerva Machine with differentiable, locally block allocated latent memory [75.65949969000596]
エピソディックメモリとセマンティックメモリは、人間のメモリモデルの重要なコンポーネントです。我々は、エピソードメモリとセマンティックメモリのギャップを埋める新しい原理ベイズメモリ割り当てスキームを開発しました。この割り当て方式がメモリ条件画像生成の性能を向上させることを実証する。
論文参考訳（メタデータ） (2021-02-20T18:40:40Z)
DMV: Visual Object Tracking via Part-level Dense Memory and Voting-based Retrieval [61.366644088881735]
DMVと呼ばれる部分レベル高密度メモリと投票ベースの検索による新しいメモリベースのトラッカーを提案する。また,メモリの信頼できない情報をフィルタリングする新たな投票機構を提案する。
論文参考訳（メタデータ） (2020-03-20T10:05:30Z)

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