技术文章

浅谈基于SCADE Suite模型设计的安全性分析

时间:2024-01-25

作者·李雷

随着机载系统复杂度越来越高,机载系统软件的复杂度和代码量也急剧上升,同时要保证软件研制效率和质量难度越来越大,传统的软件研制方法已经难以满足要求。为了应对这些挑战,基于模型的软件研制方法应运而生,正被越来越广泛接受和应用。从趋势看,基于模型的软件方法将成为未来复杂软件研制的主要方法。目前很多研制单位正在积极引入基于模型的软件研制方法,并通过各种定制使其能和自己的业务更加匹配,并达到尽可能的自动化。

在这大环境下,SCADE Suite模型设计方案得到了市场的广泛认可。

 

一、什么是SCADE Suite?

 

SCADE Suite是软件设计工具,用于嵌入式控制软件建模、验证和代码生成。SCADE Suite可以实现软件的数据流处理、控制逻辑、状态切换等方面进行建模。而且SCADE Suite模型生成的代码可通过DO-178C/DO-330、EN 50128、ISO 26262、IEC 61508等标准认证。

SCADE Suite模型生成的代码能过一系列的认证,保证模型到代码的一致性,主要从以下方面严格要求:

1、实现建模准则:值的唯一性

SCADE Suite模型生成代码是模型对应的算法函数,该函数被调用一次,即执行一个周期。值的唯一性表示:在一个执行周期内,假设所有运算在同一时间内完成,也就是每个变量(无论输入、输出,还是局部变量)只能有一个值,通过这种方式来保证数据的安全性。同时SCADE Suite是由Esterel语言和Lustre语言等形式化语言发展而来的,要求模型做到精准无歧义。如实现一个计数器,完成自加功能,即i = i +1;常规建模如下:

模型中的i加1又给到了i,模型中的i既作为输入,又作为输出,这样的模型就会出现歧义,会导致后台语言无法识别i的真实用意。模型check就不会通过,就会给出相应的错误提示,数据i被多次赋值。也就不满足其值的唯一性。如果要实现这一功能,需要使用last值,利用上一周期的值进行累加,建模如下:

这样,模型生成的函数,每运行一次都是对上一个周期的数据加1,每个周期都有确定的值,以保证其数据的安全发生性,及代码生成的可靠性。

2、防御性模型设计

SCADE Suite是由Esterel语言和Lustre语言等形式化语言发展而来的,也决定了建模的确定性,在同等条件下,输入序列必定产生同样的输出序列。同时也必产生同样的C代码。包含对异常的数据处理。如从一个长度为8的数组里进行动态取值,即Valueout=ArrayIn[index]。如果index超出数组长度范围或出现负数的情况下,函数调用可能会中断下来。所以建模时需要进行如下处理,而不是单独的只是取值。

取得数组第Index个元素,如果Index超出数组范围,则输出操作符的第二个参数0作为默认值。生成的代码如下:

3、模型设计使用非常简单的控制流结构

模型到代码,使用简单的数据流翻译。从根本上杜绝使用goto语句等不安全代码。生成的代码中也没有使用直接或间接递归。

通常更简单的控制流可转化为更强的分析能力,可提高代码的 清晰度。避免递归的结果是拥有一个非循环函数调用图,代码生成前,可以分析堆栈使用的情况。

4、建模中必须给所有循环设置一个固定的上限。

SCADE Suite模型生成代码前必然检查模型中迭代有没有超过预设的迭代次数上限。如果没有上限设置,则视为违反规则。因为没有边界的递归可出现代码失控。

5、模型生成的代码不存在动态内存分配

通常内存分配器(如malloc)和垃圾回收器通常具有不可预测的行为,会严重影响性能。在不从堆分配内存的情况下,动态申请内存的唯一方法就是使用栈内存。在没有递归的情况下,堆栈内存使用量的上限可以通过静态方式推导出来,用以证明应用程序将始终在其资源范围内运行。

模型生成的代码会静态分配内存的方式确定其运行空间。强制所有应用程序在一个固定的、预先分配的内存区域内运行,可以消除以下许多问题。并使验证内存使用情况变得更容易。

6、对指针使用的限制

SCADE Suite建模过程中没有指针使用这一选项,因为即使是经验丰富的程序员也很容易滥用指针,会导致难以跟踪或分析程序中的数据流。

 

结束语

建模初期,很多开发人员会很不习惯,也不情愿去了解SCADE Suite,但是后期发现遵守模型设计规则确实有利于代码安全,这些规则减轻了开发人员和测试人员的负担,特别是在后期项目迭代的过程中,他们可以使用其他方法来确定代码的关键属性,如终止或有界性以及内存和堆栈的安全使用。这些规则就像汽车上的安全带起初,使用安全带可能会有点不舒服,但一段时间后,使用安全带就成了第二天性,而不使用安全带则会让人感到不舒服。

技术文章

姓名

公司

电话

邮箱