一種基于B方法的Android訪問控制建模與安全性分析方法

基本信息

申請?zhí)?/td> CN202010961708.9 申請日 -
公開(公告)號 CN112100633A 公開(公告)日 2020-12-18
申請公布號 CN112100633A 申請公布日 2020-12-18
分類號 G06F21/60 分類 計算;推算;計數(shù);
發(fā)明人 常瑞;苗新亮;任璐;趙永望;任奎;趙俊;單夏燁;任新新;段吉瑞 申請(專利權(quán))人 杭州光通天下網(wǎng)絡(luò)科技有限公司
代理機構(gòu) 杭州求是專利事務(wù)所有限公司 代理人 杭州光通天下網(wǎng)絡(luò)科技有限公司;浙江大學(xué)
地址 310058 浙江省杭州市西湖區(qū)余杭塘路866號
法律狀態(tài) -

摘要

摘要 本發(fā)明公開一種基于B方法的Android訪問控制建模與安全性分析方法,該方法利用形式化語言B對Android訪問控制中的安全屬性和關(guān)鍵操作進行規(guī)約并建模,通過模型檢測驗證安全性。該方法提供了一種對Android訪問控制建模并安全性分析的新方法,針對權(quán)限機制進行形式化抽象,設(shè)計組件實體抽象機并構(gòu)建基礎(chǔ)模型,在此基礎(chǔ)上建立基于調(diào)用鏈、基于IPC追蹤和基于細粒度策略的擴展模型,最后根據(jù)定理證明及模型檢測結(jié)果分析該訪問控制的安全性,為操作系統(tǒng)的安全機制建模和系統(tǒng)安全證明提供了一種實際有效的途徑。