面向SQLite3数据库API调用序列的并行运行时验证方法  

Parallel Runtime Verification for Calling Sequences of SQLite3 Database APIs

作　　者：于斌 陆旭 田聪[1,2] 段振华[1,2] 张南 YU Bin;LU Xu;TIAN Cong;DUAN Zhen-Hua;ZHANG Nan(School of Computer Science and Technology,Xidian University,Xi’an 710071,China;State Key Laboratory of Integrated Service Networks(Xidian University),Xi’an 710071,China)

机构地区：[1]西安电子科技大学计算机科学与技术学院,陕西西安710071 [2]综合业务网理论与关键技术国家重点实验室(西安电子科技大学),陕西西安710071

出　　处：《软件学报》2022年第8期2755-2768,共14页Journal of Software

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

摘　　要：作为轻量级的高可靠嵌入式数据库,SQLite3已被广泛应用于航空航天和操作系统等多个安全攸关领域,其提供了丰富灵活API函数以支持用户快速实现项目构建.然而,不正确的API函数调用序列会导致严重后果,包括运行错误、内存泄露和程序崩溃等.为了高效准确地监控SQLite3数据库API函数的正确调用情况,提出了基于多核系统的并行运行时验证方法.该方法首先分析API函数文档,自动挖掘相关API调用序列规约描述,辅助人工将其形式化表达为具有完全正则表达能力的命题投影时序逻辑公式;然后,在程序运行时,采用多任务调度策略,将程序执行产生的状态序列分割并对不同片段并行验证.实验结果表明:该方法能够发现调用SQLite3数据库API函数的30个被验证C程序中,违背API函数调用序列规约的达16个.另外,与传统串行运行时验证方法的对比实验表明,提出的并行运行时验证方法能够有效提高多核系统的验证效率.As a lightweight and highly reliable embedded database,SQLite3 has been widely used in many security-critical areas such as aerospace and operating systems.It provides rich and flexible API functions to support users to quickly construct projects.However,an incorrect API function call sequence can cause serious consequences,including runtime errors,memory leaks,orprogram crashes.In order to efficiently and accurately monitor the correct call of SQLite3 database API functions,this paper presents a parallel runtime verification approachfor multi-core machines.This approach first analyzes API function documents,automatically mines API call specification descriptions,and assists humans to formalize them as propositional projection temporal logic formulaswith the full regular expressiveness.Then,while the program is running,the multi-task scheduling strategy is employed to divide the generatedstate sequence into several segments and achieve the parallel verification for different segments.Experimental results show that the proposed approachis able to find that among the 30 programs invoking SQLite3 database API functions,there are 16 violations of the API call sequence specifications,with a violation rate of 53%.In addition,with comparative experiments of traditional sequential runtime verification approaches,it is shown that the proposed parallel runtime verification in this study can effectively improve the verification efficiency in a multi-core system.

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

分 类 号：TP311[自动化与计算机技术—计算机软件与理论]