4.2 BEYOND CLASS (A1)
Copyright(c) Management Analytics, 1995 - All Rights Reserved
Most of the security enhancements envisioned for systems that will
provide features and assurance in addition to that already provided by
class (Al) systems are beyond current technology. The discussion below
is intended to guide future work and is derived from research and
development activities already underway in both the public and private
sectors. As more and better analysis techniques are developed, the
requirements for these systems will become more explicit. In the
future, use of formal verification will be extended to the source level
and covert timing channels will be more fully addressed. At this level
the design environment will become important and testing will be aided
by analysis of the formal top-level specification. Consideration will
be given to the correctness of the tools used in TCB development (e.g.,
compilers, assemblers, loaders) and to the correct functioning of the
hardware/firmware on which the TCB will run. Areas to be addressed by
systems beyond class (A1) include:
- System Architecture A demonstration (formal or otherwise)
must be given showing that requirements of self-protection and
completeness for reference monitors have been implemented in the TCB.
- Security Testing Although beyond the current
state-of-the-art, it is envisioned that some test-case generation will
be done automatically from the formal top-level specification or formal
lower-level specifications.
- Formal Specification and Verification The TCB must be
verified down to the source code level, using formal verification
methods where feasible. Formal verification of the source code of the
security-relevant portions of an operating system has proven to be a
difficult task. Two important considerations are the choice of a
high-level language whose semantics can be fully and formally expressed,
and a careful mapping, through successive stages, of the abstract formal
design to a formalization of the implementation in low-level
specifications. Experience has shown that only when the lowest level
specifications closely correspond to the actual code can code proofs be
successfully accomplished.
- Trusted Design Environment The TCB must be designed in a
trusted facility with only trusted (cleared) personnel.