equal
deleted
inserted
replaced
298 the opposite: if a policy does not meet an access property, then |
298 the opposite: if a policy does not meet an access property, then |
299 there is a sequence of events that will violate this property in our |
299 there is a sequence of events that will violate this property in our |
300 model of the operating system. With these two results in place we |
300 model of the operating system. With these two results in place we |
301 can show that a static policy check is sufficient in order to |
301 can show that a static policy check is sufficient in order to |
302 guarantee the access properties before running the system. Again as |
302 guarantee the access properties before running the system. Again as |
303 far as we know, no such check that is the operating |
303 far as we know, no such check has been designed and proved correct |
304 system behaviour has been designed before. |
304 before. |
305 |
305 |
306 |
306 |
307 %Specified dynamic behaviour of the system; |
307 %Specified dynamic behaviour of the system; |
308 %we specified a static AC model; designed a tainted relation for |
308 %we specified a static AC model; designed a tainted relation for |
309 %the system; proved that they coincide. |
309 %the system; proved that they coincide. |
533 |
533 |
534 \noindent |
534 \noindent |
535 Clearly the operating system should only allow to clone a process @{text p} if the |
535 Clearly the operating system should only allow to clone a process @{text p} if the |
536 process is currently alive. The cloned process will get the process |
536 process is currently alive. The cloned process will get the process |
537 ID generated by the function @{term new_proc}. This process ID should |
537 ID generated by the function @{term new_proc}. This process ID should |
538 not already exist. Therefore we define @{term new_proc} as |
538 not already exist. Therefore we define @{term new_proc} as *} |
539 |
539 |
540 (* HERE ????? chunhan *) |
540 (* HERE ????? chunhan *) |
541 |
541 text {* |
542 \begin{isabelle}\ \ \ \ \ %%% |
542 \begin{isabelle}\ \ \ \ \ %%% |
543 \mbox{\begin{tabular}{l@ {\hspace{2mm}}c@ {\hspace{2mm}}l} |
543 \mbox{\begin{tabular}{l@ {\hspace{2mm}}c@ {\hspace{2mm}}l} |
544 @{term "new_proc s"} & @{text "\<equiv>"} & @{term "Max (current_procs s) + 1"} |
544 @{term "new_proc s"} & @{text "\<equiv>"} & @{term "Max (current_procs s) + 1"} |
545 \end{tabular}} |
545 \end{tabular}} |
546 \end{isabelle} |
546 \end{isabelle} |