UCON is a Usage CONtrol model, which builds heavily on traditional access control models. It incorporates dynamic usage of protected objects and changes in decisions to allow further access to these objects as a result of usage. This extension is achieved through the introduction of two novel features: access decision continuity and attribute mutability.

In a UCON system, the user initiates a request for an object protected by the UCON system. The access decision depends on the policies and constraints for the particular subject, object and right combination, identiļ¬ed by (s, o, r). The request can either be granted or denied. Even if the request is initially granted, the usage session does not end. The coupling of attribute mutability and access decision continuity means that due to the usage of the protected object, the attributes of the subject and/or object may change. As a result of this change, the decision to allow access might also be reversed. The usage session remains at state accessing as long as the constraints allow the continued use of the object.

If the user ends the usage, the usage session moves to state end. If, however, the constraints lead to a denial of access after some time, the state moves to revoke and the user is no longer allowed access to the object. Figure shows the states in the UCON usage session.

Formal verification: Formal verification is the act of proving or disproving the correctness of intended algorithms underlying a system with respect to a certain formal specification or property, using formal methods of mathematics. The most widely used techniques for system or software verification

Simulation and testing

Deductive verification

Model checking

Model checking:

Model checking is a formal verification technique, in which a abstract model of a system is testing automatically to verify whether this model meets a given specification. Typically, the systems one has in mind are hardware or software systems, and the specification contains safety requirements such as the absence of deadlocks and similar critical states that can cause the system to crash. Model checking is a technique for automatically verifying correctness properties of finite-state systems.

SPIN Model checker:

Spin is a popular open-source software tool, used by thousands of people worldwide that can be used for the formal verification of distributed software systems. The tool was developed at Bell Labs in the original UNIX group of the Computing Sciences Research Center, starting in 1980. Spin model checker understand promela code and properties are express in Linear Temporal Logic.

PROMELA Language:

PROMELA (Process or Protocol Meta Language) is a verification modeling language. The language allows for the dynamic creation of concurrent processes to model, for example, distributed systems. In PROMELA models, communication via message channels can be defined to be synchronous or asynchronous. PROMELA models can be analyzed with the SPIN model checker, to verify that the modeled system produces the desired behavior.

PROMELA programs consist of processes, message channels, and variables. Processes are global objects that represent the concurrent entities of the distributed system. Message channels and variables can be declared either globally or locally within a process. Processes specify behavior, channels and global variables define the environment in which the processes run.

Temporal Logic:

Temporal logic is formalism for describing sequences of transitions between states in a reactive system. In the temporal logics that we will consider, time is not mentioned explicitly; instead, a formula might specify that eventually some designated state is reached, or that an error state is never entered.

There are three main ways to represent Temporal Logic:

CTL* (Computation Tree Logic*):

CTL* is powerful and complex logic. Often we need only the subset (fragment) of CTL*, such as LTL or CTL, in order determined properties specify.

CTL (Computation Tree Logic) Branching time:

CTL describes all possible time lines. CTL has the same operators like CTL*, however it has syntactic restrictions; it means that each temporal logical operator must directly follow one of these two path quantifiers (A or E). So for the CTL we have the following 10 basis operators: AX and EX; AF and EF; AG and EG; AU and EU; AR and ER.

LTL (Linear Temporal Logic) Linear time:

LTL describes single possible time line, All LTL formulas are properties of paths (as opposed to states). An LTL formula is interpreted with respect to a fixed path. Compare with CTL, the LTL is perhaps more intuitive and can express some properties CTL cannot (and vice versa). LTL is Linear because conceptually it is only about paths, as opposed to computation trees (CTL, where paths can branch).

Leave a Reply