Because of the high-level abstraction,insufficient description of database states and constraints,it was difficult to find the tiny flaws in design and implementation.Based on PVS,a method for formal description and analysis of data-base security policy was proposed,which was more close to the actual database,more widely used in reality,and more complete in describing the safe properties,more extendible of the model,and ensure the efficiency of modeling and veri-fication.Finally,this method is applied in the security policy modeling and analyzing of BeyonDB,which is a commer-cial database,find some security risks in the system design,and thereby verify its effectiveness.