面向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:
  • 摘要
  • | |
  • 访问统计
  • |
  • 参考文献 [39]
  • |
  • 相似文献 [20]
  • | | |
  • 文章评论
    摘要:

    作为轻量级的高可靠嵌入式数据库,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.

    参考文献
    [1] Lee K, Won Y.Smart layers and dumb result:IO characterization of an Android-based smartphone.In:Proc.of the 10th ACM Int'l Conf.on Embedded Software.Tampere:ACM, 2012.23-32.
    [2] Haldar S.Inside Sqlite.O'Reilly Media Inc., 2007.
    [3] Nadi S, Krüger S, Mezini M, et al.Jumping through hoops:Why do Java developers struggle with cryptography APIs?In:Proc.of the 38th Int'l Conf.on Software Engineering.Austin:ACM, 2016.935-946.
    [4] Li Z, Wu JZ, Li MS.Study on key issues in API usage.Ruan Jian Xue Bao/Journal of Software, 2018, 29(6):1716-1738(in Chinese with English abstract).http://www.jos.org.cn/1000-9825/5541.htm[doi:10.13328/j.cnki.jos.005541]
    [5] Li X, Hoover HJ, Rudnicki P.API conformance verification for Java programs.In:Proc.of the 12th Int'l Conf.on Formal Engineering Methods.Shanghai:Springer, 2010.188-203.
    [6] Rieken J.Design by contract for Java-revised[MS.Thesis].Department fürInformatik, Universität Oldenburg, 2007.
    [7] DeLine R, Fähndrich M.Typestates for objects.In:Proc.of the 18th European Conf.on Object-Oriented Programming.Oslo:Springer, 2004.465-490.
    [8] Bierhoff K, Beckman NE, Aldrich J.Practical API protocol checking with access permissions.In:Proc.of the 23rd European Conf.on Object-Oriented Programming.Genoa:Springer, 2009.195-219.
    [9] Post H, Küchlin W.Integrated static analysis for Linux device driver verification.In:Proc.of the 6th Int'l Conf.on Integrated Formal Methods.Oxford:Springer, 2007.518-537.
    [10] Rubanov V, Silakov D.Certification infrastructure for the Linux standard base (LSB).In:Proc.of the 2nd Int'l Workshop on Foundations and Techniques for Open Source Software Certification.2008.79.
    [11] Hallé S, Bultan T, Hughes G, et al.Runtime verification of Web service interface contracts.Computer, 2010, 43(3):59-66.
    [12] Ramsokul P, Sowmya A.Aseha:A framework for modelling and verification ofweb services protocols.In:Proc.of the 4th IEEE Int'l Conf.on Software Engineering and Formal Methods.Pune:IEEE, 2006.196-205.
    [13] Ramsokul P, Sowmya A.A sniffer based approach to WS protocols conformance checking.In:Proc.of the 5th Int'l Symp.on Parallel and Distributed Computing.Timisoara:IEEE, 2006.58-65.
    [14] Bartocci E, Falcone Y, Francalanza A, et al.Introduction to runtime verification.In:Lectures on Runtime Verification.Springer, 2018.1-33.
    [15] Meredith PON, Jin D, Griffith D, et al.An overview of the MOP runtime verification framework.Int'l Journal on Software Tools for Technology Transfer, 2012, 14(3):249-289.
    [16] Li XS, Tao XP, Song W.Runtime verification of spatio-temporal properties for pervasive computing applications.Ruan Jian Xue Bao/Journal of Software, 2018, 29(6):1622-1634(in Chinese with English abstract).http://www.jos.org.cn/1000-9825/5466.htm[doi:10.13328/j.cnki.jos.005466]
    [17] Basin D, Klaedtke F, Zălinescu E.Runtime verification of temporal properties over out-of-order data streams.In:Proc.of the 29th Int'l Conf.on Computer Aided Verification.Heidelberg:Springer, 2017.356-376.
    [18] Pnueli A.The temporal logic of programs.In:Proc.of the 18th Annual Symp.on Foundations of Computer Science.Rhode Island:IEEE, 1977.46-57.
    [19] Clarke EM, Emerson EA.Design and synthesis of synchronization skeletons using branching time temporal logic.In:Proc.of the Workshop on Logic of Programs.New York:Springer, 1981.52-71.
    [20] Leucker M, Schallhart C.A brief account of runtime verification.The Journal of Logic and Algebraic Programming, 2009, 78(5):293-303.
    [21] Falcone Y, Havelund K, Reger G.A tutorial on runtime verification.Engineering Dependable Software Systems, 2013, 34:141-175.
    [22] Tian C, Duan ZH.Propositional projection temporal logic, Buchi automata and ω-regular expressions.In:Proc.of the 5th Int'l Conf.on Theory and Applications of Models of Computation.Xi'an:Springer, 2008.47-58.
    [23] Duan ZH.An extended interval temporal logic and a framing technique for temporal logic programming[Ph.D.Thesis].Newcastle:University of Newcastle Upon Tyne, 1996.
    [24] Lattner C, Adve V.LLVM:A compilation framework for lifelong program analysis&transformation.In:Proc.of the 2nd Int'l Symp.on Code Generation and Optimization.San Jose:IEEE, 2004.75-88.
    [25] Yu B.Research on efficient runtime verification for MSVL programs[Ph.D.Thesis].Xi'an:Xidian University, 2019.
    [26] Yu B, Zhang N, Lu X, et al.Runtime verification approach for DoS attack detection in edge servers.Journal on Communications, 2021, 42(9):75-86(in Chinese with English abstract).http://www.infocomm-journal.com/txxb/CN/10.11959/j.issn.1000-436x.2021169
    [27] Strom RE, Yemini S.Typestate:A programming language concept for enhancing software reliability.IEEE Trans.on Software Engineering, 1986, 12(1):157-171.
    [28] Gardarin G, Melkanoff M.Proving consistency of database transactions.In:Proc.of the 5th Int'l Conf.on Very Large Data Bases.Rio de Janeiro:IEEE, 1979.291-298.
    [29] Casanova MR, Bernstein PA.A formal system for reasoning about programs accessing a relational database.ACM Trans.on Programming Languages and Systems, 1980, 2(3):386-414.
    [30] Benedikt M, Griffin T, Libkin L.Verifiable properties of database transactions.Information and Computation, 1998, 147(1):57-88.
    [31] Benzaken V, Cerrito S, Praud S.Static verification of dynamical integrity constraints:A semantics based approach.Networking and Information Systems Journal, 2000.
    [32] Alagić S, Fazeli A.Verifiable object-oriented transactions.In:Proc.of the Concurrent Objects and Beyond.Springer, 2014.251-275.
    [33] Benzaken V, Contejean E, Keller C, et al.A Coq formalisation of SQL's execution engines.In:Proc.of the 9th Int'l Conf.on Interactive Theorem Proving.Oxford:Springer, 2018.88-107.
    [34] Malecha G, Morrisett G, Shinnar A, et al.Toward a verified relational database management system.In:Proc.of the 37th ACM SIGPLAN-SIGACT Symp.on Principles of Programming Languages.Madrid:ACM, 2010.237-248.
    附中文参考文献:
    [4] 李正,吴敬征,李明树.API使用的关键问题研究.软件学报, 2018, 29(6):1716-1738.http://www.jos.org.cn/1000-9825/5541.htm[doi:10.13328/j.cnki.jos.005541]
    [16] 李晅松,陶先平,宋巍.普适计算应用时空性质的运行时验证.软件学报, 2018, 29(6):1622-1634.http://www.jos.org.cn/1000-9825/5466.htm[doi:10.13328/j.cnki.jos.005466]
    [25] 于斌.MSVL程序的高效运行时验证方法研究[博士学位论文].西安:西安电子科技大学, 2019.
    [26] 于斌,张南,陆旭,段振华,田聪.基于运行时验证的边缘服务器DoS攻击检测方法.通信学报, 2021, 42(9):75-86.http://www.infocomm-journal.com/txxb/CN/10.11959/j.issn.1000-436x.2021169
    引证文献
    网友评论
    网友评论
    分享到微博
    发 布
引用本文

于斌,陆旭,田聪,段振华,张南.面向SQLite3数据库API调用序列的并行运行时验证方法.软件学报,2022,33(8):2755-2768

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

京公网安备 11040202500063号