next up previous contents
Next: Example Up: 3. Adaptive security system Previous: 3.1.4.5 Non-repudiation and trusted

3.2 Use of formal security models

Allowed and unallowed interactions will usually be derived from a higher level security specification, the formal expression of a security policy: the formal security model.

Consider a finite state-machine model and an access control matrix with as rows subjects and as columns objects. Users, computer processes or computer hosts could be (both) subjects and objects. A subject could be anything that can trigger an event (logging on, starting a program or process, issuing a command, sending a network packet, giving an error message,...), an object anything that can be the target of a request or attack (a computer service, a user, a computer host,...). Suppose that at any given point in time, the state of these subjects and objects is known or can be retrieved by the security management service through the monitors. What is understood by ``state'' will have to follow from the type of subject or object and the information we are interested in, as defined by the scope of the risk analysis phase and the security policy. The entries in the matrix consist of vectors specifying access control conditions for the subjects from the rows to access the objects from the columns. If a subject accesses an object or tries to use a resource, the monitor checks its filtering rules to see whether it has to create an event to notify the inference engine. Such an event triggers the evaluation of the control conditions by the inference engine. The monitor that created the notification also provides the inference engine with a number of parameters to evaluate the conditions. The inference mechanism of the expert system would have to ensure the correctness of the transition to the next state, i.e. take the system from one secure state to another, thereby enforcing the security policy. If the information provided is not sufficient to evaluate certain rules, the engine sends requests to an appropriate (set of) monitors to provide it with the required details. When an event occurs, various elements of the system may change state -- the initiator of the access request, the target and the communications channel for instance.

The inference engine together with the access control conditions could enforce confidentiality and integrity of information flows as captured by formal models like Bell-LaPadula, Biba, Chinese Wall, Clark-Wilson and the like [GOL97, Chapter 3 p.25 ff.]. Shortcomings of formal models -- dynamic changes, transfer of access rights or modeling other aspects than confidentiality or integrity -- might be solved by creating additional rules that execute appropriate code.


  
Figure 3.5: Example of an access control condition matrix
\begin{figure}\par\vspace{0.3cm}
{\centering\begin{tabular}{\vert c\vert c\vert ...
... {\centering\emph{Note
-
ACV
=
Access
Control
Vector}\par }
\par\par\end{figure}

In order to detect attacks, not only the state of subjects and objects from the access control matrix must be known. In the case of network intrusion detection, information about the state of individual sessions is needed to detect various types of attack signatures (see for instance [PTA98] for examples of TCP/IP protocol weaknesses and [PAX98] for examples specific to TCP/IP applications like finger, FTP, portmapper and telnet).



 
next up previous contents
Next: Example Up: 3. Adaptive security system Previous: 3.1.4.5 Non-repudiation and trusted
(c) 1998, Filip Schepers