Research On Formally Modelling And Analyzing Of Shielding Systems

Current commodity operating systems are constantly exposed a variety of security vulnerabilities,therefore attackers can affect the execution of security-critical code by attacking the commodity operating systems.For solving the problems,researchers propose shielding systems,that is,a software and hardware system that can be used to protect security-critical code.Specifically,shielding systems protect the two properties of security-critical code-(1)Confidentiality:the execution of security-critical code is invisible to commodity operating systems.The commodity operating system can only observe the input and output of the code;(2)Integrity:commodity operating systems cannot affect the behavior of protected code.Once the security-critical code finish its execution,the output of the code should be the same as the refered expected output.Typical shielding systems include TrustVisor based on hypervisor,TrustICE based on arm TrustZone and Intel SGX technology based on specific hardware.Shielding systems use core management module whose system privilege is higher than commodity operating systems to protect the security-critical code by bypassing the operating systems.With the commercialization of shielding systems,the security of shielding system is got more and more attention.At present,although the code size of shielding systems is far smaller than the code size of commodity operating systems,there is still the possibility of that shielding systems have vulnerabilities,it makes the attacker still have the opportunity to harm the execution of security-critical code.For the problem,an important solution is to conduct formal security analysis of shielding systems.By establishing the theoretical model and theoretical derivation,formal method can provide the theoretical evidence when security properties is incomplete or prove the completeness of security properties.In the field of security analysis,providing formal analysis of software and hardware system is an important method to solve security problems of software and hardware system.Based on the formal method called layer by layer refinement,this thesis focuses on the security analysis of shielding systems,and achieves the following results:(1)We propose a formal analysis method of data confidentiality for shielding systems.The security of security code private data is very important.For example,for the fingerprint unlocking program,once the fingerprint data is leaked,it will bring great harm to the users of the unlocking program.Therefore,the shielding system needs to ensure that the private data of the security code can not be obtained by the attacker.This method supports the analysis of data confidentiality of various shielding systems,such as the shielding system based on virtualization extensions and the shielding system based on ARM TrustZone.This method constructs the general formal constraints of the shielding system in data access and data encryption and decryption,and proves that these constraints is solid under the attack of a Dolev-Yao-type attacker.This method proves the data confidentiality of these systems by proving that the specific shielding system is a refinement of general constraints.Using this method,this thesis analyzes the shielding system TrustVisor and the shielding system OSP,and finds the security defects in the design of these two systems.(2)We propose a formal analysis method of data continuity of shielding system.For a specific security code,if its key data is replaced by an attacker to an old version data,its application effect may be greatly affected.For example,if the accounts in a bank account settlement program can be rolled back by the attacker,it may cause economic losses to the bank users.Therefore,the shielding system needs to ensure that the key data of the security code is always in the latest version or a tolerable old version.This method supports the analysis of a variety of shielding system state continuity protection schemes,such as monotone counter based protection scheme and history record based protection scheme.This method constructs the general formal constraints of the shielding system in data storage and power-off processing,and proves that these constraints is solid under an attacker who maliciously controls the power supply and storage memory.This method proves the data continuity of these systems by proving that a specific shielding system is a refinement of general constraints.This thesis uses this method to prove the state continuity of state continuity protection scheme Ariadne and state continuity protection scheme Menoir,and shows that this method is general.(3)We propose a formal analysis method of memory isolation on ARM platform.It is necessary to ensure that programs can not access memory between each others.Therefore,the arm platform provides a data access control mechanism,so that the security system on the ARM platform can isolate the memory between key programs.This method supports the analysis of memory isolation on various ARM platforms,such as ARM platforms that supporting virtualization extensions and arm platforms that not supporting virtualization extensions.This method gives the general formal expressions of extended paging mechanism and ARM TZASC mechanism on ARM platform,constructs the memory isolation general constraints based on these expressions,and then proves that these constraints are always solid for isolated programs with arbitrary reading and writing.This method proves the memory isolation of specific security systems by proving that they are a refinement of general constraints.This thesis uses this method to prove the memory isolation of shielding system OSP and shielding system Trustice from the view of ARM platform,and shows that this method is general.