摘要
嵌入式软件的可信性对航天任务的成败至关重要.航天嵌入式软件广泛采用中断驱动的并发机制,不确定的中断抢占可能导致并发缺陷,引发严重的安全问题.研究表明原子性违反是中断并发缺陷中最突出的一类缺陷模式.目前面向中断驱动型嵌入式软件的原子性违反检测方法都无法同时实现高精度和高可扩展性,且其对真实航天嵌入式软件的有效性尚未得到证实.为了有效提升检测该类缺陷的精度与效率,对82个航天嵌入式软件原子性违反进行实证研究,获得该类缺陷在原子区范围、中断嵌套层数、访问交错模式、共享数据访问方式、访问粒度等5个方面的表现特征.并在此基础上,提出一个精确、高效的原子性违反静态检测方法intAtom-S.首先,基于一个由数值不变式参数化的细粒度内存访问模型,引入基于规则的方法剔除标志变量访问,并采用抽象解释进行精确的共享数据分析,该分析能将共享数据访问粒度精确至数组元素,并可识别共享的内存映射I/O地址.然后,使用轻量级数据流分析技术匹配符合缺陷访问交错模式的所有并发三次访问序,作为潜在的原子性违反缺陷候选.最后,采用基于路径条件的约束求解对缺陷候选中的串行访问对和并发三次访问序进行路径可行性分析,逐步消除误报,得到最终的原子性违反结果.在基准测试集和8个真实航天嵌入式软件上的实验表明,与目前最先进的方法相比,intAtom-S误报率降低了72％,检测效率提高了3倍.此外,该方法能够快速完成对真实航天嵌入式软件的分析,平均误报率仅为8.9％,并发现了23个已被开发人员确认的缺陷.
NETL
NSTL
维普
万方数据