基于雷达软件安全的C程序到形式模型的转换方法
作者：臧伟旺 朱健
来源：《现代信息科技》2022年第07期
        摘 要：文章主要以雷达系统软件安全为背景，首先提出了从C程序到基于一阶逻辑的形式模型的总体转换方法，通过定义辅助运算子，给出从C程序到形式模型保持语义一致的映射规则，对C程序的核心结构如赋值语句、条件语句、循环语句以及函数结构进行了规约，从而得到可执行的形式模型。最后，给出一个典型的C程序案例，应用转换规则生成了对应的形式模型，验证了转换方法的有效性。
        关键词：软件安全;C程序;一阶逻辑;形式模型
        中图分类号：TP311.5 文献标识码：A文章编号：2096-4706（2022）07-0026-04
        A Conversion Method of C Program to Formal Model Based on Radar Software Security
        ZANG Weiwang， ZHU Jian
        （Nanjing Research Institute of Electronics Technology， Nanjing 210039， China）
        Abstract： This paper mainly takes the software security of radar system as the background， firstly proposes a general conversion method from C program to formal model based on first-order logic， and gives the mapping rules from C program to formal model to maintain semantic consistency by defining auxiliary operators. The core structures of C programs such as assignment statements， conditional statements， loop statements and function structures are specified， so as to obtain an executable formal model. Finally， a typical C program case is given， and the corresponding formal model is generated by applying the transformation rules， which verifies the validity of the transformation method.
        Keywords： software security; C program; first-order logic; formal model
        0 引 言
        随着雷达系统不断发展，以及结构工艺的优化提高，对雷达软件设计提出了更高的要求，其中，软件的安全性与可靠性尤为重要，影响着整个雷达系统的行为是否符合预期以及性能的高低。传统的测试仿真方法[1]可以有效提高软件的可靠性，但无法遍历所有的执
行路径，从而不能证明一个软件没有漏洞。因此，需要引入形式化方法来保证软件的安全性。
        形式化方法[2]是一种基于数理逻辑的软硬件设计方法，也是目前安全关键软件系统的一种严格的验证技术。通过形式化逻辑的方式来表示合约代码，并加以严格地推理证明。这个过程依赖于数学逻辑推理的严密性，保证100%覆盖到代码的运行行为，可以保证在一定范围内的绝对正确。基于形式化方法的研究在一些安全攸关的领域，如雷达、核电、航空、区块链[3]等已经逐步得到应用，并且取得了非常好的效果。
        常见雷达软件编程语言如C语言可以编写可执行程序，具有图灵完备属性，实现较为复杂的功能，但是其安全性较差，容易产生漏洞，如整数溢出、数组越界、函数重入等等，从而给软件安全带来潜在的威胁，造成不可预料的损失。一阶逻辑是具有明确语法和语义的形式语言，且具有丰富的表达能力，可用于规约、定理证明和模型检测。
        本文提出从C程序到基于一阶逻辑的形式模型的转换方法，首先定义了C语言的核心子集，通过定义辅助运算子，给出了保持语义一致的映射关系，从而使用基于一阶逻辑的形式模型来规约C程序语言，包括赋值语句、条件语句、循環语句以及函数的规约，指导生
成的形式模型可以自动地被验证工具执行并验证程序的正确性，有效提高了C程序的安全性，以及程序验证的效率。
        1 总体转换方法
        我们提出基于形式模型的C程序建模与验证方法，如图1所示，一个C程序主要包括赋值语句、条件语句、循环语句以及函数结构，我们为每一个元素建立了与其语义保持一致的形式模型。其中，我们考虑C语言子集包括：
        （1）赋值语句：{p1， v=e， p2}，其中p1，p2表示赋值语句执行前后的程序，v表示程序变量，e为表达式;
        （2）条件语句if： {p1，if （Cond（v）） e1 else e2，p2}，其中Cond（v），表示从包含变量集合v的布尔表达式到true或者false布尔值的映射，e1，e2为语句集合;
        （3）循环语句while：{p1， while（Cond（v））{e}，p2}，其中e为循环体内部语句集合;
        （4）函数定义{p1，return_t func_name（para_list）{e}，p2}，其中return_t为函数返回值类型，func_name为函数名，para_list为包含参数类型和参数名的列表，e表示函数体的语句集合。
        目标形式模型基于一阶逻辑，其语法包括：
        （1）量化符号∀和∃;
        （2）逻辑连接词蕴含→、否定、双条件↔、且⋀以及或⋁;
        （3）括号、方括号以及其他自定义标点符号;
        （4）集合的变量，通常标记为英文字母的小写形式如x，y，z等;
        （5）等式符号=。
        对于程序而言，用户最关心的是程序的安全属性是否得到满足，如类型检查、可达性、死锁、无状态二义性等。通过转换规则，可以使用基于一阶逻辑的形式语言对程序建模以及对期望属性规约。当得到形式模型后，可以进行模型转换，转换为更加复杂的形式
模型。同时，借助验证平台，如Rodin，Isabelle，SPIN等证明工具对模型进行验证与仿真。通过工具提供的交互式定理证明助手，自动验证生成的证明义务，从而验证模型是否满足给定的属性。对于一些状态比较简单的模型，可以通过模型检测工具，对状态空间进行搜索穷举，如果到反例，则需要修改C程序，反之，则通过验证。