用于通用软件组件自动适配的工程框架
- 2025-07-17 09:47:33

简介
在汽车领域,现代软件开发离不开可复用软件组件的运用。这类通用软件组件必须针对每个特定的目标应用进行配置和定制。如今,系统复杂度已达到这样一种程度:开发通用软件组件并为产品系列中的每个变体手动适配每个组件不仅容易出错,而且在经济上也不再可行。在本文中,我们提出了一种用于通用软件组件自动适配的工程框架,该框架侧重于时间和空间完整性。此框架围绕通用方法构建,并利用专门的软件工具来确定软件组件到嵌入式系统资源的分配,同时确保内存完整性。我们以在英飞凌 AURIX™ TC277 处理器上、在 AUTOSAR 操作系统下运行的四旋翼飞行器为例来阐释我们的方法。
1、引言
安全关键嵌入式系统是计算机控制系统中的一个特殊类别。其软件和硬件部分相互作用,实现复杂功能,如发动机控制或车辆导航。功能实现中未被检测到的错误可能危及人类生命,因此这类系统具有 “安全关键” 这一附加属性。在成本敏感且竞争激烈的市场中,正确实现必要的软件、满足所有安全要求并最大限度地提高硬件资源利用率,对现有的软件工程方法和工具构成了重大挑战。
微控制器能力不断增强的一个近期例子是嵌入式多核处理器,它包含多个且可能是异构的执行单元。为了充分发挥其潜力并最大限度地提高资源利用率,软件组件必须紧密集成,并针对每个硬件平台进行专门优化。这一优化步骤被称为适配,且通常通过手动方式进行。
随着越来越多的软件组件共享微控制器的公共资源,确保它们免受不必要的干扰至关重要,这是维持系统可靠性和安全性的必要条件。因此,适配工作需要确保紧密集成的软件组件之间实现隔离。这可以通过控制对内存和 CPU 时间的访问来实现,从而支持错误遏制。
1.1 问题陈述
当前,安全关键嵌入式系统的软件工程是以 “逐个项目” 的方式进行的。根据不同项目中系统架构的设置,可能需要将软件组件分布在微控制器网络中,或者在不同的微控制器衍生品上运行。遗憾的是,由于复杂性以及缺乏适当的工程工具,软件组件往往是为满足特定项目的需求而专门开发的。它们被手动分配到系统硬件架构的资源中,并手动适配以充分利用微控制器的功能。特别是对于安全关键系统,确保软件组件的隔离执行需要额外的配置和分析步骤,而这些步骤因微控制器而异,因此也常常通过手动方式进行。
虽然 “逐个项目” 的方法对于少量项目可能足够,但它仍然需要大量的手动工作,并且降低了软件组件的可复用性。随着安全关键设备中越来越多的控制功能通过软件实现,对不同硬件平台的可复用性和适应性的需求日益增加,这使得 “逐个项目” 的方法在经济上不再可持续。由此产生的问题是:如何以通用且可复用的方式开发安全关键嵌入式系统的软件组件,使其能够在多个项目中使用,同时又不降低资源利用率,也不损害其隔离特性和内存安全性。
1.2 总体方法
作者认为,通过基于模型开发通用软件组件,结合用于处理项目特定硬件特性和安全要求的自动适配工具包,可以显著提高软件组件的可复用性。
一般而言,软件组件涉及系统特定功能的实现。通过使用抽象层,可以以平台无关的方式开发这些组件,并将其组织为通用软件组件库,供以后在多个项目中使用。采用形式化和基于模型的开发方法后,这些通用功能能够自动定制和适配特定项目的需求。特别是,这种方法有助于将自动软件部署与自动平台特定代码生成以及隔离特性的自动配置和验证相结合。这种 “基于功能” 的软件开发并非全新概念。然而,作者认为,目前的实践水平和可用工具的能力尚未达到开发多平台安全关键嵌入式系统所需的成熟度。
1.3 贡献
在本文中,作者展示了一个联合研发项目的成果,该项目旨在构建一个工程框架,用于在安全关键嵌入式系统中使用通用软件组件。该框架整合了多个工具,以便通用软件组件能够适配特定的微控制器,并进行内存完整性分析。其共同起点是包含系统规范和功能架构的系统架构模型。此外,还需考虑有关目标硬件(微控制器系列)的附加信息以及通用软件组件库。这些规范通过通用交换格式在不同的工程工具和代码分析器之间传递。
具体而言,ASSIST 工具套件能够为目标硬件生成软件分配方案。通过纳入时序约束,它还能够构建静态调度表,从而确保系统设计的可行性。这会生成一个描述所有软件组件时空行为的操作系统配置。
结合生成的应用程序软件,使用 Astrée 对 C 源代码进行检查。通过消除分析过程中发现的内存和类型缺陷,可以在 C 代码级别确保内存完整性。此外,在分析步骤中收集有关数据和函数访问行为的信息。在最后一步中,cAMP 工具利用这些信息将数据和函数低级别映射到物理内存和保护区域。
最终成果包括带注释的应用程序代码和描述内存映射的链接脚本,它们保证满足所有项目特定的安全要求,并充分利用微控制器的功能。最终成果以及中间工作产品可在 GitHub上获取。使用该框架能够以高效且自动化的方式适配安全关键系统的通用应用程序软件,从而在不降低资源利用率或不危及系统安全的前提下实现软件复用。
2、概念概述
图 1 描绘了我们框架的简化工作流程。它基于严格的自顶向下工程方法与 “构造正确性” 方法相结合的理念],通过自动合成和验证关键工程制品为工程师提供支持。

图1:简化的工作流程
基于功能架构模型,系统工程师创建预期的系统架构模型。该模型包含从库中选择的通用软件组件以及特定项目的硬件平台。通过为所选软件组件构建部署方案,可以自动验证所选硬件平台是否满足特定项目的技术和安全相关要求(参见第 6 节)。如果找不到有效的部署方案,则需要修改硬件平台或软件组件的选择。然后,对所有软件代码应用可靠的语义代码分析,以确保足够的隔离性和内存保护,这两者对于确保系统的正确性至关重要(参见第 7 节)。最后,软件组件的数据和代码被自动映射到其微控制器的隔离分区(参见第 8 节)。
接下来的章节将更详细地描述框架的基本部分。然而,本文并非旨在详细描述框架中使用的每个工具,而是重点阐述它们在基于通用软件组件的自动化开发过程中的作用。
3、I4Copter
为了阐释我们的方法,我们将以 I4Copter 飞行控制器作为一个综合示例。I4Copter 是一个研究项目,其开发的四旋翼飞行器作为硬实时系统和控制系统的示例。虽然四旋翼飞行器软件最初打算部署到单核英飞凌 TriCore TC1796 处理器上,但在本文中我们使用 AURIX TC277,这是一款三核汽车微控制器。I4Copter 的控制软件由六个模块组成:一个用于读取传感器和远程输入的数字信号处理器(DSP)、一个两级控制器和三个观测器。所有这些模块负责在四旋翼飞行器起飞、飞行和着陆期间控制其定位。以下章节将提供 I4Copter 和目标硬件的更多细节,以描述它们与所提出框架的相关性。该示例系统在复杂性和规模上类似于汽车底盘系统中使用的控制系统。选择 AURIX TC277 是因为它是汽车领域广泛使用的微控制器。它还提供异构内存和计算单元,允许根据产品需求灵活自适应地部署软件,这使其成为软件平台驱动开发方法的合适目标平台。
4、平台开发
为了以可复用和结构化的方式开发应用程序软件组件,系统工程领域的实践现状建议从功能架构入手。功能架构是严格需求工程过程的结果,并且与其他系统视图存在关联。
功能架构与软件应用程序的逻辑意图和依赖关系紧密相关。它是一种特殊的抽象,通常不包含技术架构的细节。
将功能架构和技术架构分离,可以实现问题域与可能的技术解决方案变体之间的关注点分离。这种方法允许独立构建应用程序和基础设施软件,因为只要两端的实现都遵守公共接口的 “契约”,就可以分别开发它们。
在我们的案例中,这可以用图 2 所示的桥接模式来描述。桥接模式旨在将抽象与其实现解耦。功能元素描述抽象功能。而技术实现则是提供功能元素所描述功能的具体实现。功能元素无需了解具体实现,因此只要满足所有项目特定要求,技术实现就可以被其他解决方案替代。不过,功能视图和技术视图并非完全独立,因为任一视图的变更都可能对另一视图产生重大影响。

图2:功能元素和技术实现之间的关系显示了桥接模式
I4Copter 软件中的一个功能元素示例是用于减少传感器输入噪声的滤波器。提供该功能的技术实现可以是 α-β 滤波器、移动平均滤波器或卡尔曼滤波器。它们的软件模块必须提供公共接口,以使滤波器实现可互换。可以通过在编译时更改链接到应用程序代码中的模块来控制滤波算法的选择。
在每个项目中,系统工程师的任务是为每个功能元素选择合适的构建块,即从库中选择通用软件组件以及硬件组件(微控制器),以创建系统架构模型。当然,该模型需要满足功能架构提出的要求。
5、系统架构
我们方法的核心是系统架构模型。有多种符号可用于建模系统架构,例如 SysML、UML 或 AMALTHEA,它们允许将安全和时序相关要求表示为定义明确的一等模型元素。
一般而言,系统架构模型包括对具有不同资源需求的软件组件的描述、对可用硬件资源(如微控制器或内存)的描述,以及限制软件组件资源使用和分配的约束,特别是安全要求。
安全要求的示例包括需要检测软件组件计算中的偶发硬件缺陷、异构硬件执行环境或使用额外硬件实现错误校正 / 检测代码。这些要求转化为对系统架构的约束,从而限制了架构的解决方案空间。
6、部署
有了系统架构模型后,下一步是构建软件组件与硬件资源之间的映射。构建过程需要考虑所有可用资源的容量,例如闪存的大小。它还必须确保满足附加约束(时间和空间隔离)。这通过为所有软件组件构建可行的映射和静态周期性调度表来实现。由于解决方案空间的复杂性以及解决方案正确性的重要性,此过程通过 ASSIST 工具以自动化方式进行。通过将该问题转换为等效的约束满足问题并随后应用约束编程,来解决找到正确映射和可行静态调度表的挑战。已有针对安全关键系统的类似方法发表。
约束编程是指运筹学、离散优化和人工智能中的一组技术。这些技术有助于基于受约束影响的变量找到问题的解决方案(约束满足问题)。每个变量都有一个有限的整数域,每个约束都定义了这些变量子集的有效或无效解决方案。这类问题的解决方案可以通过结合搜索技术(包括回溯)和用于值消除的约束传播技术来获得。ASSIST 通过提供用户友好的领域特定语言来描述映射和调度问题,从而自动化此过程,并向用户隐藏形式规范的复杂性。
与其他基于具有丰富接口的组件组合的方法不同,ASSIST 在更高的抽象级别上工作,并将映射和调度视为单独的步骤,以减少每个步骤中的问题规模。为此,ASSIST 中组件属性的建模不太详细。软件任务被视为带有注释资源需求的 “黑盒”。ASSIST 还通过为包含所有任务周期性执行的单个超周期构建调度表,来简化调度问题的复杂性。在内部,ASSIST 使用 CHOCO SOLVER,该求解器已成功应用于各种调度问题。
图 3 包含英飞凌 AURIX TC277 微控制器的硬件属性规范。ASSIST 允许指定功能,如 FPU,以及容量,如闪存,以约束部署过程。

图3:ASSIST中的硬件规格
图 4 展示了软件架构的规范。它由六个应用程序及其任务组成。为了示例的简洁性和可读性,每个任务只需要一定量的处理器时间(在规范中称为 CoreUtilization)。核心利用率由任务的最坏情况执行时间(WCET)除以任务周期确定。例如,可以通过 aiT WCET 分析器为英飞凌 AURIX TC277 等时序可预测处理器计算 WCET 的安全上限。在非时序可预测的多核处理器上,WCET 估计可以由 TimeWeaver 等混合 WCET 分析器提供。任务 T2_EngineController 展示了任务如何要求处理核心的特定功能。

图4:ASSIST中的应用程序和任务
图 5 显示了 I4Copter 系统周期性任务的单个周期内不同任务之间的依赖关系。任务 T4_HeightObserver 和 T5_AltitudeObserver 可以并行运行,以充分利用 TC277 多核处理器的资源。

图5:任务依赖关系图
为了允许这两个任务并行执行,它们应部署到不同的核心。然而,这并不构成部署合成的硬约束,因为将这些任务部署到同一核心可能仍然可行,只是不太理想。因此,ASSIST 需要将 T4_HeightObserver 和 T5_AltitudeObserver 的并行执行信息视为实现优化解决方案的提示。为此,可以在 ASSIST 中指定任务图,该工具能够自动确定哪些任务可以并行运行,以便为部署导出优化提示。本文示例的任务图规范包含在图 6 中。

图6:ASSIST中的任务图规范
与 “软” 优化提示不同,还有 “硬” 部署约束,如与安全相关的约束,这些约束会影响结果的可行性和有效性。为了获得有效的部署,必须满足这些约束。对于示例用例,假设有两个附加安全要求,以确保在可能恶劣的环境条件下的可靠性。
1. 任务 T6_DSP 和 T3_AttitudeObserver 不得共享同一核心。
2. 任务 T6_DSP 和 T4_HeightObserver 不得共享同一核心。
图 7 展示了如何在 ASSIST 中将这些要求表示为 “硬” 映射约束。

图7:ASSIST中的映射约束规范
基于上述清单中描述的部署规范,ASSIST 能够确定所有有效的部署解决方案。存在 208 种不同的解决方案,在普通台式计算机上计算这些解决方案大约需要 250 毫秒。为了从有效解决方案集中找到 “最佳” 解决方案,ASSIST 允许对每个部署应用一组指标。这些指标能够为每个解决方案计算一个分数,该分数反映指标中所体现的优化目标的实现程度。因此,分数最高的解决方案被认为是 “最佳” 解决方案。
对于示例用例,针对应用程序任务的部署追求两个优化目标。最重要的是通过部署实现任务的并行执行。因此,如果任务图中的并行任务确实映射到不同的核心,解决方案应获得更高的排名。此外,核心负载均匀的映射解决方案比负载异构的解决方案更受青睐。图 8 展示了 ASSIST 中这些指标的选择。将 “最大并行度” 指标的权重设置为 2,可以表达第一个目标相对于第二个优化目标的重要性。使用上述指标进行的自动评估确定了两个得分最高的解决方案,我们从中选择了一个(见图 10)。

图8:解决方案评估
最后,ASSIST 生成 AUTOSAR-OS 配置文件,该文件构成我们工程框架后续步骤的核心工程制品。
7、操作系统配置和源代码的静态分析
本节讨论代码和数据的自动低级部署的先决条件,以提供内存处理和内存保护。
7.1 AUTOSAR-OS 系统模型
AUTOSAR 是不同汽车制造商之间的合作伙伴关系,旨在为嵌入式汽车操作系统设计标准。目前该标准有两个版本,适用于静态系统的 AUTOSAR Classic 和适用于动态系统的 AUTOSAR Adaptive。在本文中,我们仅参考 AUTOSAR Classic 系列操作系统。AUTOSAR 系统模型如图 9 所示。

图9:AUTOSAR隔离方案

图10:ASSIST找到的部署解决方案
该系统围绕在底层硬件的一个特定计算单元上执行的 OS - 应用程序构建。OS - 应用程序管理内存中的指令和数据,作为一个或多个任务的执行环境。任务本身是可调度的执行单元,每个任务都有自己的数据和堆栈段。通过使用基于硬件的内存访问保护,如内存保护单元(MPU),内核内存可以与 OS - 应用程序进行空间隔离。相同的机制还允许 OS - 应用程序之间以及 OS - 应用程序内部任务之间的空间隔离。这在图 9 中用粗黑线表示。
AUTOSAR 系统的静态结构,包括核心、OS - 应用程序、任务和内存保护区域的映射,以及调度和计时器事件,在配置文件中描述。所谓的 ARXML 文件以 AUTOSAR 标准化的 XML 格式编写。基于该文件,实现 AUTOSAR 标准的操作系统可以生成反映 ARXML 文件中描述的配置的操作系统代码。ASSIST 的输出就是这样一个 ARXML 文件,该文件又可被 Astrée 用于操作系统和应用程序代码的语义分析。
7.2 确保内存和类型安全
尽管所有软件组件都已成功部署,但仍需要解决内存和类型安全问题,以确保所有紧密集成的软件组件之间的空间隔离。在 C 编程语言范围内,内存安全定义为不存在触发未定义行为的内存访问,以及不存在并发线程在没有适当同步的情况下访问共享变量的数据竞争。尽管 C 编程语言本身不确保内存安全,但对 C 源代码的可靠静态分析能够在编程语言级别保证内存安全。
在我们的框架中,我们使用 Astrée 分析器。其主要目的是报告由 C99 标准规定的未指定和未定义行为引起的程序缺陷。报告的代码缺陷包括整数 / 浮点除以零、数组索引越界、错误的指针操作和 dereferencing(缓冲区溢出、空指针 dereferencing、悬空指针等)、数据竞争、锁定 / 解锁问题以及死锁。为了处理并发缺陷,Astrée 实现了低级并发语义,该语义提供了一种可扩展的可靠抽象,涵盖所有可能的线程交织。分析器考虑任务优先级,对于多核系统,还考虑任务到应用程序和核心的映射。表 1 展示了内存和类型安全与 Astrée 发现的缺陷之间的关系。Astrée 广泛应用于安全关键系统,并提供必要的工具资格支持,包括资格支持套件和资格软件生命周期数据报告。

表 1:类型和内存安全要求与 Astrée 告警类型的映射
ASSIST 在高级部署期间生成的 AUTOSAR-OS 配置文件由 Astrée 解析,以自动生成匹配的分析配置,该配置对各种任务和中断服务程序(ISRs)的异步执行进行建模。Astrée 返回潜在代码缺陷的列表。分析结果为零告警可保证 C 源代码中不存在内存安全违规。由于 C 语义假设堆栈空间无限,源代码级分析需要辅以二进制级的可靠静态堆栈使用分析,以证明不存在堆栈溢出。此外,使用经过形式验证的编译器可确保不会因错误编译引入内存安全缺陷。这些方法共同作用,能够防止软件引起的内存损坏,从而建立内存安全。
除了报告运行时错误和并发缺陷外,Astrée 还生成详细的数据和控制流报告。可靠性保证不会遗漏任何控制流路径或读写访问,即使在存在数据或函数指针访问或任务干扰的情况下也是如此。全局数据和控制流分析总结了程序执行过程中的变量访问和函数调用。
报告还包含每个实际共享变量、访问该变量的任务列表、任务所属的应用程序和核心,以及访问类型(读、写、读 / 写)。通过指针进行的间接变量访问以及函数指针调用目标都被充分考虑。过滤功能允许确定每个软件组件的控制和数据流,从而支持 DO-178C 要求的数据流和控制耦合分析。示例系统的数据流报告摘录如表 2 所示。请注意,Astrée 在我们的示例系统中检测到每个共享变量的数据竞争,这是预期的,因为代码中不包含任何同步机制。

表 2:Astrée 数据流报告摘录
8、内存映射
在完成系统定义、所有软件组件的部署以及内存安全分析之后,下一步是将所有指令及其数据低级映射到特定微控制器的物理内存。这一步骤也称为绑定。
8.1 异构内存
对于英飞凌 AURIX TC277 等具有异构内存的多核处理器,此任务尤为重要,以实现良好的运行时行为以及无干扰的空间隔离。AURIX TC277 提供六个核心耦合 SRAM,分别用于数据(DSPR)和指令(PSPR)、非易失性闪存(PMU)以及总线访问 SRAM(LMU)。可以使用微控制器的总线从任何核心访问任何内存。然而,来自耦合核心的核心耦合 SRAM 读写操作仅需一个 CPU 周期,而通过总线的内存访问则需要更多时间。此外,由于并发总线访问引起的干扰,通过总线的访问具有较低的确定性访问时间。闪存还配备了纠错功能,以确保数据完整性。
8.2 数据和函数类别
同时,数据和函数表现出诸如访问来源、访问类型、访问频率以及逻辑特性(如常量或用于系统内校准)等特征。这些特性的组合有助于将每个数据项或函数绑定到微控制器的不同内存。表现出相似特征的数据项和函数可以分组到变量和函数类别中,每个类别根据绑定策略有一组首选内存。在 I4Copter 示例中,存在两种正交的分类类型:任务级和核心级。任务本地数据和函数仅由单个任务访问,而任务全局数据由两个或多个任务访问。与此类似,核心本地数据和函数仅从单个核心访问,而核心全局数据和函数在不同核心之间共享。常量数据项被分组到不同类别,因为它们的只读属性使它们适合绑定到闪存,并依靠核心耦合缓存来减少访问时间。
8.3 绑定策略
绑定策略描述特定数据项或函数应映射到哪个内存,这取决于可用内存的属性以及变量和函数类别。
此类策略的一个示例是将任务本地、核心本地数据映射到核心耦合 SRAM,以实现最快的访问时间。另一个策略是将任务全局、核心全局数据映射到访问量最大的核心的核心耦合内存。由于这些内存的容量有限,需要决定先绑定哪些数据和函数。这可以通过优化策略来实现,从基于总访问频率的非常简单的策略(对读写操作使用不同权重)到使用约束求解问题或整数线性规划的复杂优化算法。
在本文介绍的 I4Copter 示例中,数据项按对其的读写总量排序。访问频率通过将 Astrée 报告的读写量乘以系统一个超周期(9 毫秒)内的任务激活量来确定。总访问次数较高的数据项优先映射。
8.4 自动内存映射
对于任意复杂度的系统,手动收集数据和函数特征信息、将其组合到类别中,然后创建到硬件内存的映射是不可行的。cAMP 工具通过自动生成指令和数据到内存的映射来解决此问题。为此,它使用先前开发步骤中的所有可用信息:ASSIST 的部署信息(通过考虑生成的 ARXML 文件中描述的部署解决方案);从 Astrée 提取的关于数据和函数特征的信息(通过考虑数据流报告(见表 2));以及系统规范中的要求,如任务时间、安全要求和约束。
cAMP 内聚合这些信息,并用于生成数据和函数到内存的绑定,以及为每个使用的内存段分配 MPU 强制的内存保护区域。绑定过程遵循所选硬件的绑定策略。此过程的结果是一个链接脚本,该脚本描述内存映射并公开配置系统 MPU 所需的段。
为了减少使用链接脚本所需的工作量(即,将各个变量和函数分配到各种内存段),cAMP 能够与代码生成工具接口,以自动在生成的代码中包含必要的注释。在当前形式下,cAMP 能够与 TargetLink 接口,TargetLink 是 MatLab/Simulink 中广泛使用的 C 代码生成器。
使用 cAMP 通过创建可重现的绑定过程,允许自动定制应用程序以适应特定硬件和内存布局。使用代码生成和基于平台的开发还带来了其他好处,如自动代码适配和可复用绑定策略。数据和代码的自动绑定显著减少了软件开发时间,同时比手动绑定更不易出错。
9、相关工作
我们框架的基本思想受到 KESO 和 Parnas 提出的程序家族的启发。Parnas 是最早思考程序家族和软件产品线(SPL)的人之一。他在操作系统的背景下描述了这个问题。基于他的思想,后来的方法研究了大型软件系统中的可变性挑战。例如,Sincero 等人研究了 Linux 内核,并通过配置分析将其视为 SPL。Liebig 等人研究了基于预处理器指令的可配置 C 语言组合软件,并探索了处理由此引发的复杂性的方法。还有一些解决方案使用生成式编程从可配置性模型创建程序变体。另一个利用程序家族思想的项目是名为 PURE 的操作系统构造工具包 [6]。作者定义了一组可复用的操作系统基础设施组件(如线程、调度、并发、中断或内存服务),用于构建基础设施服务。例如,可用于组合地址空间和进程的轻量级线程。作者采用基于配置和代码生成的框架来创建操作系统变体。与这些先前的工作不同,我们允许在设计早期阶段基于可复用应用部分的架构和代码分析技术来操纵空间和时间隔离属性,这些应用部分也可以使用基于模型的技术开发。
KESO Java 虚拟机提供了一种隔离概念,类似于通用操作系统中的进程概念。KESO 具有编译器,能够生成专门针对特定应用的虚拟机环境。因此,KESO 采用了 Parnas 方法的思想。下面我们描述与我们工作相关的 KESO 特征。空间隔离确保控制流只能访问其执行上下文所属保护区域(称为域)的数据区域内存。因此,每个数据块可以逻辑上分配给恰好一个域。在 Java 中,类型安全确保程序只能访问被赋予显式引用的内存区域;引用的类型还决定了程序访问引用所指向内存区域的方式。为了实现空间隔离,KESO 编译器强制引用值永远不会出现在多个域中。与 KESO 不同,我们的应用程序不是用 Java 开发的,而是使用基于模型的技术,其中生成的 C 代码通过抽象解释进行分析,以创建内存安全的 C 代码。我们扩展了 Astrée,使其使用 AUTOSAR OS 线程模型的信息,以便能够基于 OS - 应用程序执行流和上下文敏感分析,构建由内存保护硬件强制的逻辑隔离区域。
文章解决了与我们工作类似的问题,但假设了不同的通信模型。与 AUTOSAR 使用共享内存进行任务间通信不同,他们的通信模型基于 Kahn 进程网络,所使用的操作系统基于非共享内存模型。对于空间隔离,他们仅依靠 MPU 来确保动态故障遏制。相比之下,我们通过对集成源代码的可靠静态分析来通过构造增强安全性,并将 MPU 用作安全网。此外,高级部署不是他们工作流程的一部分,而是作为输入假设。
10、结论
作者展示了一个联合研发项目的成果,该项目旨在构建一个工程框架,用于在安全关键嵌入式系统中使用通用软件组件。该框架整合了多个工具,以便通用软件组件能够适配特定的微控制器,并进行内存完整性分析。其共同起点是包含系统规范和功能架构的系统架构模型。此外,还需考虑有关目标硬件(微控制器系列)的附加信息以及通用软件组件库。这些规范通过通用交换格式在不同的工程工具和代码分析器之间传递。
具体而言,ASSIST 工具套件能够为目标硬件生成软件分配方案。通过纳入时序约束,它还能够构建静态调度表,从而确保系统设计的可行性。这会生成一个描述所有软件组件时空行为的操作系统配置。
结合生成的应用程序软件,使用 Astrée 对 C 源代码进行检查。通过消除分析过程中发现的内存和类型缺陷,可以在 C 代码级别确保内存完整性。此外,在分析步骤中收集有关数据和函数访问行为的信息。在最后一步中,cAMP 工具利用这些信息将数据和函数低级映射到物理内存和保护区域。
最终成果包括带注释的应用程序代码和描述内存映射的链接脚本,它们保证满足所有项目特定的安全要求,并充分利用微控制器的功能。最终成果以及中间工作产品可在 GitHub上获取。使用该框架能够以高效且自动化的方式适配安全关键系统的通用应用程序软件,从而在不降低资源利用率或不危及系统安全的前提下实现软件复用。
本文由豆包软件翻译,如有不当之处请参照原文
下载请扫二维码:





- 点赞 0
-
分享
微信扫一扫
-
加入群聊
扫码加入群聊