Executable Logic Specifications: A New Approach

This paper discusses the use of logic programming techniques in the specification and verification of secure systems. The secure systems specifications discussed are formal and directly executable. The advantages of executable specifications are: (1) the specification is itself a prototype of the specified system, (2) incremental development of specification sis possible, (3)behavior exhibited by the specification when executed can be used to check conformity of the specification with security requirements such as DoD security policy, or discretionary and integrity policies.We discuss Horn clause logic, which has a procedural interpretation, and we use the predicate logic programming language, PROLOG, to specify and verify the functional correctness of secure systems, The PROLOG system possesses a powerful pattern-matching feature which is based on unification. An executable specification is very useful in checking completeness of a design and rectifying flaws in it before the expensive step of coding starts. In this paper, three examples of executable logic specifications are given a "login" command from military message system experiment, a security kernel for an imaginary computer architecture, and a simple downgrade trusted process. Executable logic specifications for secure systems could prove very useful to the DoD Computer Security Center in assessing computer products according to trusted computer system evaluation criteria.