Information Technology Reference
In-Depth Information
( Accessuid = 0
∨
Accessuid = owner (attributes(file'))
∨
Readable
∈
others (attributes(file'))
)"
ReadDirJudgement is a isabelle description of function that judges if a sub-
ject is allowed to read a dir by MAC (Mandatory Access Control) and the usual
Unix file permission constraint.
consts
lookup_secure :: "States => Objects => uid
⇒
('a,'b,'c)env
=> 'c list =>
×
('a,'b,'c)env option
States"
lookup_secure_option :: "States => Objects => uid
⇒
('a,'b,'c)env option
×
=> 'c list => ('a,'b,'c)env option
States"
primrec
(lookup_secure)
"lookup_secure State1 AccessSubject AccessUid (Val a) xs = (if xs = [] then
(Some (Val a), State1) else (None, State1))"
"lookup_secure State1 AccessSubject AccessUid (Env b es) xs = (let State3
= (GetReadTran State1
AccessSubject
(Env b es) ); judgement = (ReadDirJudgement State1
AccessSubject
(Env b es) AccessUid)
in
(case xs of
[] => (Some (Env b es), State1)
|y#ys=>
if (~judgement)
then
(None, State1)
else
lookup_secure_option State3
AccessSubject AccessUid (es y) ys
))"
The function lookup secure search recursively from the specified directory
until the operation is not permitted or the string of path name is exhausted and
the file is got. At the same time, the transition of system state is recorded.
Based on this definition, we can define many delicate theorems about recur-
sive properties of system and prove them.
5
Conclusions
During the formalization of SECIMOS, we strengthen the idea that formal works
is a indispensable part of developing secure operating systems. During the for-
malization procedure, we find some design faults in Linux Security Module and
report the bugs to corresponding mailing-list. We write more than 30 security
theorems and 40 auxiliary lemmas in order to prove them. The intermediate
proof results are more than 150'000 lines long. We encountered many dicul-
ties in theorem proofing; many of them are insurmountable using current Z
tools. This is not expected in the pre-design stage of SECIMOS when we are
