• 主题
高级搜索  >
历史搜索 清空历史
首页> 外文学位 >Design and Analysis of Mobile Operating System Security Architecture using Formal Methods
【24h】

Design and Analysis of Mobile Operating System Security Architecture using Formal Methods

机译：基于形式化方法的移动操作系统安全体系结构设计与分析

获取原文
获取原文并翻译 | 示例
页面导航
  • 摘要
  • 著录项
  • 相似文献
  • 相关主题

摘要

The Android operating system (OS) is now used in the majority of mobile devices. Hence, Android security is an important issue to handle. In this work, we tackle the problem using two separate approaches: directly modifying Android OS and developed a framework to provide a guarantee of non-interference.;Firstly, we present a design and an implementation of a security policy specification language based on metric linear-time temporal logic (MTL) to specify timing- dependent security policies. The design of the language is driven by the problem of runtime monitoring of applications in mobile devices. A main case of the study is the privilege escalation attack in the Android OS, where an unprivileged app gains access to privileged resource or functionalities through indirect flow. To capture these attacks, we extend MTL with recursive definitions to express call chains between apps. We then show how our language design can be used to specify policies to detect privilege escalation under various fine-grained constraints. We present a new algorithm for monitoring safety policies written in our specification language. The monitor does not need to store the entire history of events generated by the apps. We modified the Android OS kernel to allow us to insert our generated monitors modularly. We have tested the modified OS (LogicDroid) on an actual device, and show that it is effective in detecting policy violations. Furthermore, LogicDroid is able to prevent a previously unknown exploit to breach Android security which allows an unprivileged application to access certain critical and privileged functionalities of an Android phone, such as making phone calls, terminating phone calls, and sending SMS, without having to ask any permissions to do so.;Subsequently, we provided a framework to ensure non-interference properties of DEX bytecode. Each application in Android runs in an instance of the Dalvik virtual machine, which is a register-based virtual machine (VM). Most applications for Android are developed using Java, compiled to Java bytecode and further into DEX bytecode. Following a methodology that has been developed for Java byte-code certification by Barthe et al., we developed a type-based method for certifying non-interference property of a DEX program. To this end, we develop a formal operational semantics of the Dalvik VM, a type system for DEX bytecode, and prove the soundness of the type system with respect to a notion of non-interference. We have also formalized the proof of a subset of DEX in Coq for an additional guarantee that our proof is correct.;We then study the translation process from Java bytecode to DEX bytecode, as implemented in the dx tool in the Android SDK. We show that an abstracted version of the translation from Java bytecode to DEX bytecode preserves the non-interference property. More precisely, we show that if the Java bytecode is typable in Barthe et al.'s type system, then its translation is typable in our type system. This result opens up the possibility to leverage existing bytecode verifiers for Java to certify non-interference properties of Android bytecode.
机译：现在，大多数移动设备都使用Android操作系统（OS）。因此，Android安全性是一个重要的问题。在这项工作中，我们使用两种不同的方法来解决该问题：直接修改Android OS并开发了一个提供不干扰保证的框架。首先，我们提出了基于度量线性的安全策略规范语言的设计和实现时态逻辑（MTL）来指定时序相关的安全策略。语言的设计受到移动设备中应用程序运行时监视问题的驱动。该研究的主要案例是Android操作系统中的特权升级攻击，其中非特权应用通过间接流获得对特权资源或功能的访问权。为了捕获这些攻击，我们使用递归定义扩展了MTL，以表达应用之间的调用链。然后，我们展示如何使用我们的语言设计来指定策略，以检测各种细粒度约束下的特权升级。我们提出了一种新的算法，用于监控以规范语言编写的安全策略。监视器不需要存储应用程序生成的事件的全部历史记录。我们修改了Android OS内核，以允许我们以模块化方式插入生成的监视器。我们已经在实际设备上测试了修改后的OS（LogicDroid），并表明它可以有效地检测到策略违规。此外，LogicDroid能够阻止以前未知的利用Android安全的漏洞，该漏洞允许未经特权的应用程序访问Android手机的某些关键和特权功能，例如拨打电话，终止电话和发送SMS，而无需询问随后，我们提供了一个框架来确保DEX字节码的无干扰属性。 Android中的每个应用程序都在Dalvik虚拟机实例中运行，该实例是基于寄存器的虚拟机（VM）。 Android的大多数应用程序都是使用Java开发的，编译为Java字节码，然后再编译为DEX字节码。遵循Barthe等人针对Java字节码认证开发的方法，我们开发了一种基于类型的方法来认证DEX程序的无干扰性。为此，我们开发了Dalvik VM（一种用于DEX字节码的类型系统）的形式化操作语义，并针对非干扰的概念证明了类型系统的正确性。我们还正式确定了Coq中DEX子集的证明，以确保我们的证明正确无误。;然后，我们研究了从Java字节码到DEX字节码的转换过程，这是在Android SDK中的dx工具中实现的。我们显示了从Java字节码到DEX字节码的转换的抽象版本保留了非干扰属性。更准确地说，我们表明，如果Java字节码在Barthe等人的类型系统中是可键入的，则其翻译在我们的类型系统中也是可键入的。该结果为利用现有的Java字节码验证程序验证Android字节码的无干扰属性提供了可能性。

著录项

  • 作者

    Gunadi, Hendra.;

  • 作者单位

    The Australian National University (Australia).;

  • 授予单位 The Australian National University (Australia).;
  • 学科 Computer science.
  • 学位 Ph.D.
  • 年度 2017
  • 页码 231 p.
  • 总页数 231
  • 原文格式 PDF
  • 正文语种 eng
  • 中图分类 生理学;
  • 关键词

相似文献

  • 外文文献
  • 中文文献
  • 专利
获取原文

客服邮箱：kefu@zhangqiaokeyan.com

京公网安备：11010802029741号 ICP备案号：京ICP备15016152号-6 六维联合信息科技 (北京) 有限公司©版权所有

  • 客服微信

  • 服务号