US 11,868,481 B2
Method for discovering vulnerabilities of operating system access control mechanism based on model checking
Rui Chang, Hangzhou (CN); Zhuoruo Zhang, Hangzhou (CN); Shaoping Pan, Hangzhou (CN); and Kui Ren, Hangzhou (CN)
Assigned to ZHEJIANG UNIVERSITY, Hangzhou (CN)
Filed by ZHEJIANG UNIVERSITY, Hangzhou (CN)
Filed on Jul. 27, 2021, as Appl. No. 17/386,494.
Application 17/386,494 is a continuation of application No. PCT/CN2020/115227, filed on Sep. 15, 2020.
Claims priority of application No. 202010961713.X (CN), filed on Sep. 14, 2020.
Prior Publication US 2022/0083668 A1, Mar. 17, 2022
Int. Cl. G06F 21/57 (2013.01); G06F 21/55 (2013.01); G06F 21/60 (2013.01)
CPC G06F 21/577 (2013.01) [G06F 21/554 (2013.01); G06F 21/575 (2013.01); G06F 21/604 (2013.01)] 3 Claims
OG exemplary drawing
 
1. A method for discovering vulnerability of access control of an operating system based on model checking, applied in an Advanced RISC Machines (ARM)-Android access control vulnerability discovery process based on model checking and executed by a computer, the computer comprises:
at least one processor, and
a memory configured to store instructions executable by the at least one processor;
wherein the instructions cause the at least one processor to:
Step 1: analyzing an access control mechanism of an ARM platform based on TrustZone hardware isolation, and formalizing access control rules and security attributes to describe a security attribute specification, and providing a security specification by analyzing program semantics and system dynamic behaviors, to describe a specification of operating system access control;
wherein the security attributes comprise atomic security attributes and resource security attributes, and the atomic security attributes comprise privilege definition, access location and user type; and the resource security attributes comprise subject security attributes and object security attributes;
Step 2: analyzing the specification of the operating system access control, defining three basic elements, wherein the three basic elements comprises processes, resources and access control files, constructing corresponding three basic abstract machines TrustZone (TZ) Proc, TZ Res and TZ Policy, determining static and dynamic properties, formally describing processes' access to the resources, establishing and refining an access control model TZ Sys closer to reality based on the corresponding three basic abstract machines TZ Proc, TZ Res and TZ Policy;
Step 3: using a theorem proving tool Atelier B to automatically or interactively prove proof obligations of the access control model to ensure an internal consistency of the abstract machines in a specification initialization, reasoning and refinement implementation stages, to analyze a security of the access control model based on proof results;
Step 4: aiming at possible access rule conflicts in the security specification of the access control model, loading the access control model into a model checking tool ProB for model checking, choosing reasonable verification methods and rules of the model checking tool ProB to perform state space exploration or fixed point calculation, exploring a state space by adopting a Mixed DF/BF algorithm for abstract machines TZ Proc and TZ Res, adopting breadth-first-search for abstract machines TZ Policy and TZ Sys to ensure that all operations are covered, and checking whether there is any invariant violation;
Step 5: based on the security analysis of the access control model in Step 3 and model checking results in Step 4, simulating an actual attack scenario, and detecting security risks and vulnerabilities of access control.