Formal Modeling Of The Security Of The Linux Operating System And Secure Web System

This paper is based on the research of "Bell-LaPadula Model" which is the mostprevalent formal model used currently to implement a secure operating system. We haveimproved this mode f according to the need of reaIization, solved the problem existing inthe originaf model which may incur revelation of information from the high security levelto lower security level, advanced an improved Bell-LaPadula model named of "BLP~+Model". For purpose of implementing, we brought fotward ourselves'11 operating rules,which were derived from the access rules of Bell-LaPadula Model. Based on thisjmproved formal modei, we then implemented the SecLinux, a native secure operatingsystem, of which we own the independent copyright. Finally, in response to the pressingdemand of a secure WWW system, and in order to clarify the ambiguous definition ofsuch system, we advanced the concept of the Secure WWW System according to ourunderstanding. We deveIoped ourselves' security appltcation, SecWeb, which is a WEBserver system of high security level. Such a system constitutes an integrated solution forthe security problems and achieves the goal of coherent security ranging from theoperating systems to the applications.