Abstract:As part of the Android security model, SEAndroid is critical to assure the security of operating systems. In this study, we propose an approach to analyze SEAndroid policies based on capability dependency graph. Capability dependency graph describes attacker's potential capabilities and the dependency relationships among these capabilities. It also describes the configuration of SEAndroid policies. We collect some security related system facts, and encode the collected data to Prolog predicates. We adopt logic programming to automatically compute a capability dependency graph with driving rules. We enumerate all the attack paths from initial nodes to goal nodes in the capability dependency graph, and categorize the attack paths into attack patterns. We apply our approach to analyze and compare some different versions of Android. We find that with the upgrade of the Android version, the SEAndroid security policy has also been updated. The new SEAndroid provides a stronger constraint and protection for the system, and a experimental attack pattern has been verified in the actual system.