基于AADL的嵌入式系统完整性访问控制模型设计方法

摘要

本发明公开一种基于AADL的嵌入式系统完整性访问控制模型设计方法，具体步骤包括：1、利用架构分析和设计语言AADL搭建功能性架构模型，2、利用AADL搭建硬件架构模型，3、将完整性访问控制模型映射到架构模型中，4、验证完整性待验证的嵌入式系统架构模型的完整性，5、根据验证结果修改Integrity_Label属性值，6、输出包含完整性访问控制模型的嵌入式系统架构模型。克服了现有技术中需要在组件上标识主体、客体和访问关系的缺陷，和验证过程中需要将AADL模型转化为其他模型的缺陷。本发明具有建立和验证符合完整性访问控制模型的模型效率高的优点。

说明书

技术领域

本发明属于计算机技术领域，更进一步涉及嵌入式系统安全性分析技术领域中的一种基于架构分析和设计语言AADL(Architecture Analysis&Design Language)的嵌入式系统完整性访问控制模型设计方法。本发明可用于建立嵌入式控制系统的完整性系统架构模型以及验证嵌入式控制系统架构模型的完整性。

背景技术

完整性是指数据在传输时能够不被非法的篡改，或者在被篡改后能够及时的发现。从访问控制的角度看，完整性访问控制模型通过为访问数据的主体与数据客体分别分配一个完整性标签并在访问控制执行时，对完整性标签进行比较从而确保完整性要求得到满足。复杂的嵌入式系统的设计阶段容易产生缺陷导致违反完整性，违反完整性的设计会导致依据该设计实现的控制系统的控制参数(高完整性)易被低完整性的环境输入(如传感器输入)或攻击者注入的恶意数据篡改，引起控制系统完整性威胁。为了减少或避免设计上出现违反完整性要求的缺陷，优化系统设计，提出了一种基于AADL嵌入式控制系统完整性建模方法并提出针对该建模方法得到的模型的完整性验证方法。

西北工业大学在其申请的专利文献“基于AADL的系统脆弱性模型设计方法”(申请号：202110076365.2，申请公布号：CN 112764722 A，申请日：2021.01.20)中提出一种系统安全性建模的方法。该方法首先定义访问控制策略规定访问主体、访问客体以及访问关系，并使用附录扩展的形式对访问控制策略建模，然后将在每一个访问客体构件的构件实现中声明脆弱性模型附录子句并通过对每一个交互设置访问标志来标识交互是否被访问控制策略允许，得到基于AADL的系统脆弱性模型。该方法存在的不足之处是：需要通过对每一个交互设置访问标志来标识交互是否被访问控制策略允许，在系统交互量大的时候安全性建模开销大，得到的系统架构安全模型复杂度高，加大了对系统模型安全性验证的难度。

北京航空航天大学在其申请的专利文献“一种基于smartIflow的AADL模型的安全性分析方法”(申请号：202010062226.X，申请公布号：CN 111274699 A，申请日：2020.01.19)中提出了一种AADL模型的安全性分析方法。该方法首先通过建立AADL系统架构模型与错误模型并将其转化为smartIflow模型以验证其安全性，然后根据安全性需求制定安全属性并将其与smartIflow模型输入到smartIflow模型验证平台上从而输出验证结果。该方法存在的不足之处是：需要将AADL模型转化为其他可验证的模型，未能直接从AADL模型上执行验证过程，需要付出模型转化的额外开销，在系统架构模型较复杂的条件下，增加了系统安全性验证的开销。

发明内容

本发明的目的是针对上述现有技术的不足，提出了一种基于架构分析和设计语言AADL的嵌入式系统完整性访问控制模型设计方法，用于解决安全性建模开销大，得到的系统架构安全模型复杂度高的问题以及AADL模型安全性验证开销大的问题。

实现本发明目的的具体思路是：利用架构分析和设计语言AADL搭建架构模型，将完整性访问控制模型映射到架构模型中。本发明通过使用AADL对嵌入式系统架构进行建模，得到嵌入式系统架构模型，再定义完整性访问控制模型与架构模型的映射关系以及使用AADL的扩展属性集建立表示主客体完整性标签的Integrity_Label属性并将Integrity_Label属性根据访问规则添加到架构模型中，得到完整性待验证的嵌入式系统架构模型，该模型不需要在组件上标识主体、客体以及访问关系从而解决了解决安全性建模开销大，得到的系统架构安全模型复杂度高的问题。本发明对该嵌入式系统架构模型的完整性进行验证，修改不符合的Integrity_Label属性值，该验证过程直接对AADL模型进行验证，无需转化为其他模型，解决了AADL模型安全性验证开销大的问题，最终输出符合完整性访问控制模型的嵌入式系统架构模型。

本发明的具体步骤包括：

步骤1，利用架构分析和设计语言AADL搭建功能性架构模型；

步骤2，利用AADL搭建硬件架构模型；

步骤3，将完整性访问控制模型映射到架构模型中：

(3a)将嵌入式系统架构模型中的系统组件、进程组件、线程组件、处理器组件、设备组件和总线组件映射为完整性访问控制模型的主体；

(3b)将嵌入式系统架构模型中所有的数据端口、事件端口以及事件数据端口均映射为完整性访问控制模型的客体；

(3c)使用AADL的扩展属性集建立表示主客体完整性标签的Integrity_Label属性；

(3d)根据完整性访问控制规则将Integrity_Label属性分别依次添加到嵌入式系统架构模型中所有的系统组件、进程组件、线程组件、处理器组件、总线组件以及设备组件中和嵌入式系统架构模型中所有的数据端口、事件端口以及事件数据端口中；

(3e)输出完整性待验证的嵌入式系统架构模型；

步骤4，验证完整性待验证的嵌入式系统架构模型的完整性：

(4a)对于嵌入式系统架构模型中所有类型为系统组件、进程组件、线程组件、处理器组件以及设备组件的每一个组件，获取其特征声明中的数据端口、事件端口以及事件数据端口，将该组件的Integrity_Label属性值与其特征声明中所有的数据端口、事件端口以及事件数据端口中的Integrity_Label属性值进行比较，若该组件的Integrity_Label属性值大于或等于其特征声明中所有的数据端口、事件端口以及事件数据端口中的Integrity_Label属性值则执行步骤(4b)，否则，执行步骤5；

(4b)对于嵌入式系统架构模型中所有类型为系统组件、进程组件、线程组件、处理器组件、总线组件以及设备组件的每一个组件，获取其子组件声明中的子组件，将该组件的Integrity_Label属性值与其子组件声明中所有的子组件中的Integrity_Label属性值进行比较，若该组件的Integrity_Label属性值小于或等于其子组件声明中所有的子组件中的Integrity_Label属性值，则执行步骤(4c)，否则，执行步骤5；

(4c)判断嵌入式系统架构模型中所有类型为系统组件、进程组件、线程组件的每一个组件是否声明了处理器绑定属性，若声明了处理器绑定属性，则获取处理器绑定属性中声明的处理器组件并比较该组件与处理器组件的Integrity_Label属性值，若该组件的Integrity_Label属性值大于或等于处理器组件的Integrity_Label属性值，则执行步骤(4d)，否则，执行步骤5；

(4d)判断嵌入式系统架构模型中所有类型为系统组件、进程组件、线程组件、处理器组件以及设备组件的每一个组件是否声明了流路径，若声明了流路径，则获取所有流路径中声明的源特征与目的特征,并比较源特征与目的特征的Integrity_Label属性值，若源特征的Integrity_Label属性值大于或等于目的特征的Integrity_Label属性值，则执行步骤(4e)，否则，执行步骤5；

(4e)对于嵌入式系统架构模型中所有类型为系统组件、进程组件、线程组件、处理器组件以及设备组件的所有组件，获取这些组件的所有的连接实例，比较连接实例两端的端口的Integrity_Label属性值，若连接实例两端的端口的Integrity_Label属性值相等，则执行步骤6，否则，执行步骤5；

步骤5，根据验证结果修改Integrity_Label属性值；

步骤6，输出包含完整性访问控制模型的嵌入式系统架构模型。

本发明与现有技术相比具有以下优点：

第一，由于本发明将完整性访问控制模型映射到架构模型中，克服了现有技术中需要在组件上标识主体、客体以及访问关系的缺陷，使得本发明具有在建立符合完整性访问控制模型的嵌入式系统架构模型上获得模型复杂度低，建模效率高的优点。

第二，由于本发明验证完整性待验证的嵌入式系统架构模型的完整性，克服了现有技术在验证过程中需要将AADL模型转化为其他模型的缺陷，使得本发明能够直接在AADL模型上验证，节约了验证开销。

附图说明

图1为本发明的流程图；

图2为本发明实施例中无人机飞控系统的核心控制子系统图；

图3为本发明实施例中无人机飞控系统的硬件支持子系统图；

图4为本发明实施例中无人机飞控系统图。

具体实施方式

下面以无人机飞控系统为例结合附图对本发明做进一步的描述。

参照图1对本发明无人机飞控系统的完整性访问控制模型设计步骤作进一步详细说明。

步骤1，使用AADL的系统组件对无人机飞控系统的核心控制子系统UAVfunction建模，使用AADL的进程组件以及线程组件对无人机飞控系统的核心控制子系统中的四个核心控制组件建模，四个核心控制组件具体包括，传感器功能组件，位置控制组件，姿态控制组件，发动机控制组件；具体的核心控制组件建模过程为，使用AADL进程组件对传感器功能sensorfunction建模，使用线程组件对传感器功能sensorfunction内的速度传感器功能Acc、图像传感器功能Image以及陀螺仪功能Gyro建模；使用AADL进程组件对位置控制功能position建模，使用线程组件对位置控制组件的位置处理控制功能positionhandle建模；使用AADL进程组件对姿态控制attitude建模，使用线程组件对姿态控制的姿态控制处理功能attitudehandle建模；使用AADL进程对发动机控制功能motors建模，使用线程组件对发动机控制的发动机控制处理功能motorshandle建模。

表1，无人机飞控系统核心控制子系统架构模型组件端口表

使用AADL的数据组件与非数据组件的特征字段中的数据端口、数据事件端口、事件端口、端口连接以及数据流，对核心控制组件模型间的交互建模，得到每个核心控制组件交互模型；无人机飞控系统的各个控制组件以及控制组件的控制功能的模型所具有的端口，端口类型如表1所示。

无人机飞控系统各个端口连接以及数据流如表2所示。

表2，无人机飞控系统核心控制子系统架构模型交互表

由上述建模过程以及结合表1和表2得到的无人机飞控系统的功能性架构模型如图2所示。

步骤2，使用AADL的系统组件对飞行控制系统的硬件支持子系统UAVhardware建模，使用AADL进程组件对嵌入式系统的硬件支持子系统的固件建模；所述的固件为无人机处理器固件UAVfcProcessorFirmware。

使用AADL的设备组件对无人机飞控系统的硬件支持子系统的传感器sensor建模；使用AADL的处理器组件对无人机飞控系统的硬件支持子系统的无人机处理器UAVfcProcessor建模。

使用总线组件对无人机飞控系统的硬件支持子系统的支持传感器、处理器之间的物理连接的无人机总线UAVbus建模。

使用AADL的数据组件与非数据组件的特征字段中的数据端口、数据事件端口、事件端口、端口连接以及数据流对无人机飞控系统的硬件支持子系统的固件交互建模；所述的固件具体包括无人机处理器固件和无人机通信固件UAVCommunicationFirmware，各个固件模型的特征字段中声明的端口如表3所示，各个固件端口之间的端口连接和流路径如表4所示。

表3，无人机飞控系统硬件支持子系统固件端口表

表4，无人机飞控系统硬件支持子系统端口交互表

使用AADL的硬件组件的特征字段中的总线访问以及访问连接对无人机飞控系统的硬件支持子系统的传感器与处理器之间的交互建模；具体的建模过程为，在组件类型为设备组件的传感器sensor中的特征字段中声明传感器总线访问sensor_in,在组件类型为处理器组件的无人机处理器UAVfcProcessor中的特征字段中声明处理器总线访问processor_in，在硬件支持子系统UAVhardware中声明传感器模型与总线模型的访问连接bus_access1，在硬件支持子系统UAVhardware中声明处理器模型与总线模型的访问连接bus_access2。

使用AADL的处理器绑定属性对无人机飞控系统的硬件支持子系统的固件与处理器之间的搭载关系建模；在硬件支持子系统UAVhardware的属性字段中声明Actual_Processor_Binding属性将两个固件无人机处理器固件UAVfcProcessorFirmware以及无人机通信固件UAVCommunicationFirmware与无人机处理器UAVfcProcessor模型相关联。

根据上述建模过程得到的无人机飞控系统的硬件架构模型如图3所示，完整的无人机飞控系统模型如图4所示，其中图4(a)为无人机飞控系统的核心控制子系统，图4(b)为无人机飞控系统的硬件支持子系统。

步骤3，将无人机飞控系统架构模型中的系统组件、进程组件、线程组件、处理器组件、设备组件和总线组件映射为完整性访问控制模型的主体；所述的组件包括，传感器功能sensorfunction(进程)，速度传感器功能Acc(线程)，陀螺仪功能Gyro(线程)，图像传感器功能Image(线程)，位置控制功能position(进程)，位置处理控制功能positionhandle(线程)，姿态控制功能attitude(进程)，姿态控制处理功能attitudehandle(线程)，发动机控制功能motors(进程)，发动机控制处理功能motorshandle(线程)，无人机处理器固件UAVfcProcessorFirmware(进程)，传感器sensor(设备)，无人机处理器UAVfcProcessor(处理器)，无人机通信固件UAVCommunicationFirmware(进程)，无人机总线UAVbus(总线)。

将无人机飞控系统架构模型中所有的数据端口、事件端口以及事件数据端口均映射为完整性访问控制模型的客体；所述的端口包括，数据输出data_out(输出数据端口)，速度传感器输出Acc_out(输出数据端口)，陀螺仪输出Gyro_out(输出数据端口)，图像输出Image_out(输出数据端口)，位置输入position_in(输入数据端口)，位置输出position_out(输出事件数据端口)，位置处理输入positionhandle_in(输入数据端口)，位置处理输出positionhandle_out(输出数据端口)，姿态输入attitude_in(输入数据端口)，姿态输出attitude_out(输出事件数据端口)，姿态处理输入attitudehandle_in(输入数据端口)，姿态处理输出attitudehandle_out(输入数据端口)，发动机控制输入motors_in(输入事件数据端口)，发动机处理输入motorshandle_in(输入事件端口)，无人机处理器固件输出UAVfcProcessorFirmware_out(输出数据端口)，无人机处理器固件输入UAVfcProcessorFirmware_in(输入数据事件端口)，无人机通信固件输入1UAVCommunicationFirmware_in1(输入数据端口)，无人机通信固件输出2UAVCommunicationFirmware_out2(输出数据端口)，无人机通信固件输出1UAVCommunicationFirmware_out1(输出事件数据端口)，无人机通信固件输入2UAVCommunicationFirmware_in2(输入事件端口)。

使用AADL的扩展属性集建立表示主客体完整性标签的Integrity_Label属性。

根据完整性访问控制规则将Integrity_Label属性分别依次添加到无人机飞控系统架构模型中所有的系统组件、进程组件、线程组件、处理器组件、总线组件以及设备组件中和无人机飞控系统架构模型中所有的数据端口、事件端口以及事件数据端口中；具体的Integrity_Label属性值与需要添加的组件与端口如下，无人机飞控系统UAV(系统)的Integrity_Label属性值为Unclassified，核心控制子系统UAVfunction(系统)的Integrity_Label属性值为Unclassified，传感器功能sensorfunction(进程)的Integrity_Label属性值为Unclassified，速度传感器功能Acc(线程)的Integrity_Label属性值为Important，陀螺仪功能Gyro(线程)的Integrity_Label属性值为Important，图像传感器功能Image(线程)的Integrity_Label属性值为Important，位置控制功能position(进程)的Integrity_Label属性值为VeryImportant，位置处理控制功能positionhandle(线程)的Integrity_Label属性值为Critical，姿态控制功能attitude(进程)的Integrity_Label属性值为VeryImportant，姿态控制处理功能attitudehandle(线程)的Integrity_Label属性值为Critical，发动机控制功能motors(进程)的Integrity_Label属性值为VeryImportant，发动机处理功能motorshandle(线程)的Integrity_Label属性值为Critical，硬件支持子系统UAVhardware(系统)的Integrity_Label属性值为Unclassified，传感器Sensor(设备)的Integrity_Label属性值为VeryImportant，无人机处理器UAVfcProcessor(处理器)的Integrity_Label属性值为VeryImportant，无人机处理器固件UAVfcProcessorFirmware(进程)的Integrity_Label属性值为VeryImportant，无人机通信固件UAVCommunicationFirmware(进程)的Integrity_Label属性值为VeryImportant，无人机总线UAVbus(总线)的Integrity_Label属性值为VeryImportant，数据输出data_out(输出数据端口)的Integrity_Label属性值为Unclassified，速度传感器输出Acc_out(输出数据端口)的Integrity_Label属性值为Unclassified，陀螺仪输出Gyro_out(输出数据端口)的Integrity_Label属性值为Unclassified，图像输出Image_out(输出数据端口)的Integrity_Label属性值为Unclassified，位置输入position_in(输入数据端口)的Integrity_Label属性值为Important，位置输出position_out(输出事件数据端口)的Integrity_Label属性值为Important，位置处理输入positionhandle_in(输入数据端口)的Integrity_Label属性值为Important，位置处理输出positionhandle_out(输出数据端口)的Integrity_Label属性值为Important，姿态输入attitude_in(输入数据端口)的Integrity_Label属性值为Important，姿态输出attitude_out(输出事件数据端口)的Integrity_Label属性值为Important，姿态处理输入attitudehandle_in(输入数据端口)的Integrity_Label属性值为Important，姿态处理输出attitudehandle_out(输入数据端口)的Integrity_Label属性值为Important，发动机控制输入motors_in(输入事件数据端口)的Integrity_Label属性值为Important，发动机处理输入motorshandle_in(输入事件端口)的Integrity_Label属性值为Important，无人机处理器固件输出UAVfcProcessorFirmware_out(输出数据端口)的Integrity_Label属性值为Important，无人机处理器固件输入UAVfcProcessorFirmware_in(输入数据事件端口)的Integrity_Label属性值为Important，无人机通信固件输入1UAVCommunicationFirmware_in1(输入数据端口)的Integrity_Label属性值为Important，无人机通信固件输出2UAVCommunicationFirmware_out2(输出数据端口)的Integrity_Label属性值为Important，无人机通信固件输出1UAVCommunicationFirmware_out1(输出事件数据端口)的Integrity_Label属性值为Important，无人机通信固件输出1UAVCommunicationFirmware_out1(输出事件数据端口)的Integrity_Label属性值为Important，无人机通信固件输入2UAVCommunicationFirmware_in2(输入事件端口)的Integrity_Label属性值为Important。

输出完整性待验证的无人机飞控系统架构模型。

步骤4，使用开源AADL工具环境OSATE(Open Source AADL Tool Environment)上的模型验证工具Resolute执行步骤4，验证完整性待验证的嵌入式系统架构模型的完整性。

第一步，定义Resolute函数is_lower_or_same_integrity_level_property(lower,higher),该函数的参数lower为理论上Integrity_Label属性值较小的AADL模型元素，参数higher为理论上Integrity_Label属性值较大的AADL模型元素，该函数通过将理论结果与实际结果进行比较，返回值为true则说明所比较的两个AADL模型元素的Integrity_Label属性值的实际大小关系与理论上的大小关系一致；返回值为false则说明不一致。

第二步，对于无人机飞控系统架构模型中所有类型为系统组件、进程组件、线程组件、处理器组件以及设备组件的每一个组件，获取其特征声明中的数据端口、事件端口以及事件数据端口，将该组件的Integrity_Label属性值与其特征声明中所有的数据端口、事件端口以及事件数据端口中的Integrity_Label属性值进行比较，若该组件的Integrity_Label属性值大于或等于其特征声明中所有的数据端口、事件端口以及事件数据端口中的Integrity_Label属性值则执行本步骤的第三步；具体过程为，定义Resolute函数rule_1，该函数使用Resolute内置函数features()获取组件中features的集合，遍历集合并将组件与features集合中的元素作为参数执行is_lower_or_same_integrity_level_property(lower,higher)函数，对无人机飞控系统架构模型中所有类型为系统组件、进程组件、线程组件、处理器组件以及设备组件的每一个组件均执行rule_1函数，所有被执行的rule_1函数的返回值均为true。

第三步，对于无人机飞控系统架构模型中所有类型为系统组件、进程组件、线程组件、处理器组件、总线组件以及设备组件的每一个组件，获取其子组件声明中的子组件，将该组件的Integrity_Label属性值与其子组件声明中所有的子组件中的Integrity_Label属性值进行比较，若该组件的Integrity_Label属性值小于或等于其子组件声明中所有的子组件中的Integrity_Label属性值，则执行本步骤的第四步；具体过程为，定义Resolute函数rule_2，该函数使用Resolute内置函数subcomponents()获取组件中的subcomponent集合，遍历集合并将组件与subcomponent集合中的元素作为参数执行is_lower_or_same_integrity_level_property(lower,higher)函数，对无人机飞控系统架构模型中所有类型为系统组件、进程组件、线程组件、处理器组件、总线组件以及设备组件的每一个组件均执行rule_2函数，所有被执行的rule_2函数的返回值均为true。

第四步，判断无人机飞控系统架构模型中所有类型为系统组件、进程组件、线程组件的每一个组件是否声明了处理器绑定属性，若声明了处理器绑定属性，则获取处理器绑定属性中声明的处理器组件并比较该组件与处理器组件的Integrity_Label属性值，若该组件的Integrity_Label属性值大于或等于处理器组件的Integrity_Label属性值，则执行本步骤的第五步；具体过程为，定义Resolute函数rule_3，该函数将声明了处理器绑定属性的所有类型为系统组件、进程组件、线程组件的组件与其绑定的处理器组件作为is_lower_or_same_integrity_level_property(lower,higher)函数的参数，无人机飞控系统架构模型中所有类型为系统组件、进程组件、线程组件且声明了处理器绑定属性的每一个组件均执行rule_3函数，所有被执行的rule_3函数的返回值均为true。

第五步，判断无人机飞控系统架构模型中所有类型为系统组件、进程组件、线程组件、处理器组件以及设备组件的每一个组件是否声明了流路径，若声明了流路径，则获取所有流路径中声明的源特征与目的特征,并比较源特征与目的特征的Integrity_Label属性值，若源特征的Integrity_Label属性值大于或等于目的特征的Integrity_Label属性值，则执行本步骤的第六步；具体过程为，定义Resolute函数rule_4，该函数使用Resolute内置函数flow_specifications()获取组件内定义的流路径的集合，对集合中的每一个流路，将源features和目的features作为参数执行Resolute自定义函数is_lower_or_same_integrity_level_property(lower,higher)，对无人机飞控系统架构模型中所有类型为系统组件、进程组件、线程组件、处理器组件以及设备组件且声明了流路径的每一个组件均执行rule_4函数，所有被执行的rule_4函数的返回值均为true。

第六步，对于嵌入式系统架构模型中所有类型为系统组件、进程组件、线程组件、处理器组件以及设备组件的所有组件，获取这些组件的所有的连接实例，比较连接实例两端的端口的Integrity_Label属性值，若连接实例两端的端口的Integrity_Label属性值相等，则执行步骤5；具体过程为，定义Resolute函数rule_5，该函数使用Resolute函数connections()获取所有的连接实例，对每个连接实例，获取其两端的端口，再使用Resolute自定义函数get_Integrity_Label(element)获取端口的Integrity_Label属性值并比较，对于无人机飞控系统架构模型中所有类型为系统组件、进程组件、线程组件、处理器组件以及设备组件的所有连接实例执行rule_5，所有被执行的rule_5函数的返回值均为true。

步骤5，根据验证结果修改Integrity_Label属性值，完整性待验证的嵌入式系统架构模型的完整性的验证结果均正确，故无需修改Integrity_Label属性值。

步骤6，输出嵌入式系统的包含完整性访问控制模型的架构模型。