基于编码规则的中断数据访问冲突检测方法*

陈 睿，杨孟飞

(1.北京控制工程研究所，北京 100190； 2.北京轩宇信息技术有限公司，北京 100190；3.中国空间技术研究院，北京 100190)



基于编码规则的中断数据访问冲突检测方法*

陈 睿1,2，杨孟飞3

(1.北京控制工程研究所，北京 100190； 2.北京轩宇信息技术有限公司，北京 100190；3.中国空间技术研究院，北京 100190)

针对“重复加锁解锁”和“volatile修饰符误用”两种数据访问冲突缺陷模式，提出基于编码规则的检测方法.首先，对缺陷模式的故障机理进行分析，提炼出3条编码规则用以在开发阶段避免缺陷发生，并基于一个静态代码检查工具SpaceCCH进行了规则检测方法研究和实现.在实际星上软件上的实验结果表明，扩展的SpaceCCH能够高效、低误报、低漏报地发现规则违反，从而有效避免这两种的数据访问冲突问题.本文的贡献在于将一类复杂缺陷的检测转换为相应的编码规则及其检测. 关键词： 数据访问冲突；编码规则；静态分析；航天嵌入式软件

0 引 言

数据访问冲突问题是当前航天型号软件开发中最难解决的问题之一[1].这类问题发生在中断驱动型程序或多任务程序中，当两个不同的中断(或任务)对同一个共享数据进行同时的读写访问，且至少存在一次写操作时.由于两次访问的时序不可确定，程序会产生异常行为，如关键数据被非预期地修改，严重时甚至导致系统或软件失效.然而，数据访问冲突问题发生概率小、难以复现，往往在特殊的外部条件和中断(或任务)交迭情况下才会出现，难以通过传统的软件测试方法发现，遗漏率较高.因此，近年来数据访问冲突自动检测方法已成为研究热点，国家自然科学基金“可信软件基础研究”重大研究计划以及民用航天预先研究等都先后资助了相关课题，产生了一批有价值的方法或工具成果[2-9].

在安全关键领域，在软件编码过程中采用一定的编码标准是缺陷预防的最有效手段之一.各个行业组织和机构都根据应用领域或软件开发的特点制定各自的编码标准，比较著名的有汽车工业软件可靠性协会的MISRA C[10]、NASA喷气推进实验室的“The Power of Ten”[11]以及中国空间技术研究院院标准《航天器C语言软件编程约定》等.一般地，一个编码标准包含若干编码规则，每条规则在编程语言标准语言特性的基础上增加使用限制，以使相应的危险程序行为受限或降低其发生风险.实践证明，通过应用编码规则及相应的自动化检查工具，能够在编码阶段有效地预防一些潜在的问题.

文献[2]通过大量真实案例分析提出刻画有害数据访问冲突的7种缺陷模式，并针对其中部分模式提出了相应的检测方法.本文针对尚缺乏自动化检测方法的模式5和模式6，对其故障机理进行分析，提炼形成3条相应的编码规则；在软件编码过程应用这些编码规则可以避免相应模式的缺陷；进一步提出基于规则的数据访问冲突检测方法，对上述3条编码规则进行自动化检测，实现对相应缺陷的保障.上述研究方法学如图1所示.本文提出的方法在一个C语言静态代码检查工具SpaceCCH基础上实现，并在实际航天型号软件中进行了实验评估，验证了方法的有效性.

1 缺陷模式及实例分析

文献[2]中的缺陷模式5和6是本文研究的问题.本节结合实例对这两个模式进行说明和分析.

模式5. 重复加锁解锁

开关中断类似于多线程程序中的锁机制,可用于屏蔽中断处理,从而保证一段代码的原子性.这两个操作总是成对出现的.若在没有意识到此时已经处于锁保护状态下再次进行加锁解锁操作,会导致第二次解锁时候的代码未被保护,从而引发非预期的数据访问冲突.

图3给出了模式5对应的的程序示例,为了保证StarTime变量计算的完整性，主程序main中采用ET0=0和ET0=1这一对加锁解锁操作来屏蔽中断2中对Time结构体的更新.然而，实际执行中可能出现下面的场景：

1)主程序main执行ET0=0，清除ET0寄存器以关闭中断2；

2)中断1打断主程序，进行某种操作，由于需要对中断2进行屏蔽，也进行了ET0=0和ET0=1的操作分别对中断2进行关闭和打开；

3)从中断1返回主程序后，当前中断2处于未屏蔽状态，与主程序原期望不符；

4)中断2打断主程序，并对Time变量进行了写操作，导致主程序和中断2发生了数据访问冲突，StarTime计算错误.

上述场景是在系统实际运行中真实暴露的，通过传统的测试非常难以发现.但从加锁解锁操作的时序特征比较容易刻画，中断2的加锁解锁操作序列为加锁、加锁、解锁、解锁.这一模式便于将这类缺陷规则化，易于研究进一步的检查方法.

模式6. volatile修饰符误用

volatile是C语言中一个极易被误解的特性.该关键字告诉编译器被修饰的变量可能被中断、任务或编译器不知道的其他并发操作所修改.当变量被volatile修饰时，编译器知道处理器必须每次都从内存中读取该变量的值，因此编译器不会对这类变量的访问进行优化.一些较老的编译器不支持volatile关键字，开发人员必须关闭编译器优化以获得正确的结果.

在下面的示例中，secondsToday为long类型，长度为4字节，无论是8位机还是16位机，对secondsToday变量的一条操作语句会拆分为多条目标码指令.当完成对该变量的第一个字节进行读，若发生中断，则会导致13行语句执行后IReturn值与secondsToday值不一致.为了避免这种情况，在第14～16行增加一个while循环对13行语句是否正确执行进行再次判断和赋值，最终保证返回当前实际的secondsToday值.

若secondsToday变量未采用volatile修饰，大多数编译器做这样的假设：除非程序修改变量的值，否则变量值会在内存中保持，在编译优化打开的情况下，在第14行处，程序会从寄存器中读取secondsToday的值，与程序编写预期不同；一些优化编译器会认为在13行secondsToday的值刚刚复制到IReturn变量，14行的while条件总是为假，则会优化掉整个while循环体.

由于对volatile特性的不了解，上述案例常常被认为是编译器的缺陷.上述问题的最优解决方法是：制定编码规则，通过编码规则来保证程序在共享变量上正确使用volatile修饰符，进一步通过规则自动检查的方法来实现对该缺陷模式的自动检测.

2 检测方法及工具

针对缺陷模式5和6，提炼形成3条相应的编码规则，基于一个已有的静态代码检查工具SpaceCCH进行了规则的扩展实现.其中，规则1和规则2的自动检查采用符号表检索和类型检查方法，通过SpaceCCH已有分析引擎可较容易实现；针对规则3，本文提出了面向状态机规则的静态分析方法，并扩展了SpaceCCH的分析引擎.最终，实现了所有规则的自动检查.

2.1 面向数据访问冲突的编码规则

本文对缺陷模式5和6进行了分析，提炼出3条用于避免缺陷发生的编码规则.

规则1.对于下列情况必须使用volatile进行数据声明修饰.

a)被任意中断服务程序使用的全局变量；

b)在两个以上抢占式任务中使用的全局变量；

c)指向I/O端口或外设寄存器组的指针变量.

规则原理：强制上述数据的声明使用volatile修饰，可以保证编译器优化不会改变对这些数据的读写访问及其顺序，避免部分关键操作在实际目标码中丢失，引发数据访问冲突.

规则2.volatile修饰符应在变量所有的声明或定义处保持一致.

规则2的违反示例如图4所示.程序中，smp.c中ipi_count的定义采用volatile修饰，而smp.h中该变量的外部声明未采用volatile修饰，这两处volatile修饰符的使用不一致.

规则原理：按照规则1，对有关共享数据采用volatile进行修饰.但若头文件中的声明和c文件中的定义使用不一致时，在包含该头文件的源代码中对应共享数据不被视为volatile，导致volatile修饰无效，可能引发问题.这种不一致的定义声明方式在一些编译器中是合法的，因此需要进行约束.

规则3.当采用中断屏蔽机制进行原子区加锁保护时，禁止在同一条执行路径上出现两次以上嵌套加锁/解锁操作.

规则原理：每一对加锁/解锁操作都期望保护一段完整的临界区不被打断，若嵌套额外的加锁/解锁操作队时，内层的解锁操作会使外层临界区处于开放状态，从而引发非预期的数据访问冲突.

2.2 SpaceCCH工具及规则扩展

SpaceCCH工具是由北京控制工程研究所自主研发的面向高安全软件系统的静态代码检查工具，能够对超过250条编码规则进行自动审查.SpaceCCH工具采用插件式的体系结构，提供基于统一中间表示(抽象语法树、符号表、控制流图)的扩展开发API，支持自定义规则的快速开发.SpaceCCH工具的系统结构如图5所示.

SpaceCCH工具由前端分析器和静态分析引擎两部分组成.

其中，前端分析器又包括词法分析器、语法分析器和AST分析器三部分.以给定源程序为输入，首先由词法分析器和语法分析器处理，并获得程序的抽象语法树，此后AST分析器通过对AST的一系列分析处理，最终产生静态分析过程所需的中间表示，主要包括控制流图(control flow graph, CFG)、调用图、符号表和抽象语法树(abstract syntax tree, AST).

静态分析引擎包括控制流分析器、数据流分析器、规则检查引擎等.其中，控制流分析器主要用于对提取控制路径、检测循环、处理函数调用等；数据流分析器主要完成对循环的局部数据流分析，产生迭代分析的结果供整体分析过程利用；规则检查器以及实例化的规则实现负责完成相应的规则检查功能.静态分析引擎以前端输出的四种中间表示为输入，经过控制流分析器、数据流分析器和规则检查器的共同处理，最后生成缺陷报告.

SpaceCCH提供了符号表检索、AST遍历、数据流分析和类型检查等丰富的扩展接口，本文基于上述接口对规则1、2进行了扩展.其中，规则1通过调用图分析结果，根据AST特征收集中断或任务中使用的所有I/O端口、全局变量、绝对地址指针变量，进一步根据规则1的要求筛选出相关数据的声明语句，判断其是否采用volatile修饰，确定是否违反规则、存在潜在的数据访问冲突风险；规则2通过跨文件符号表检索获得所有volatile修饰的符号定义，再判断该定义对应的符号声明是否也用volatile修饰，实现对该规则的检查.

2.3 面向有限状态机规则的静态分析

针对规则3，本文提出一种基于有限状态机规则的静态分析方法.在这种方法中，一条规则R可以采用一个扩展的有限状态机来表示，其对应的扩展状态机模型为M=〈Q,P,δ,q0,F〉，其中：

1)Q是规则中定义的状态的集合.

2)P是M的模式集合，只有输入字母能与P中某个模式相匹配时，该输入才被状态机所接收，从而触发状态转移.

3)δ是M的转移函数，指定状态机从某一状态迁移到下一状态.

4)q0是M的初始状态.

5)F是状态机的终止状态，即规则的错误状态.

规则3对应的状态机模型示例图如图6所示.其中，状态集Q={初始态,加锁态,多重加锁态,错误态}，模式集P={lock, unlock}，对应中断屏蔽和打开的C语言操作.状态机模型是静态分析时状态机实例的元模型，状态机实例的状态值来源于该模型的状态集合，同样初始状态和终止状态也是在模型中所定义的.当一个M的状态机实例到达状态机模型中的错误状态时即表明违反给定规则的错误出现.

在对该规则进行检查的算法(如图7所示)是：

1)给定被测程序的入口函数控制流图cfg、当前程序状态ps和规则r，调用check函数进行检查；初始时ps为基于该状态机模型创建的状态机实例I，I为初始态；

2)静态分析引擎依次对主程序或中断的入口函数CFG进行深度优先遍历；

3)在对路径中每个节点进行分析时，规则检查器根据状态机实例当前状态、节点操作与模式的匹配情况决定是否进行状态转移，当程序状态中的某个状态机实例转移到错误状态时，表示程序中出现了违反给定规则的错误.

为了提高错误检测的精确性，SpaceCCH静态分析引擎引入路径敏感分析，并且支持上下文敏感的过程间分析.考虑到效率和可伸缩性，SpaceCCH在遍历分析的环节采用了一系列缓存优化机制，显著地加快了分析过程，这些方法与文献[2]相同.

3 实验与评估

为了对SpaceCCH的分析性能和分析精确度等指标进行评估，针对本文提出的3条与数据访问冲突相关的编码规则，选取4个真实的星上软件样本进行了实验.实验是在一台普通的HP PC机(CPU为Intel Core 2 2.40 G，内存为2 GB)上进行的，表1给出了每个被分析软件的属性以及分析的各项指标.

从实验结果中可以看出，SpaceCCH能够适应于各种编译配置下的软件，如软件B和软件D分别采用Keil C51和SPARC扩展的C方言进行编程.对于规模最大的软件A，SpaceCCH在12.185秒内就能完成分析，并且只占用28.65 M的内存，表明工具具有良好的可伸缩性.由于软件样本的限制，本文没有对规模更大的软件进行实验.

被分析项编译配置规模(LOC)分析时间/s内存峰值/M规则1违反预埋规则2违反预埋规则3违反预埋误报漏报软件AANSIC1086212.185028.6561000软件BKeilC5116710.76504.4121100软件CANSIC942716.387023.4272000软件DgccforSPARC34871.37504.5331000

本文针对3条规则在4个被测软件中预埋了一定数量的违反，如表1所示.在实验中，未发现SpaceCCH的分析结果中存在误报，并且实现了零漏报.这是因为，本文从方法学上把一个复杂数据访问冲突缺陷的检测转换为了对特定编码规则的检查，编码规则检查方法较少涉及程序行为的分析，是可判定的.

上述实验结果表明：

1)SpaceCCH具有良好的可伸缩性，能够适用于大规模航天嵌入式软件的编码规则检查，而且具有较好的分析精度和分析性能；

2)本文提出的3条编码规则在SpaceCCH中得到了实现，并能够有效检测出潜在的数据访问冲突缺陷.

4 结束语

本文针对航天嵌入式软件中断数据访问冲突中两类难以测试的缺陷模式，提出了相应的3条编码规则，用以在编码阶段有效避免相关的数据访问冲突问题.基于编码规则，对一个已有的静态代码检查工具SpaceCCH进行了扩展，并提出了一个基于有限状态机规则的静态分析方法，实现了对3条编码规则的自动检查.实验结果表明，扩展后的SpaceCCH能够高效、精确地对相应的编码规则违反进行自动检查，从而避免数据访问冲突问题的发生.

[1] 杨孟飞, 顾斌, 郭向英, 等. 航天嵌入式软件可信性保障技术及应用研究[J]. 中国科学: 技术科学, 2015(2):198-203. YANG M F， GUO B, GUO X Y, et al. Aerospace embeded software dependability guarantee technology and application[J]. Scientia Sinica Technologica, 2015(2):198-203.

[2] 陈睿, 杨孟飞, 郭向英. 基于变量访问序模式的中断数据竞争检测方法[J].软件学报,2016, 27(3): 547-561. CHEN R, YANG M F, GUO X Y. Interrupt data race detection based on shared variable access order pattern[J]. Journal of Software, 2016, 27(3): 547-561.

[3] 段永颢,陈睿.基于启发式的静态中断数据竞争检测方法[J].计算机工程与设计,2013,34(1):140-145. DUAN Y H, CHEN R. Heuristic static data race detection for interrupt-driven software[J]. Computer Engineering and Design, 2013,34(1):140-145.

[4] CHEN R, GUO X Y, DUAN Y H, et al. Static data race detection for interrupt-driven embedded software[C]//International Conference on Secure Integration and Reliability Improvement. New York: IEEE,2011，47-52.

[5] REGEHR J, COOPRIDER N. Interrupt verification via thread verification[J]. Electron. Notes Theoretical Computer Science,2007,174(9).

[6] 周筱羽, 顾斌, 赵建华,等.中断驱动系统模型检验[J]. 软件学报,2015,26(9):2221-2230. ZHOU X Y, GU B,ZHAO J H, et al. Model checking technique for interrupt-driven system[J]. Journal of Software,2015,26(9):2221-2230.

[7] WU X G, Wen Y J, CHEN L Q, et al. Data race detection for interrupt-driven programs via bounded model checking[C]//The IEEE 7thInternational Conference on Software Security and Reliability-Companion(SERE-C).New York: IEEE,2013,204-210.

[8] 霍玮,于洪涛, 冯晓兵,等.静态检测中断驱动程序的数据竞争[J].计算机研究与发展,2011,48(12):2290-2299. HUO W YU H T, FENG X B, et al. Static data race detection of interrupt-driven programs[J].Journal of Computer Research and Development,2011,48(12):2290-2299.

[9] 陈园军,石浚菁,王林章,等.中断驱动的嵌入式系统数据竞争检测工具[J].计算机科学与探索, 2015, 9(8):914-925. CHEN Y J, SHI J J, WANG L Z, et al. Data race detection tool for interrupt-driven embedded system[J]. Journal of Frontiers of Computer Science and Technology, 2015,9(8):914-925.

[10] Motor Industry Software Reliability Association (MISRA). Guidelines for the use of the C language in critical systems[S].MISRA-C, 2004.

[11] The Power of Ten . Rules for developing safety critical code[J]. IEEE Computer, 2006:93-95.

Coding Rule Based Interrupt Data Race Detection Method

CHEN Rui1,2, YANG Mengfei1,3

(1.BeijingInstituteofControlEngineering，Beijing100190，China；2.BeijingSunwiseInformationTechnologyCo.Ltd.，Beijing100190，China；3.ChinaAcademyofSpaceTechnology,Beijing100094,China)

To solve pattern “double lock & unlock” and pattern “misuse of volatile”, a detection method based on coding rules is proposed. Firstly, the failure mechanism is analyzed, and then 3 coding rules are proposed to avoid corresponding defects in development stage. These rules and corresponding checking methods are researched and implemented by extending an existing static analysis tool named SpaceCCH. The evaluation result based on real world on-board software show that, the extended SpaceCCH can find rules violations efficiently with low false positive rate and low false negative rate, by which the data race bugs of pattern “double lock & unlock” and pattern “misuse of volatile” can be avoided effectively. The main contribution of this paper is that the detection of a really complex bug is transformed to corresponding coding rules and their automatic detection.

data race； coding rule； static analysis； aerospace embedded software

*国家自然科学基金资助项目(91118007,61632005).

2017-02-01

陈 睿(1984—)，男，高级工程师，研究方向为程序分析与软件测试；杨孟飞(1962—),男,研究员,研究方向为空间飞行器系统设计、控制计算机系统及嵌入式软件.

TP311

A

1674-1579(2017)03-0059-07

10.3969/j.issn.1674-1579.2017.03.010