中断驱动型航天嵌入式软件原子性违反检测方法_于婷婷.pdf

中断驱动型航天嵌入式软件原子性违反检测方法于婷婷1,2李超1,2王博祥1陈睿1,2江云松1,21（北京轩宇信息技术有限公司北京100190）2（北京控制工程研究所北京100190）（）Atomicity Violation Detection for Interrupt-Driven Aerospace Embedded SoftwareYuTingting1,2,LiChao1,2,WangBoxiang1,ChenRui1,2,andJiangYunsong1,21（Beijing Sunwise Information Technology Ltd.,Beijing 100190）2（Beijing Institute of Control Engineering,Beijing 100190）AbstractThe dependability of embedded software is vital to the success of the aerospace mission.Aerospaceembedded software extensively uses interrupt-driven concurrency mechanisms.However,uncertain interleavingexecutionofinterruptsmaycauseconcurrencybugs,whichcouldresultinserioussafetyproblems.Researcheshadshowed that atomicity violation was the most prominent interrupt concurrency bug.Current atomicity violationdetectionmethodsforinterrupt-drivenembeddedsoftwarecannotachievebothhighprecisionandhighscalability,andtheir effectiveness on real embedded software has not been evaluated.To significantly improve the ability oftechniquesinbugdetection,wedesignanempiricalstudyon82atomicityviolationsinaerospaceembeddedsoftwareandgaintheirmanifestationcharacteristicsofatomicregionrange,thenumberofinterruptnestinglevels,shareddataaccessinterleavingpattern,accesspatternsandaccessgranularities.Onthisbasis,wepresentintAtom-S,apreciseandefficientstaticdetectiontechniqueforatomicityviolations.Firstly,torealizeaccurateanalysisofshareddata,intAtom-Sconstructsafine-grainedmemorymodelparameterizedbynumericalinvariants,andintroducesrule-basedmethodtoeliminateflagvariableaccesses.Moreover,itcanhandlearrayelementsaswellassharedI/Oaddresses.Then,alightweightdataflowanalysistechniqueisusedtofindallaccessinterleavingsthatmatchthepatternsaspotentialbugcandidates.Finally,intAtom-Sadoptsaconsecutiveaccesspairfeasibilityanalysisandaccessinterleavingfeasibilityanalysistoprunetheinfeasiblepaths.intAtom-Sgraduallyeliminatesfalsepositives,andobtainsthefinalatomicityviolations.Experimentsonabenchmarkand8real-worldaerospaceembeddedsoftwareshowthatintAtom-Sreducesthe false positive rate by 72%and improves the detection speed by 3 times,compared with the state-of-the-artmethods.Furthermore,itcanfinishanalyzingthereal-worldaerospaceembeddedsoftwareveryfastwithanaveragefalsepositiverateof8.9%,whilefinding23bugsthathadbeenconfirmedbydevelopers.Key wordsaerospaceembeddedsoftware；interrupt；concurrencybugs；bugcharacteristics；atomicityviolation；staticanalysis摘要嵌入式软件的可信性对航天任务的成败至关重要.航天嵌入式软件广泛采用中断驱动的并发机制,不确定的中断抢占可能导致并发缺陷,引发严重的安全问题.研究表明原子性违反是中断并发缺陷中最突出的一类缺陷模式.目前面向中断驱动型嵌入式软件的原子性违反检测方法都无法同时实现高精度和高可扩展性,且其对真实航天嵌入式软件的有效性尚未得到证实.为了有效提升检测该类缺陷的精度收稿日期：20221026；修回日期：20221229基金项目：国家自然科学基金项目（61802017,62192730）ThisworkwassupportedbytheNationalNaturalScienceFoundationofChina(61802017,62192730).通信作者：陈睿（）计 算 机 研 究 与 发 展DOI：10.7544/issn1000-1239.202220908JournalofComputerResearchandDevelopment60（2）：294310，2023与效率,对 82 个航天嵌入式软件原子性违反进行实证研究,获得该类缺陷在原子区范围、中断嵌套层数、访问交错模式、共享数据访问方式、访问粒度等 5 个方面的表现特征.并在此基础上,提出一个精确、高效的原子性违反静态检测方法 intAtom-S.首先,基于一个由数值不变式参数化的细粒度内存访问模型,引入基于规则的方法剔除标志变量访问,并采用抽象解释进行精确的共享数据分析,该分析能将共享数据访问粒度精确至数组元素,并可识别共享的内存映射 I/O 地址.然后,使用轻量级数据流分析技术匹配符合缺陷访问交错模式的所有并发三次访问序,作为潜在的原子性违反缺陷候选.最后,采用基于路径条件的约束求解对缺陷候选中的串行访问对和并发三次访问序进行路径可行性分析,逐步消除误报,得到最终的原子性违反结果.在基准测试集和 8 个真实航天嵌入式软件上的实验表明,与目前最先进的方法相比,intAtom-S 误报率降低了 72%,检测效率提高了 3 倍.此外,该方法能够快速完成对真实航天嵌入式软件的分析,平均误报率仅为 8.9%,并发现了 23 个已被开发人员确认的缺陷.关键词航天嵌入式软件；中断；并发缺陷；缺陷特征；原子性违反；静态分析中图法分类号TP311嵌入式软件的可信性对航天任务成败至关重要，即使一个微小的软件缺陷也可能导致重要任务的失败.航天嵌入式软件广泛采用中断驱动的并发机制，与硬件频繁地进行交互并实时地响应外界事件1.当一个系统中的大量处理都由中断发起时，我们称这类系统为中断驱动型系统2.中断驱动型嵌入式软件使用大量的共享数据来实现主任务和中断，以及不同中断之间的通信和数据交互.如图 1 所示，航天嵌入式软件通常由主任务和多个中断服务程序构成.主任务的结构是一个无限循环，等待中断的触发进行相应的操作.中断由来自软件或硬件（如定时器、外设和 I/O 端口）的中断信号触发，例如由内部事件及“异常”，或由接收字节的串行端口控制器触发.然后，处理器通过挂起其他当前活动、保存其状态并执行中断处理程序来响应当前事件.待中断处理完成后，处理器恢复其正常活动.由于中断可能在任意时刻发生并抢占正在执行的计算，因此，如果对共享数据的访问没有被恰当地同步，则不确定的中断抢占可能会导致数据访问冲突，引起严重的安全问题.据中国空间技术研究院软件产品保证中心统计3，在航天器总装集成测试（assembly，integration&test，AIT）阶段发现的软件质量问题中，约 80%为中断相关的并发缺陷.这些缺陷在经过各种严格的软件测试后仍然被遗漏，是航天嵌入式软件开发中最难以消除的缺陷类型之一.根据文献 4 对航天嵌入式软件并发缺陷的研究，原子性违反是中断并发缺陷中最突出的一类缺陷模式.这种模式指的是程序员对共享数据连续多次访问的原子性执行期望由于中断抢占而遭到破坏，导致非预期的程序行为.中断驱动型软件硬件内存处理器中断控制外部设备外设初始化CPU初始化中断请求直接交互无限循环主循环中断1中断2中断3I/O端口外设计时器Fig.1Interrupt-drivenmodelinaerospaceembeddedsoftware图1航天嵌入式软件的中断驱动模型原子性违反检测是国内外研究的热点，已有方法大多面向多线程程序5-14，但这些方法不能直接应用于中断驱动型航天嵌入式软件，这是由于中断驱动型航天嵌入式软件与多线程程序在并发模型和编程范式方面存在显著差异.例如，任务与中断之间或中断与中断之间具有非对称抢占关系，而线程之间可以互相抢占，异步并发事件及其优先级之间的隐式依赖关系，使用于检测竞争的 happens-before 关系于婷婷等：中断驱动型航天嵌入式软件原子性违反检测方法295复杂化，这导致适用于 2 类程序的缺陷检测方法存在差异；中断驱动型航天嵌入式软件一般缺乏底层并发编程框架，经常采用基于自定义标志变量的同步方式，而多线程程序多采用标准并发控制原语，自定义标志变量的存在极易导致检测结果存在大量误报；此外，中断驱动型航天嵌入式软件依赖大量的内存映射 I/O 地址与外设进行交互，若不能恰当识别这些数据，将使检测结果存在漏报.这些差异对检测方法的有效性具有决定性作用，直接应用针对多线程程序的检测方法面临检测结果不精确的问题.目前，仅有少量工作针对中断驱动型程序中的原子性违反4,15.文献 4 采用静态分析的方法，可扩展到工业规模的嵌入式软件，但存在较多误报；文献15 采用程序模型检验方法，但仅能扩展到百行规模的程序.一方面，文献 4,15 都无法同时实现高精度和高可扩展性；另一方面，中断驱动型航天嵌入式软件的硬件依赖性强且多采用裸机编程，其并发缺陷的表现形式具有领域相关特征，且已有方法的有效性都未经过真实航天嵌入式软件的评估.本文面向真实中断驱动型嵌入式软件中的原子性违反，研究精确且高效的静态检测方法.首先对20092022 年中国空间技术研究院第三方评测机构报告的 82 个原子性违反缺陷进行特征研究，获得该类缺陷在访问交错模式、共享数据访问方式、访问粒度等 3 方面的表现特征.在此基础上，提出了一个精确、高效的静态缺陷检测方法 intAtom-S.该方法的核心思想是逐阶段地采用