Software Model Checking
Software Model Checking
复制标题
软件模型检查
DOI：
10.1145/3103111.3104040
复制
发表时间：
2017
期刊：
影响因子：
--
通讯作者：
Asavoae I
中科院分区：
文献类型：
--
作者：
Asavoae I
在这份立场文件中，我们提倡软件模型检查作为一种技术，适用于移动的应用程序的安全分析。我们的建议是基于我们在Android操作系统的背景下分析应用程序共谋所取得的有希望的结果。一般来说，应用共谋出现在执行威胁时，几个应用一起工作，即，他们交换他们自己无法获得的信息。在这种情况下，我们开发了Kandroid工具，它在K框架内提供了Android/Smali代码语义的编码。Kandroid允许对Android APK文件进行软件模型检查。虽然我们的经验到目前为止仅限于共谋，我们相信这种方法适用于进一步的安全属性以及其他移动的操作系统。
In this position paper we advocate software model checking as a technique suitable for security analysis of mobile apps. Our recommendation is based on promising results that we achieved on analysing app collusion in the context of the Android operating system. Broadly speaking, app collusion appears when, in performing a threat, several apps are working together, i.e., they exchange information which they could not obtain on their own. In this context, we developed the Kandroid tool, which provides an encoding of the Android/Smali code semantics within the K framework. Kandroid allows for software model checking of Android APK files. Though our experience so far is limited to collusion, we believe the approach to be applicable to further security properties as well as other mobile operating systems.