paperbot · PL 论文追踪

全部论文 待读 收藏

P2 Safe Low-Level Code Without Overhead is Practical

无运行时开销的安全底层代码是可行的
ICSE 2023 IEEE/ACM 45th International Conference on Software Engineering (ICSE)2023匹配度 2/10 · 论文关注类型系统与低层代码安全，属于纯 PL 领域，与用户核心的 PL 与 AI/LLM 交叉方向（如静态分析用于 ML/Agent、LLM 改进静态分析、浮点/贝叶斯程序分析）无直接关联。引用 1 inbox
Solal Pirelli, George Candea
类型系统语言设计与特性
crossref: 2026-09-12dblp: 2026-09-12

AI 速览

一句话：通过类型不变式证明潜在不安全操作的安全性，实证表明 Rust、C# 与 Ada 可无运行时开销实现安全网络设备驱动。

底层系统代码开发者出于性能考虑常使用不安全的编程语言，由此引入安全语言本可避免的缺陷与漏洞。本文主张，借助类型不变式（type invariants）证明潜在不安全操作的安全性，可以在不引入运行时开销的前提下获得安全性。作者从实证角度出发，将这类特性扩展到 Rust 与 C# 中，用它们实现安全的网络设备驱动，并确认运行时无额外开销；同时指出 Ada 语言已经内建了这些特性。该工作说明安全与性能在低层系统编程中并非必然取舍，为在现有语言中引入零开销安全机制提供了可行路径。

问题
开发者因性能顾虑使用不安全语言编写底层系统代码，由此产生安全语言本可避免的 bug 与漏洞。
方法
提出用类型不变式证明潜在不安全操作的安全性，从而在不引入运行时开销的情况下保障安全；并在 Rust 与 C# 中扩展此类特性，同时考察 Ada 的既有机制。
评估
通过实证用扩展后的 Rust 与 C# 实现安全的网络设备驱动，验证其运行时不产生额外开销；并确认 Ada 已具备这些特性。
原文摘要（Abstract）

Developers write low-level systems code in unsafe programming languages due to performance concerns. The lack of safety causes bugs and vulnerabilities that safe languages avoid. We argue that safety without run-time overhead is possible through type invariants that prove the safety of potentially unsafe operations. We empirically show that Rust and C# can be extended with such features to implement safe network device drivers without run-time overhead, and that Ada has these features already.

链接与引用

DOI 原文 · PDF（开放获取） · DBLP

BibTeX 
@inproceedings{PirelliC23,
  title = {Safe Low-Level Code Without Overhead is Practical},
  author = {Solal Pirelli and George Candea},
  booktitle = {ICSE},
  year = {2023},
  doi = {10.1109/icse48619.2023.00183}
}