Download complete thesis as PDF

The next theorem, SecureSystem, states three properties for a System to be
secure. Firstly, if the current state is secure, a transition will result in the next state also
being secure. Also, an actualization of a flow in the system due to a read or write
operation for a particular system state implies that the flow is enabled for that system
state. From the two theorems, we would also be able to deduce that starting from an
empty secure state, all subsequent states should be secure based on the properties defined
in SecureSystem.
op secure_write_transition(S1: State, at: Flow): Boolean =
if (Write in? at.fset) then
let S' = (write_op (at.subj, at.obj) S1).2 in
((get_resource_memory (at.obj) S1).1 ~=
(get_resource_memory (at.obj) S').1) =>
(currently_accessible? at S1).1
else
false
op secure_read_transition(S1: State, at: Flow): Boolean =
if (Read in? at.fset) then
let S' = (read_op (at.subj, at.obj) S1).2 in
((get_resource_memory (at.subj) S1).1 ~=
(get_resource_memory (at.subj) S').1) =>
(currently_accessible? at S1).1
else
false
op securestate?(S: State, policy: Policy): Boolean =
fa(at: Flow) at in? S.atset
=> access_secure?(policy.srm, policy.bbm, at)
theorem EmptySecure is
fa(sys: System)
sys.sysstate.atset = empty &&
securestate?(sys.sysstate, sys.pol)
theorem SecureSystem is
fa(S: State, input:Input, sys: System)
securestate?(S, sys.pol)
=> securestate?((transition (input, sys) S).2, sys.pol)
&&
secure_write_transition(S, input.at)
&&
secure_read_transition(S, input.at)
Figure 90
Security Theorems for secure state
77