[Paper] 嵌入式系统的相关 HAL 接口需求

Source: arXiv - 2512.14514v1

概述

嵌入式软件通常通过 Hardware Abstraction Layer (HAL) 与硬件交互。当 HAL 被误用时，硬件可能表现出不可预测的行为，导致昂贵的系统崩溃甚至物理损坏。本文形式化了 what HAL 需求对于避免此类故障真正关键，并展示了如何使用模型检查自动证明这些需求的相关性，以真实的 SPI‑bus 错误报告作为测试平台。

关键贡献

• “相关性” 的正式定义 用于 HAL 接口需求，基于安全关键的故障预防。
• 基于模型检查的证明技术，能够将需求认证为 无可争议 的相关性。
• 自动化提取流水线，将问题报告数据（例如 bug 单）转换为候选 HAL 需求。
• 案例研究验证，针对涉及 Linux spidev HAL 的三个真实 SPI 总线 bug，展示可行性。
• 新优先级划分范式的路线图，侧重于防止硬件引发的故障，而非通用缺陷分流。

方法论

1. 需求建模 – 作者将 HAL API 合约（前置/后置条件、使用模式）编码为逻辑规范。
2. 故障场景提取 – 从问题报告中识别导致硬件故障的具体 API 调用序列。
3. 相关性形式化 – 如果在假设该需求成立的情况下，故障场景在系统模型中变得不可达，则该需求为相关的。
4. 软件模型检查 – 使用符号模型检查器（例如 CBMC 或 CPAchecker），自动探索所有可能的程序路径。检查器尝试找到一个反例，使得故障在不违反候选需求的情况下发生。如果不存在此类反例，则该需求被证明是相关的。
5. 迭代剪枝 – 通过对每个候选需求重复上述过程，获得一组可证明相关的最小需求集合。

该流水线刻意保持轻量：它基于现有源代码和 bug 报告工作，仅需适度的注释工作。

结果与发现

• 对于三个 SPI‑bus bug，每个 bug 的分析都确定了 一到两个 HAL 要求（例如 “在任何传输之前必须配置 SPI 时钟”），当这些要求被强制执行时，数学上可以保证观察到的故障不再发生。
• 模型检查步骤在普通笔记本电脑上每个要求只需 几秒到几分钟 即可完成，表明该技术能够扩展到中小型嵌入式代码库。
• 提取出的相关要求与开发者的直觉相吻合，确认了形式化的相关性概念与实际安全关注点相匹配。

实际意义

• Prioritised Testing & Code Review – 团队可以将 QA 资源集中在少数对硬件安全最关键的 HAL 合约上，而不是把精力分散到所有 API 文档。
• Automated Guard Generation – 一旦需求被证明是相关的，开发者即可自动生成运行时断言或静态分析规则来强制执行该需求，从而在 CI 流水线中及早捕获误用。
• Regulatory Compliance – 安全关键领域（汽车、航空、医疗设备）通常需要证明关键接口被正确使用；形式化的相关性证明为审计提供了具体的可交付成果。
• Issue‑Report Mining – 提取步骤表明，现有的缺陷跟踪系统可以被重新用于驱动面向安全的需求工程，从而减少对单独规格文档的需求。

限制与未来工作

• Scalability – 当前评估仅限于小型 SPI 示例；更大的 HAL（具有数十个 API）可能导致模型检查中的状态空间爆炸。
• Annotation Overhead – 必须手动提供准确的前置/后置条件，这对遗留代码来说容易出错。
• Dynamic Hardware Effects – 该模型抽象了与时序相关的故障（例如总线争用），这些故障同样可能是安全关键的。

未来的研究方向包括将该方法与 symbolic execution 相结合，以处理更大的代码库，扩展相关性概念以涵盖 timing and concurrency constraints，以及构建能够自动从源码仓库提取并注释 HAL 合约的 tooling。

作者

• Manuel Bentele
• Andreas Podelski
• Axel Sikora
• Bernd Westphal

论文信息

• arXiv ID: 2512.14514v1
• 类别: cs.LO, cs.SE
• 发表时间: 2025年12月16日
• PDF: 下载 PDF