論文の概要: Sockeye: a language for analyzing hardware documentation
- arxiv url: http://arxiv.org/abs/2510.27485v1
- Date: Fri, 31 Oct 2025 14:04:01 GMT
- ステータス: 翻訳完了
- システム内更新日: 2025-11-03 17:52:16.121382
- Title: Sockeye: a language for analyzing hardware documentation
- Title（参考訳）: Sockeye: ハードウェアドキュメンテーションを解析するための言語
- Authors: Ben Fiedler, Samuel Gruetter, Timothy Roscoe,
- Abstract要約: ハードウェアのセマンティクス、ソフトウェア動作に関する仮定、および所望のセキュリティ特性を記述するためのドメイン固有言語を導入する。
次に、参照マニュアルから8つのSystem-on-Chipsの多様なセットのマシン仕様を作成します。
- 参考スコア（独自算出の注目度）: 0.2142042364864257
- License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
- Abstract: Systems programmers have to consolidate the ever growing hardware mess present on modern System-on-Chips (SoCs). Correctly programming a multitude of components, providing functionality but also security, is a difficult problem: semantics of individual units are described in English prose, descriptions are often underspecified, and prone to inaccuracies. Rigorous statements about platform security are often impossible. We introduce a domain-specific language to describe hardware semantics, assumptions about software behavior, and desired security properties. We then create machine-readable specifications for a diverse set of eight SoCs from their reference manuals, and formally prove their (in-)security. In addition to security proofs about memory confidentiality and integrity, we discover a handful of documentation errors. Finally, our analysis also revealed a vulnerability on a real-world server chip. Our tooling offers system integrators a way of formally describing security properties for entire SoCs, and means to prove them or find counterexamples to them.
- Abstract（参考訳）: システムプログラマは、現代のSystem-on-Chips (SoCs) に存在するハードウェアの混乱をさらに強化する必要がある。
個々の単位のセマンティクスは英語の散文で記述され、説明はしばしば不特定であり、不正確なものになりがちである。
プラットフォームのセキュリティに関する厳格な発言は、しばしば不可能です。
ハードウェアのセマンティクス、ソフトウェア動作に関する仮定、および所望のセキュリティ特性を記述するためのドメイン固有言語を導入する。
次に、参照マニュアルから8つのSOCの多様なセットのマシン可読仕様を作成し、その(内部)セキュリティを正式に証明します。
メモリの機密性と整合性に関するセキュリティ証明に加えて、いくつかのドキュメンテーションエラーを発見します。
最後に、我々の分析は現実世界のサーバーチップの脆弱性も明らかにした。
当社のツールは,システムインテグレータに対して,SoC全体のセキュリティプロパティを正式に記述する手段を提供しています。
関連論文リスト
- What You Code Is What We Prove: Translating BLE App Logic into Formal Models with LLMs for Vulnerability Detection [20.200451226371097]
本稿では,BLEアプリケーションセキュリティ分析を意味翻訳問題として再編成する。
脆弱性を直接検出するのではなく、トランスレータとして機能するために、大きな言語モデル(LLM)を活用しています。
静的解析,プロンプト誘導型LLM翻訳,シンボル検証を組み合わせたシステムであるVerifiaBLEで,このアイデアを実装した。
論文 参考訳（メタデータ） (2025-09-11T09:27:37Z) - Not quite a piece of CHERI-cake: Are new digital security by design architectures usable? [0.8594140167290099]
CHERIはバッファオーバーフローやメモリ安全性のエラーを恐れずにプログラムできる。
私たちは、CHERIの警告とエラーの表示と、さまざまなドキュメントの欠如に、開発者が苦労していることに気付きました。
論文 参考訳（メタデータ） (2025-06-30T10:04:14Z) - CRUST-Bench: A Comprehensive Benchmark for C-to-safe-Rust Transpilation [51.18863297461463]
CRUST-Benchは100のCリポジトリのデータセットで、それぞれが安全なRustとテストケースで手書きのインターフェースとペアリングされている。
我々は、このタスクで最先端の大規模言語モデル(LLM)を評価し、安全で慣用的なRust生成が依然として難しい問題であることを確認した。
最高のパフォーマンスモデルであるOpenAI o1は、ワンショット設定で15タスクしか解決できない。
論文 参考訳（メタデータ） (2025-04-21T17:33: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) - Guess & Sketch: Language Model Guided Transpilation [59.02147255276078]
学習されたトランスパイレーションは、手作業による書き直しやエンジニアリングの取り組みに代わるものだ。
確率的ニューラルネットワークモデル(LM)は、入力毎に可塑性出力を生成するが、正確性を保証するコストがかかる。
Guess & Sketch は LM の特徴からアライメントと信頼性情報を抽出し、意味的等価性を解決するためにシンボリック・ソルバに渡す。
論文 参考訳（メタデータ） (2023-09-25T15:42:18Z) - (Security) Assertions by Large Language Models [25.270188328436618]
セキュリティのためのハードウェアアサーション生成において,コード生成に新たな大規模言語モデル(LLM)を用いることを検討する。
我々は、人気のあるLCMに注目し、プロンプトの様々なレベルの詳細を考慮し、アサーションを箱から書き出す能力を特徴付ける。
論文 参考訳（メタデータ） (2023-06-24T17:44:36Z) - Dos and Don'ts of Machine Learning in Computer Security [74.1816306998445]
大きな可能性にもかかわらず、セキュリティにおける機械学習は、パフォーマンスを損なう微妙な落とし穴を引き起こす傾向がある。
我々は,学習ベースのセキュリティシステムの設計,実装,評価において共通の落とし穴を特定する。
我々は,落とし穴の回避や軽減を支援するために,研究者を支援するための実用的な勧告を提案する。
論文 参考訳（メタデータ） (2020-10-19T13:09:31Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。