Mousse: A System for Selective Symbolic Execution of Programs with Untamed Environments

被引：9

作者：

Liu, Yingtong ^{[1
]}

Hung, Hsin-Wei ^{[1
]}

Sani, Ardalan Amiri ^{[1
]}

机构：

[1] Univ Calif Irvine, Irvine, CA 92717 USA

来源：

PROCEEDINGS OF THE FIFTEENTH EUROPEAN CONFERENCE ON COMPUTER SYSTEMS (EUROSYS'20) | 2020年

基金：

美国国家科学基金会;

关键词：

selective symbolic execution; program environment; program analysis;

D O I：

10.1145/3342195.3387556

中图分类号：

TP301 [理论、方法];

学科分类号：

081202 ;

摘要：

Selective symbolic execution (SSE) is a powerful program analysis technique for exploring multiple execution paths of a program. However, it faces a challenge in analyzing programs with environments that cannot be modeled nor virtualized. Examples include OS services managing I/O devices, software frameworks for accelerators, and specialized applications. We introduce Mousse, a system for analyzing such programs using SSE. Mousse uses novel solutions to overcome the above challenge. These include a novel process level SSE design, environment-aware concurrent execution, and distributed execution of program paths. We use Mousse to comprehensively analyze five OS services in three smartphones. We perform bug and vulnerability detection, taint analysis, and performance profiling. Our evaluation shows that Mousse outperforms alternative solutions in terms of performance and coverage.

引用

页数：15

共 42 条

[11]

Brown C. S., 2018, 1 PHONE GLASS FINGER

[12]

Cadar C., 2008, P USENIX OSDI

[13]

Ceze L., 2016, COMPUTING COMMUNITY

[14]

Cha S. K., 2012, P IEEE S SEC PRIV S

[15]

Chipounov V., 2011, P ACM ASPLOS

[16]

Chipounov V., 2010, P ACM EUROSYS

[17]

Chipounov V., 2009, P USENIX WORKSH HOT

[18] The S2E Platform: Design, Implementation, and Applications [J].

Chipounov, Vitaly ;

Kuznetsov, Volodymyr ;

Candea, George .

ACM TRANSACTIONS ON COMPUTER SYSTEMS, 2012, 30 (01)

[19]

Ciortea L., 2010, SIGOPS Operating System Review

[20]

Engler D., 2007, P INT S SOFTW TEST A

← 1 2 3 4 5 →