计算机科学技术学报 ›› 2020,Vol. 35 ›› Issue (6): 1295-1311.doi: 10.1007/s11390-020-0541-z

所属专题: Software Systems

• Special Section on Software Systems 2020-Part 2 • 上一篇    下一篇

模式化条件下推系统的可到达性

Xin Li1, Patrick Gardy1, Yu-Xin Deng1,*, and Hiroyuki Seki2   

  1. 1 Shanghai Key Laboratory of Trustworthy Computing, East China Normal University, Shanghai 200062, China;
    2 Graduate School of Informatics, Nagoya University, Nagoya 464-8601, Japan
  • 收稿日期:2020-04-11 修回日期:2020-10-09 出版日期:2020-11-20 发布日期:2020-12-01
  • 通讯作者: Yu-Xin Deng E-mail:yxdeng@sei.ecnu.edu.cn
  • 作者简介:Xin Li is a research associate professor in East China Normal University, Shanghai. She received her Ph.D. degree in information processing from Japan Advanced Institute of Science and Technology, Nomi, in 2007. Her research interests include formal methods and verification, especially about the theory and practice of model checking, and interdisciplinary machine learning research.
  • 基金资助:
    This work was supported by the National Natural Science Foundation of China under Grant Nos. 61802126, 61672229, 61832015 and 62072176, the Ministry of Science and Technology of the People's Republic of China under Grant No. 2018YFC0830400, and Shanghai Pujiang Program under Grant No. 17PJ1402200.

Reachability of Patterned Conditional Pushdown Systems

Xin Li1, Patrick Gardy1, Yu-Xin Deng1,*, and Hiroyuki Seki2        

  1. 1 Shanghai Key Laboratory of Trustworthy Computing, East China Normal University, Shanghai 200062, China;
    2 Graduate School of Informatics, Nagoya University, Nagoya 464-8601, Japan
  • Received:2020-04-11 Revised:2020-10-09 Online:2020-11-20 Published:2020-12-01
  • Contact: Yu-Xin Deng E-mail:yxdeng@sei.ecnu.edu.cn
  • About author:Xin Li is a research associate professor in East China Normal University, Shanghai. She received her Ph.D. degree in information processing from Japan Advanced Institute of Science and Technology, Nomi, in 2007. Her research interests include formal methods and verification, especially about the theory and practice of model checking, and interdisciplinary machine learning research.
  • Supported by:
    This work was supported by the National Natural Science Foundation of China under Grant Nos. 61802126, 61672229, 61832015 and 62072176, the Ministry of Science and Technology of the People's Republic of China under Grant No. 2018YFC0830400, and Shanghai Pujiang Program under Grant No. 17PJ1402200.

1、研究背景(context)。
下推系统由一个有限的状态集合、一个有限但增长不受限的栈,和其上的转换规则构成。该系统由于可以自然地建模递归程序被广泛地应用于程序分析和验证领域。条件下推系统扩展了下推系统,通过使用定义于栈字母表上的正则表达式来进一步约束每个转移规则的应用条件。条件下推系统可用于建模那些需要检查程序运行时栈状态的程序验证问题,例如Java程序在运行时通过栈检查进行动态访问控制、HTML5解析器规范的兼容性检查等。
2、目的(Objective):
条件下推系统的可达性问题已被证明为EXPTIME-完备。本研究的目的是提出一个可建模现有条件下推系统应用问题的子系统,并为其研究设计高效的可达性问题求解算法。
3、方法(Method):
我们研究提出了一个条件下推系统在实际应用中的重要子系统,称为模式化条件下推系统,并为该子系统设计提出了模式引导的可达性分析算法。受实际应用问题启发,我们定义模式为若干基本正则表达式构成的布尔组合。我们扩展了经典的针对下推系统的饱和算法,并动态地计算和跟踪栈所满足的模式,有效地避免了以往算法中可能过早出现的系统状态爆炸问题。最后,系统分析总结了提出算法的时空复杂性,并进行了初步的实验验证。
4、结果(Result&Findings):
本文提出的模式引导算法在最差情况下仍需要指数的时间和空间。我们进一步确定了具有固定参数多项式时空算法的子系统,并实验初步验证了该算法的可扩展性。
5、结论(Conclusions):
结果表明,在给定一个小的固定参数的情况下,我们提出的模式引导算法在解决具有简单模式的条件下推系统的可达到性问题上具有良好的可扩展性。相信我们的工作有助于设计高效的程序验证算法,并有望扩展到具备更复杂模式的条件下推系统。

关键词: 条件下推系统, 模式, 可达性, 饱和算法

Abstract: Conditional pushdown systems (CPDSs) extend pushdown systems by associating each transition rule with a regular language over the stack alphabet. The goal is to model program verification problems that need to examine the runtime call stack of programs. Examples include security property checking of programs with stack inspection, compatibility checking of HTML5 parser specifications, etc. Esparza et al. proved that the reachability problem of CPDSs is EXPTIMEcomplete, which prevents the existence of an algorithm tractable for all instances in general. Driven by the practical applications of CPDSs, we study the reachability of patterned CPDS (pCPDS) that is a practically important subclass of CPDS, in which each transition rule carries a regular expression obeying certain patterns. First, we present new saturation algorithms for solving state and configuration reachability of pCPDSs. The algorithms exhibit the exponential-time complexity in the size of atomic patterns in the worst case. Next, we show that the reachability of pCPDSs carrying simple patterns is solvable in fixed-parameter polynomial time and space. This answers the question on whether there exist tractable reachability analysis algorithms of CPDSs tailored for those practical instances that admit efficient solutions such as stack inspection without exception handling. We have evaluated the proposed approach, and our experiments show that the pattern-driven algorithm steadily scales on pCPDSs with simple patterns.

Key words: conditional pushdown system, pattern, reachability, saturation algorithm

[1] Schwoon S. Model-checking pushdown systems[Ph.D. Thesis]. Department of Computer Science, Technische Universität München, 2002.
[2] Suwimonteerabuth D, Berger F, Schwoon S, Esparza J. jMoped:A test environment for Java programs. In Proc. the 33rd International Conference on Computer-Aided Verification, July 2017, pp.164-167.
[3] Ball T, Rajamani S K. The SLAM project:Debugging system software via static analysis. In Proc. the 29th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, January 2002, pp.1-3.
[4] Reps T W, Schwoon S, Jha S, Melski D. Weighted pushdown systems and their application to interprocedural dataflow analysis. Sci. Comput. Program., 2005, 58(1/2):206-263.
[5] Song F, Touili T. PuMoC:A CTL model-checker for sequential programs. In Proc. the 27th IEEE/ACM International Conference on Automated Software Engineering, September 2012, pp.346-349.
[6] Hague M, Ong C H L. Analysing mu-calculus properties of pushdown systems. In Proc. the 17th International SPIN Workshop on Model Checking Software, September 2010, pp.187-192.
[7] Bouajjani A, Müller-Olm M, Touili T. Regular symbolic analysis of dynamic networks of pushdown systems. In Proc. the 16th International Conference on Concurrency Theory, August 2005, pp.473-487.
[8] Cai X J, Ogawa M. Well-structured pushdown systems. In Proc. the 24th International Conference on Concurrency Theory, August 2013, pp.121-136.
[9] Abdulla P A, Atig M F, Stenman J. Dense-timed pushdown automata. In Proc. the 27th Annual IEEE Symposium on Logic in Computer Science, June 2012, pp.35-44.
[10] Abdulla P A, Atig M F, Stenman J. Computing optimal reachability costs in priced dense-timed pushdown automata. In Proc. the 8th International Conference Language and Automata Theory and Applications, March 2014, pp.62-75.
[11] Esparza J, Kucera A, Schwoon S. Model-checking LTL with regular valuations for pushdown systems. In Proc. the 4th International Symposium on Theoretical Aspects of Computer Software, October 2001, pp.316-339.
[12] Li X, Ogawa M. Conditional weighted pushdown systems and applications. In Proc. the 2010 ACM SIGPLAN Workshop on Partial Evaluation and Program Manipulation, January 2010, pp.141-150.
[13] Minamide Y, Mori S. Reachability analysis of the HTML5 parser specification and its application to compatibility testing. In Proc. the 18th International Symposium on Formal Methods, August 2012, pp.293-307.
[14] Johnson J I, Sergey I, Earl C, Might M, van Horn D. Pushdown flow analysis with abstract garbage collection. Journal of Functional Programming, 2014, 24(2/3):218-283.
[15] Nitta N, Takata Y, Seki H. An efficient security verification method for programs with stack inspection. In Proc. the 8th ACM Conference on Computer and Communications Security, November 2001, pp.68-77.
[16] Shivers O G. Control-flow analysis of higher order languages or taming lambda[Ph.D. Thesis]. Carnegie Mellon University, 1991.
[17] Bravenboer M, Smaragdakis Y. Strictly declarative specification of sophisticated points-to analyses. In Proc. the 24th ACM SIGPLAN Conference on Object Oriented Programming Systems Languages and Applications, October 2009, pp.243-262.
[18] Lhoták O, Hendren L. Context-sensitive points-to analysis:Is it worth it? In Proc. the 15th International Conference on Compiler Construction, March 2006, pp.47-64.
[19] Thanh H V L, Li X. An on-the-fly algorithm for conditional weighted pushdown systems. Journal of Information Processing, 2014, 22(4):1-7.
[20] Uezato Y, Minamide Y. Pushdown systems with stack manipulation. In Proc. the 11th International Symposium on Automated Technology for Verification and Analysis, October 2013, pp.412-426.
[21] Song F, Miao W K, Pu G G, Zhang M. On reachability analysis of pushdown systems with transductions:Application to Boolean programs with call-by-reference. In Proc. the 26th International Conference on Concurrency Theory, September 2015, pp.383-397.
[22] Esparza J, Ganty P. Complexity of pattern-based verification for multithreaded programs. In Proc. the 38th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, January 2011, pp.499-510.
[1] 孔雀屏, 王子彦, 黄袁, 陈湘萍, 周晓聪, 郑子彬, 黄罡. 定义和检测智能合约中低效率的Gas模式[J]. 计算机科学技术学报, 2022, 37(1): 67-82.
[2] Feng Wang, Guo-Jie Luo, Guang-Yu Sun, Yu-Hao Wang, Di-Min Niu, Hong-Zhong Zheng. 在忆阻器中基于模式表示法的二值神经网络权重映射法[J]. 计算机科学技术学报, 2021, 36(5): 1155-1166.
[3] Zeynep Banu Ozger, Nurgul Yuzbasioglu Uslu. 基于三元组重新排序的有效离散人工蜂群SPARQL查询路径优化[J]. 计算机科学技术学报, 2021, 36(2): 445-462.
[4] Dong Liu, Zhi-Lei Ren, Zhong-Tian Long, Guo-Jun Gao, He Jiang. 挖掘设计模式应用场景和相关设计模式对:基于网络发帖的案例研究[J]. 计算机科学技术学报, 2020, 35(5): 963-978.
[5] Monidipa Das, Soumya K. Ghosh. 用于时空分析的数据驱动方法:研究现状综述[J]. 计算机科学技术学报, 2020, 35(3): 665-696.
[6] Wen-Yan Chen, Ke-Jiang Ye, Cheng-Zhi Lu, Dong-Dai Zhou, Cheng-Zhong Xu. 混部容器负载干扰分析:从硬件性能计数器的视角[J]. 计算机科学技术学报, 2020, 35(2): 412-417.
[7] Jiu-Ru Gao, Wei Chen, Jia-Jie Xu, An Liu, Zhi-Xu Li, Hongzhi Yin, Lei Zhao. 针对多子图模式匹配模型的有效框架[J]. 计算机科学技术学报, 2019, 34(6): 1185-1202.
[8] Zhe Liu, Cheng-Jian Qiu, Yu-Qing Song, Xiao-Hong Liu, Juan Wang, Victor S. Sheng. 基于高阶衍生的均值CLBP甲状腺MR图像纹理特征提取[J]. 计算机科学技术学报, 2019, 34(1): 35-46.
[9] Xiao-Dong Dong, Sheng Chen, Lai-Ping Zhao, Xiao-Bo Zhou, Heng Qi, Ke-Qiu Li. 多请求,少开销:分层计价模式下的数据中心间不确定流量传输[J]. 计算机科学技术学报, 2018, 33(6): 1152-1163.
[10] Aakash Ahmad, Claus Pahl, Ahmed B. Altamimi, Abdulrahman Alreshidi. 支持软件体系结构的重用驱动演化的变更日志挖掘模型[J]. 计算机科学技术学报, 2018, 33(6): 1278-1306.
[11] Xin Xu, Jiaheng Lu, Wei Wang. 一种面向复杂符号数据的分层聚类方法及其在辐射源识别上的应用[J]. , 2018, 33(4): 807-822.
[12] Lei Guo, Yu-Fei Wen, Xin-Hua Wang. 社会网络中基于预训练网络嵌入式表示模型的推荐算法研究[J]. , 2018, 33(4): 682-696.
[13] Guo-Wei Wang, Jin-Dou Zhang, Jing Li. 用户异源移动轨迹链接的研究[J]. , 2018, 33(4): 792-806.
[14] Bei-Ji Zou, Yao Chen, Cheng-Zhang Zhu, Zai-Liang Chen, Zi-Qian Zhang. 基于特征选择的有监督视网膜血管动静脉分类[J]. , 2017, 32(6): 1222-1230.
[15] Shi-Ming Guo, Hong Gao. HUITWU:一个在事务数据库中有效挖掘高效用项集的算法[J]. , 2016, 31(4): 776-786.
Viewed
Full text


Abstract

Cited

  Shared   
  Discussed   
[1] 李万学;. Almost Optimal Dynamic 2-3 Trees[J]. , 1986, 1(2): 60 -71 .
[2] C.Y.Chung; 华宣仁;. A Chinese Information Processing System[J]. , 1986, 1(2): 15 -24 .
[3] 章萃; 赵沁平; 徐家福;. Kernel Language KLND[J]. , 1986, 1(3): 65 -79 .
[4] 黄学东; 蔡莲红; 方棣棠; 迟边进; 周立; 蒋力;. A Computer System for Chinese Character Speech Input[J]. , 1986, 1(4): 75 -83 .
[5] 史忠植;. Knowledge-Based Decision Support System[J]. , 1987, 2(1): 22 -29 .
[6] 龚振和;. On Conceptual Model Specification and Verification[J]. , 1987, 2(1): 35 -50 .
[7] 唐同诰; 招兆铿;. Stack Method in Program Semantics[J]. , 1987, 2(1): 51 -63 .
[8] 闵应骅;. Easy Test Generation PLAs[J]. , 1987, 2(1): 72 -80 .
[9] 夏培肃; 方信我; 王玉祥; 严开明; 张廷军; 刘玉兰; 赵春英; 孙继忠;. Design of Array Processor Systems[J]. , 1987, 2(3): 163 -173 .
[10] 乔香珍;. An Efficient Parallel Algorithm for FFT[J]. , 1987, 2(3): 174 -190 .
版权所有 © 《计算机科学技术学报》编辑部
本系统由北京玛格泰克科技发展有限公司设计开发 技术支持:support@magtech.com.cn
总访问量: