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

作者简介:

于斌(1990-),男,博士,讲师,CCF专业会员,主要研究领域为模型检测,运行时验证;
段振华(1948-),男,博士,教授,博士生导师,CCF会士,主要研究领域为时序逻辑,形式化方法,高可信嵌入式系统;
陆旭(1985-),男,博士,副教授,CCF专业会员,主要研究领域为智能规划,模型检测,程序验证;
张南(1984-),女,博士,副教授,博士生导师,CCF高级会员,主要研究领域为形式化验证,模型检测;
田聪(1981-),女,博士,教授,博士生导师,CCF杰出会员,主要研究领域为可信软件的基础理论与方法,人工智能系统安全.

通讯作者:

田聪,E-mail:ctian@mail.xidian.edu.cn;段振华,E-mail:zhhduan@mail.xidian.edu.cn

中图分类号:

TP311

基金项目:

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


Parallel Runtime Verification for Calling Sequences of SQLite3 Database APIs
Author:
Affiliation:

Fund Project:

  • 摘要
  • |
  • 图/表
  • |
  • 访问统计
  • |
  • 参考文献
  • |
  • 相似文献
  • |
  • 引证文献
  • |
  • 资源附件
  • |
  • 文章评论
    摘要:

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

    Abstract:

    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调用序列的并行运行时验证方法.软件学报,2022,33(8):2755-2768

复制
分享
文章指标
  • 点击次数:
  • 下载次数:
  • HTML阅读次数:
  • 引用次数:
历史
  • 收稿日期:2021-06-26
  • 最后修改日期:2021-10-14
  • 录用日期:
  • 在线发布日期: 2022-01-28
  • 出版日期: 2022-08-06
您是第位访问者
版权所有:中国科学院软件研究所 京ICP备05046678号-3
地址:北京市海淀区中关村南四街4号,邮政编码:100190
电话:010-62562563 传真:010-62562533 Email:jos@iscas.ac.cn
技术支持:北京勤云科技发展有限公司

京公网安备 11040202500063号