软件学报

作者：于斌，陆旭，田聪，段振华，张南

单位：于斌，西安电子科技大学 计算机科学与技术学院, 陕西 西安 710071;综合业务网理论与关键技术国家重点实验室(西安电子科技大学), 陕西 西安 71007111,陆旭，西安电子科技大学 计算机科学与技术学院, 陕西 西安 710071;综合业务网理论与关键技术国家重点实验室(西安电子科技大学), 陕西 西安 71007102,田聪，西安电子科技大学 计算机科学与技术学院, 陕西 西安 710071;综合业务网理论与关键技术国家重点实验室(西安电子科技大学), 陕西 西安 71007103,段振华，西安电子科技大学 计算机科学与技术学院, 陕西 西安 710071;综合业务网理论与关键技术国家重点实验室(西安电子科技大学), 陕西 西安 71007104,张南，西安电子科技大学 计算机科学与技术学院, 陕西 西安 710071;综合业务网理论与关键技术国家重点实验室(西安电子科技大学), 陕西 西安 71007105

关键词：SQLite3;API调用序列;命题投影时序逻辑;并行;运行时验证

基金：国家重点研发计划(2018AAA0103202);国家自然科学基金(61732013,62172322,62002290);中央高校基本科研业务费专项基金(XJS210305);陕西省自然科学基础研究计划(2021JQ-208)

作为轻量级的高可靠嵌入式数据库,SQLite3已被广泛应用于航空航天和操作系统等多个安全攸关领域,其提供了丰富灵活API函数以支持用户快速实现项目构建.然而,不正确的API函数调用序列会导致严重后果,包括运行错误、内存泄露和程序崩溃等.为了高效准确地监控SQLite3数据库API函数的正确调用情况,提出了基于多核系统的并行运行时验证方法.该方法首先分析API函数文档,自动挖掘相关API调用序列规约描述,辅助人工将其形式化表达为具有完全正则表达能力的命题投影时序逻辑公式;然后,在程序运行时,采用多任务调度策略,将程序执行产生的状态序列分割并对不同片段并行验证.实验结果表明:该方法能够发现调用SQLite3数据库API函数的30个被验证C程序中,违背API函数调用序列规约的达16个.另外,与传统串行运行时验证方法的对比实验表明,提出的并行运行时验证方法能够有效提高多核系统的验证效率.

来源：2022年第8期

《软件学报》期刊编辑部

查看软件学报杂志2022年第8期