[5]   

1. Intrusion Detection

One problem in information survivability is the recognition of new forms of attack. While we can accumulate exhaustive data on known attacks, novel intrusion techniques are likely to go undetected. One approach to this problem is to identify departures from baseline behavioral data. The inherently statistical nature of this approach seems to require human review of detected variation.

Another approach to this problem is to identify known system invariants and temporal properties and track the system's adherence to these specifications. While the fact that system specifications are adhered to is clearly not sufficient to identify all attacks, it provides an additional approach. When considering attacks on large distributed systems, it seems certain that we will need to depend on a diverse set of solutions to provide multiple overlapping lines of defense, detection and recovery.

Computational Logic has experience tracking specifications at run time for the purposes of uncovering implementation errors. Under DARPA sponsorship and in collaboration with the Open Group Research Institute, a mathematical specification for the Mach 3.0 kernel [Bevier 93] was written and run time tests implemented to ensure that the kernel complied with its specification. Errors were found that had not been found by conventional testing techniques. This work is now being extended to simplify the creation of specifications by designers and to track temporal behaviors by mapping abstract events in the model to operations in the code.

We believe this work holds promise for intrusion detection. It may even provide insight into corrective approaches.

In another effort that could potentially be related to intrusion detection we are working with Javasoft to create a formal definition of the Java Virtual Machine. The thrust of this effort is to ensure the safety of machines running potentially hostile applets on the Internet. While this work focuses on ensuring that intrusions cannot occur, the question arises as to whether the JVM's response to violation of it's requirements can be integrated into a larger survivability framework.

2. Background

CLI has long been at the forefront in applying mathematical modeling and machine assisted analysis to digital computing systems. We have constructed sophisticated theorem-proving environments, and we have performed more verifications using our tools than any other group of which we know. Our group collectively has over 150 man years of theorem-proving experience.

We have specified a large number of different systems. These systems are complex and in some cases involve commercial systems and processors.

• The formalization of Motorola's Complex Arithmetic Processor (CAP) digital signal processor, and the verification of algorithms running on its pipelined, super-scalar implementation.

• A mechanically checked proof of the correctness of the kernel of the AMD5K86 floating-point division algorithm, done in conjunction with Advanced Micro Devices. AMD has gone on to use our technology to prove the square root algorithm on the same chip (a change was made in response to problems uncovered in the course of proof) and to analyze cache behavior in their K7 chip.

• The ``CLI short stack'' [Bevier 89a], connects a chain of abstract machines starting with a gate-level hardware description and ending with an operational semantics for a simple high-level programming language.
  • Compiler. A compiler for the language @g(m)-Gypsy, proved to correctly translate programs into its target language, Piton [Young 89].

  • Assembler. An assembler for the Piton assembly language, proved to correctly assemble, link and load program for the FM9001 processor [Moore 88].

  • Microprocessor. A microprocessor, whose gate-level implementation is mathematically proved to satisfy a behavioral model of its instruction set [Hunt 92a].

  • Kernel. A small operating system kernel, whose implementation is proved correct at the machine code level [Bevier 89b].

• Formalization and correctness proofs for the fabricated FM9001 microprocessor [Hunt 92b, Hunt 92a].

• Formalization of a substantial part of the MC68020 Motorola microprocessor together with correctness proofs for object code programs including 21 of the 22 programs in the Berkeley Unix C string library [Yuan 92a, Yuan 92b].

• Model of an implementation of multitasking and task isolation and communication on a uniprocessor [Bevier 89b, Bevier 87], with correctness proof.

• The Encrypted Packet Interface [SmithMK 81] may be the first verified large scale model of a distributed system. It involved encryption and secure packet delivery across an unsecure network of computers.

CLI has also developed and supported state-of-the-art automated reasoning tools including the Gypsy Verification Environment [Akers 90] (no longer supported), Nqthm [Boyer 79, Boyer 88] and its interactive enhancement Pc-Nqthm [Kaufmann 88], and currently ACL2 [Kaufmann 94].

ACL2 is our most advanced tool for mathematical modeling and analysis of digital systems. It is a theorem proving system whose design was motivated by the inadequacies of its predecessors when used in large-scale verification projects. Foremost among those inadequacies is the fact that most logics are inefficient programming languages. We now recognize that an efficienctly executable logic has great importance for the models of microprocessors, operating systems, and languages that are typically constructed in verification projects. Execution allows us to corroborate them against the realities they model. Simulation of large scale systems stresses an inefficiently executable logic.

ACL2 also supports certain proof techniques not provided by its predecessor, for example congruence-based rewriting. In addition it encourages the reuse of previously developed libraries and collaboration on large verification projects.

3. REFERENCES

[Akers 90] Robert L. Akers, Bret A. Hartman, Lawrence M. Smith, Millard C. Taylor, William D. Young. Gypsy Verification Environment User's Manual Computational Logic Inc., 1990.

[Bevier 87] W.R. Bevier. A Verified Operating System Kernel. Technical Report CLI-11, Computational Logic, Inc., October, 1987. Ph.D. thesis, The University of Texas at Austin.

[Bevier 89a] W.R. Bevier, W.A. Hunt, Jr., J S. Moore, W.D. Young. An Approach to Systems Verification. Journal of Automated Reasoning 5(4):411-428, December, 1989.

[Bevier 89b] W.R. Bevier. Kit: A Study in Operating System Verification. IEEE Transactions on Software Engineering 15(11):1368-81, November, 1989. Also published as CLI Technical Report 28.

[Bevier 93] W.R. Bevier and L.M. Smith. A Mathematical Model of the Mach Kernel: Entities and Relations. Technical Report 88, Computational Logic, Inc., April, 1993.

[Boyer 79] R.S. Boyer and J S. Moore. A Computational Logic. Academic Press, New York, 1979.

[Boyer 88] R.S. Boyer and J S. Moore. A Computational Logic Handbook. Academic Press, Boston, 1988.

[Hunt 92a] W.A. Hunt, Jr. and Bishop Brock. A Formal HDL and its use in the FM9001 Verification. Proceedings of the Royal Society , 1992.

[Hunt 92b] B.C. Brock, W.A. Hunt, Jr., and W.D. Young. Introduction to a Formally Defined Hardware Description Language. In V. Stavridou, T.F. Melham, and R.T. Boute (editors), IFIP Transactions. Number A10: Theorem Provers in Circuit Designs. North Holland, 1992.

[Kaufmann 88] M.J. Kaufmann. A User's Manual for an Interactive Enhancement to the Boyer-Moore Theorem Prover. Technical Report 19, Computational Logic, Inc., May, 1988.

[Kaufmann 94] M.J. Kaufmann, J S. Moore. Design Goals of ACL2. Technical Report 101, Computational Logic, Inc., August, 1994.

[Moore 88] J S. Moore. PITON: A Verified Assembly Level Language. Technical Report 22, Computational Logic, Inc., 1988.

[SmithMK 81] M. K. Smith, A. Siebert, B. DiVito, and D. Good. A verified encrypted packet interface. Software Engineering Notes 6(3), July, 1981.

[Young 89] W.D. Young. A Mechanically Verified Code Generator. Technical Report 37, Computational Logic, Inc., January,1989.

[Yuan 92a] R.S. Boyer and Yuan Yu. Automated Correctness Proofs of Machine Code Programs for a Commercial Microprocessor. In D. Kapur (editor), Automated Deduction -- CADE-11, pages 416-430. Springer-Verlag, 1992.

[Yuan 92b] Y. Yu. Automated Proofs of Object Code for a Widely Used Microprocessor. Technical Report, The University of Texas at Austin, December, 1992.

Back to the Table of Contents
   [5]