Analyzing system software components using API model guided symbolic execution
Analyzing system software components using API model guided symbolic execution
复制标题
使用 API 模型引导的符号执行分析系统软件组件
DOI：
10.1007/s10515-020-00276-5
复制
发表时间：
2020
影响因子：
3.4
通讯作者：
Bai, Ken
中科院分区：
文献类型：
--
作者：
Yavuz, Tuba;Bai, Ken
分析现实世界的软件是具有挑战性的，由于复杂的软件框架或API，他们dependent.In本文中，我们提出了一个工具，PROMPT，便于分析的软件组件usingAPI模型引导符号执行。PROMPT有一个规范组件PROSE，它允许用户定义一个API模型，该模型由一组数据约束和生命周期规则组成，这些规则定义顺序组合的API函数之间的控制流约束。给定一个PROSE模型和一个软件组件，PROMPT象征性地执行组件，同时强制执行指定的API模型。PROMPT已在KLEE符号执行引擎之上实现，并已应用于Linux设备驱动程序，包括视频、声音和网络子系统，以及BlueZ的一些易受攻击的组件，BlueZ是Linux内核的蓝牙协议栈的实现。PROMPT在一些分析的系统软件组件中检测到两个新的和四个已知的内存漏洞。
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.
登录
查看更多内容
DOI：
--
发表时间：
2009
期刊：
International Journal on Software Tools for Technology Transfer (STTT)
影响因子：
--
作者：
S. Chatterjee;Shuvendu K. Lahiri;S. Qadeer;Zvonimir Rakamaric
通讯作者：
Zvonimir Rakamaric
用于 JavaScript 静态分析的不透明代码自动建模
DOI：
--
发表时间：
2019
期刊：
Fundamental Approaches to Software Engineering
影响因子：
--
作者：
Joonyoung Park;Alexander Jordan;Sukyoung Ryu
通讯作者：
Sukyoung Ryu
用于操作系统内核模块静态验证的可配置工具集
影响因子：
0.7
作者：
I. Zakharov;M. Mandrykin;V. Mutilin;E. Novikov;A. Petrenko;A. Khoroshilov
通讯作者：
A. Khoroshilov
FrAngel：具有控制结构的基于组件的合成
DOI：
--
发表时间：
2018
期刊：
Proc. ACM Program. Lang.
影响因子：
--
作者：
Kensen Shi;J. Steinhardt;Percy Liang
通讯作者：
Percy Liang
用于程序分析的分区内存模型
DOI：
--
发表时间：
2017
期刊：
International Conference on Verification, Model Checking and Abstract Interpretation
影响因子：
--
作者：
Wen Wang;Clark W. Barrett;Thomas Wies
通讯作者：
Thomas Wies