随着移动网、传感网、物联网的飞速发展以及BYOD(Bring Your Own Device)办公模式的日益流行,安装在移动设备和智能终端的Android Apps广泛应用于关乎国计民生的各个领域,涉及金融、税务、工商、交通、电力、社交、通讯等诸多行业,如何保障其安全性已经成为移动互联网乃至物联网发展过程中所面临的重要问题。建立一个有效的行为分析与检测模型是解决这一问题的重要手段之一,也是当前移动安全领域的研究热点。但由于移动终端的动态性、无边界性、处理能力弱、容量有限等固有的特点使传统的安全方法和技术无法直接应用。为了提升并发执行性能,Android Apps广泛采用的多线程和组件间通信等技术,也引入了大量不确定性和安全性问题。现有的行为建模与检测技术在描述行为的交互和并发特征、降低建模的复杂度等方面尚存在不足。针对这些问题,本文的主要研究工作如下。首先,针对现有方法不能有效对Android Apps行为的并发和交互特征进行建模的问题,提出一种基于PiDroid进程代数的行为形式化描述及映射机制。利用逆向分析和代码优化技术,通过控制流和数据流分析提取出行为特征。通过扩展Pi演算构建适合于Android Apps行为建模特点的Pi Droid,并依据PiDroid的语法语义及进程等价概念,将提取的行为特征进行了形式化映射,建立起软件行为与PiDroid进程代数语义的对应关系,奠定了软件行为的形式化基础。其次,针对现有行为检测模型无法有效地表示和检测Android Apps中多线程、事件驱动和异步调度引入的并发行为的问题,给出一种并发行为分析和检测方法。给出并发行为的映射方法并形式化的描述了应用程序中时序、交互、同步和互斥等并发特征。构建了并发行为的演算规则和迁移规则,探讨了依据这些规则进行并发行为检测的方法和步骤,给出了行为检测算法。通过理论分析和实验验证,论证了该方法的精确性和效率。再次,通过深入探讨Android Apps组件间通信机制所引入的交互性问题,提出了一种Android Apps组件间通信的行为分析和检测方法。通过分析数据流图和数据事实得到数据依赖关系,并跟踪跨组件边界的控制流和数据流,构建了组件间通信模型并进行了形式化映射。依据该模型,给出了运行时检测敏感路径触发的算法,并通过分析Intent的异常来检测组件劫持攻击。通过实验验证和对比分析,论证了所提出方法的建模和检测效率以及行为检测的有效性。最后,构建了一个统一的行为检测模型,给出模型的总体框架、行为建模和检测的整体步骤。通过对权限提升攻击案例的分析以及应对策略的讨论,阐述了所提出的行为检测模型的拓展应用方法。