一种基于B方法的Android访问控制建模与安全性分析方法

基本信息

申请号 CN202010961708.9 申请日 -
公开(公告)号 CN112100633A 公开(公告)日 2020-12-18
申请公布号 CN112100633A 申请公布日 2020-12-18
分类号 G06F21/60 分类 计算;推算;计数;
发明人 常瑞;苗新亮;任璐;赵永望;任奎;赵俊;单夏烨;任新新;段吉瑞 申请(专利权)人 杭州光通天下网络科技有限公司
代理机构 杭州求是专利事务所有限公司 代理人 杭州光通天下网络科技有限公司;浙江大学
地址 310058 浙江省杭州市西湖区余杭塘路866号
法律状态 -

摘要

摘要 本发明公开一种基于B方法的Android访问控制建模与安全性分析方法,该方法利用形式化语言B对Android访问控制中的安全属性和关键操作进行规约并建模,通过模型检测验证安全性。该方法提供了一种对Android访问控制建模并安全性分析的新方法,针对权限机制进行形式化抽象,设计组件实体抽象机并构建基础模型,在此基础上建立基于调用链、基于IPC追踪和基于细粒度策略的扩展模型,最后根据定理证明及模型检测结果分析该访问控制的安全性,为操作系统的安全机制建模和系统安全证明提供了一种实际有效的途径。