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 条
  • [21] Generating Unit Tests for Floating Point Embedded Software using Compositional Dynamic Symbolic Execution
    Prelgauskas, J.
    Bareisa, E.
    ELEKTRONIKA IR ELEKTROTECHNIKA, 2012, 122 (06) : 19 - 22
  • [22] Automatic Test Pattern Generation for Virtual Hardware Model using Constrained Symbolic Execution
    Mohamed, Nahla
    Safar, Mona
    Wahba, Ayman
    Salem, Ashraf
    2015 10TH INTERNATIONAL DESIGN & TEST SYMPOSIUM (IDT), 2015, : 149 - 150
  • [23] Model -Guided Symbolic 1-1,xecution Testing for etwork Protocol Binary Software
    Wen, Shameng
    Feng, Chao
    Meng, Qingkun
    Zhang, Bin
    Wu, Ligeng
    Tang, Chaojing
    PROCEEDINGS OF THE 2016 INTERNATIONAL CONFERENCE ON PROGRESS IN INFORMATICS AND COMPUTING (PIC), VOL 1, 2016, : 561 - 565
  • [24] Evaluating software quality attributes of communication components in an Automated Guided Vehicle system
    Mårtensson, F
    Grahn, H
    Mattsson, M
    ICECCS 2005: 10TH IEEE INTERNATIONAL CONFERENCE ON ENGINEERING OF COMPLEX COMPUTER SYSTEMS, PROCEEDINGS, 2005, : 550 - 558
  • [25] Path-guided conformance test case generation for models with data and time using symbolic execution techniques
    Bannour, Boutheina
    Lapitre, Arnault
    Le Gall, Pascale
    SCIENCE OF COMPUTER PROGRAMMING, 2025, 243
  • [26] Efficient symbolic model checking of software using partial disjunctive partitioning
    Barner, S
    Rabinovitz, I
    CORRECT HARDWARE DESIGN AND VERIFICATION METHODS, PROCEEDINGS, 2003, 2860 : 35 - 50
  • [27] An execution model for hardwarie/software compilation and its system-level realization
    Lange, Holger
    Koch, Andreas
    2007 INTERNATIONAL CONFERENCE ON FIELD PROGRAMMABLE LOGIC AND APPLICATIONS, PROCEEDINGS, VOLS 1 AND 2, 2007, : 285 - 292
  • [28] Retrieval of software components using a distributed web system
    Behle, A
    Kirchhof, M
    Nagl, M
    Welter, R
    JOURNAL OF NETWORK AND COMPUTER APPLICATIONS, 2002, 25 (03) : 197 - 222
  • [29] Identification of System Software Components Using Clustering Approach
    Shahmohammadi, Gholam Reza
    Jalili, Saeed
    Hasheminejad, Seyed Mohammad Hossein
    JOURNAL OF OBJECT TECHNOLOGY, 2010, 9 (06): : 77 - 98
  • [30] SMARTEST: Effectively Hunting Vulnerable Transaction Sequences in Smart Contracts through Language Model-Guided Symbolic Execution
    So, Sunbeom
    Hong, Seongjoon
    Oh, Hakjoo
    PROCEEDINGS OF THE 30TH USENIX SECURITY SYMPOSIUM, 2021, : 1361 - 1378
12345