|
|
|
Recall that a specification is a description of characteristics of a computer system or program. A security specification specifies desired security properties. (See Definition 19–7.) To this we add the definition of a formal specification.
Definition 20–1. A formal specification is a specification written in a formal language with a restricted syntax and well-defined semantics based on well-established mathematical concepts.
Formal specifications use a language with precise semantics. This avoids ambiguity and may allow for proofs of properties about the specification. These languages support precise descriptions of the behavior of system functions and generally eliminate implementation details.
|
EXAMPLE: One good example of the use of formal mathematical specifications can be seen in the Bell-LaPadula security policy model (see Section 5.2.3). The elements and rules of this security policy model are precisely defined in mathematical language. Using this well-defined specification, theorems were generated showing the consistency of the model rules with its axioms. Precise mathematical proofs of the theorems complete this model. Other formal specification languages resemble programming languages and are usually supported by automated tools that verify correct syntax and semantics of a specification in the language. |
Generally, the specification languages are supported by automated tools for verifying the correct use of the language syntax and semantics. Inductive verification, protocol verifiers, and model checkers use formal specification languages as input to the tools of the technique, making a formal specification a part of any formal verification technology. Formal specification is also important as a stand-alone technique. The specification may or may not be needed for some proof process. The process of writing formal specifications helps us to understand the design better and to see potential flaws, even without claims and proofs.
SPECIAL is a first-order logic-based language developed at SRI, International, as a stand-alone specification language. SPECIAL provides an excellent example of a nonprocedural and strongly typed specification language that is well suited for writing functional specifications, as described in Chapter 17. The strengths of SPECIAL are the richness of its expressive capability and its ability to describe inputs, constraints, errors, and outputs without implementation details. SPECIAL has a rich set of built-in operators, including set operations such as UNION and DIFF; logical operators such as AND, OR, and => (implies); universal and existential quantifiers (FORALL, EXISTS); IF/THEN/ELSE constructs; arithmetic operators; and many others. SPECIAL also has a mechanism for distinguishing an old value of a variable from a new value.
A specification in SPECIAL represents a module, and the specifier defines the scope of the module. Several modules can be used to describe a system. Two good reasons to make smaller modules are convenience and ease of manipulation, but another reason is to take advantage of the ability to hide information between modules.
A SPECIAL module specification has several sections for describing types, parameters, assertions, and functions. SPECIAL types are identified syntactically using keywords in capital letters. Two examples are the DESIGNATOR type, which allows the use of a type whose specifics are to be defined at a lower level of abstraction, and the BOOLEAN type, which includes the values TRUE and FALSE. SPECIAL also supports discrete sets, sets defined in terms of other types, and structured types. Parameters define constants and entities whose ability to change is outside the scope of the specification. Definitions are a shortcut for complex expressions that need to be used repeatedly. Global assertions can be made about the other elements of the module and can be used in proving theorems about the specification.
The heart of the SPECIAL specification is the functions, which define state variables and state transitions. Any function can be defined as private to the scope of the module in which that function is defined or as visible and addressable outside the specific module description. The visible functions define the external interface to the module. A visible function may have an exceptions clause that lists the conditions to be tested and passed for the effects of the function to take place. VFUNs describe variable data. Primitive VFUNs describe the system state variables, whereas derived VFUNs provide values determined by expressions involving primitive VFUNs, which have an initial value. VFUNs are viewed as functions that return a value to the caller and thus contribute to the definition of the system state. OFUNs and OVFUNs describe state transitions. They have exception sections as well as an effects section that describs changes in VFUN values. Like OFUNs, OVFUNs describe state transitions, but, like VFUNs, they also return a value and thus are state transition functions and contribute to the state of the system. Any function specification can contain "local" assertions that are specific to the function.
|
EXAMPLE: The specification below represents parts of the SPECIAL specification of the Bell-LaPadula Model. The give_access rule is a generalization of the give_read rule described in Section 5.2.4.2.
MODULE Bell_LaPadula_Model Give_access
TYPES
Subject_ID: DESIGNATOR;
Object_ID: DESIGNATOR;
Access_Mode: {OBSERVE_ONLY, ALTER_ONLY, OBSERVE_AND_ALTER};
Access: STRUCT_OF( Subject_ID subject;
Object_ID object;
Access_Mode mode);
FUNCTIONS
VFUN active (Object_ID object) -> BOOLEAN active:
HIDDEN;
INITIALLY
TRUE;
VFUN access_matrix () -> Accesses accesses:
HIDDEN;
INITIALLY
FORALL Access a: a INSET accesses => active (a.object);
OFUN give_access(Subject_ID giver; Access access);
ASSERTIONS
active(access.object) = TRUE;
EFFECTS
'access_matrix() = access_matrix() UNION (access);
END_MODULE
This example defines four types. The Subject_ID and Object_ID are to be described at a lower level of abstraction, and so are of type DESIGNATOR. Variables of type Access_Mode may take only the values OBSERVE_ONLY, ALTER_ONLY, and OBSERVE_AND_ALTER. The type Access is a structure with three fields—namely, a Subject_ID, an Object_ID, and an Access_Mode. The first VFUN defines the state variable active for an object to be TRUE. The second VFUN defines the state variable access_matrix to be the set of triplets of (subject, object, right). The OFUN defines the transition occurring when a new element is added to the matrix. It requires that the state variable active for the object be TRUE (in the ASSERTIONS). Then the value of the variable access_matrix after the transition is the value of that variable before the transition, with the additional access right added to the access_matrix variable. An interpretation of this specification is that the triples in active_matrix define the current set of access rights in the system and the active state variable for an object is TRUE if the object is in access_matrix—that is, if the object exists. |
|
|
|
| Top |