Analyzing system software components using API model guided symbolic execution

被引：3
|
作者：
Yavuz, Tuba [1 ]
Bai, Ken [2 ]
机构：
[1] Univ Florida, ECE Dept, Benton 321, Gainesville, FL 32611 USA
[2] Univ Florida, ECE Dept, Larsen 234, Gainesville, FL 32611 USA
来源：
AUTOMATED SOFTWARE ENGINEERING | 2020年 / 27卷 / 3-4期
基金：
美国国家科学基金会;
关键词：
Symbolic execution; API modeling; Specification; CHECKING;
D O I：
10.1007/s10515-020-00276-5
中图分类号：
TP31 [计算机软件];
学科分类号：
081202 ; 0835 ;
摘要：
Analyzing real-world software is challenging due to complexity of the software frameworks or APIs they depend on. In this paper, we present a tool, PROMPT, that facilitates the analysis of software components usingAPI model guided symbolic execution. PROMPT has a specification component, PROSE, that lets users define an API model, which consists of a set of data constraints and life-cycle rules that define control-flow constraints among sequentially composed API functions. Given a PROSE model and a software component, PROMPT symbolically executes the component while enforcing the specified API model. PROMPT has been implemented on top of the KLEE symbolic execution engine and has been applied to Linux device drivers from the video, sound, and network subsystems and to some vulnerable components of BlueZ, the implementation of the Bluetooth protocol stack for the Linux kernel. PROMPT detected two new and four known memory vulnerabilities in some of the analyzed system software components.
引用
收藏
页码：329 / 367
页数：39
相关论文
共 50 条
  • [31] Proof assisted bounded and unbounded symbolic model checking of software and system models
    Krings, Sebastian
    Leuschel, Michael
    SCIENCE OF COMPUTER PROGRAMMING, 2018, 158 : 41 - 63
  • [32] A software of generating a symbolic circuit model with computers forwireless power transmission system
    Hirata, Takuya
    Yamamoto, Yuta
    Yamaguchi, Kazuya
    Hodaka, Ichijo
    WSEAS Transactions on Circuits and Systems, 2014, 13 : 266 - 273
  • [33] About estimation software reliability using Musa basic Execution Time Model
    Popescu, M
    Truta, M
    Bica, MS
    6TH WORLD MULTICONFERENCE ON SYSTEMICS, CYBERNETICS AND INFORMATICS, VOL XVIII, PROCEEDINGS: INFORMATION SYSTEMS, CONCEPTS AND APPLICATIONS OF SYSTEMICS, CYBERNETICS AND INFORMATICS, 2002, : 135 - 137
  • [34] Using graph transformation as the semantical model for software process execution in the APSEE environment
    Reis, CAL
    Reis, RQ
    de Abreu, MA
    Schlebbe, H
    Nunes, DJ
    GRAPH TRANSFORMATIONS, PROCEEDINGS, 2002, 2505 : 254 - 269
  • [35] Abstraction-guided model checking using symbolic IDA* and heuristic synthesis
    Qian, KR
    Nymeyer, A
    Susanto, S
    FORMAL TECHNIQUES FOR NETWORKED AND DISTRIBUTED SYSTEMS - FORTE 2005, 2005, 3731 : 275 - 289
  • [36] Calibration of PIXE system using GUPIXWIN software package for analyzing spectra
    Yu, Ling-Da
    Wang, Guang-Fu
    Zhu, Guang-Hua
    Yuanzineng Kexue Jishu/Atomic Energy Science and Technology, 2010, 44 (01): : 75 - 79
  • [37] Analyzing software system quality risk using Bayesian Belief Network
    Yong, Hu
    Juhua, Chen
    Huang, Jiaxing
    Liu, Mei
    Xie, Kang
    GRC: 2007 IEEE INTERNATIONAL CONFERENCE ON GRANULAR COMPUTING, PROCEEDINGS, 2007, : 93 - +
  • [38] Analyzing system reliability using conflicting bifuzzy failure rates of the components
    Chaube, Shshank
    ENGINEERING APPLICATIONS OF ARTIFICIAL INTELLIGENCE, 2023, 126
  • [39] On the estimation of reliability of a software system using reliabilities of its components
    Krishnamurthy, S
    Mathur, AP
    EIGHTH INTERNATIONAL SYMPOSIUM ON SOFTWARE RELIABILITY ENGINEERING, PROCEEDINGS, 1997, : 146 - 155
  • [40] Development of power system analysis software using object components
    Nor, K. M.
    Mokhlis, H.
    Suyono, H.
    Abdel-Akher, M.
    Rashid, A-. H. A-.
    Gani, Taufiq A.
    TENCON 2005 - 2005 IEEE REGION 10 CONFERENCE, VOLS 1-5, 2006, : 1267 - 1272
12345