Verifying Abstract Information Flow Properties in Fault Tolerant Security Devices
The verification of information flow properties of security devices is difficult because it involves the analysis of schematic diagrams, artwork, embedded software, etc. In addition, a typical security device has many modes, partial information flow, and needs to be fault tolerant. We propose a new approach to the verification of such devices based upon checking abstract information flow properties expressed as graphs. This approach has been implemented in software, and successfully used to find possible paths of information flow through security devices.
Unable to display preview. Download preview PDF.
- 1.ISO/IEC 13568, Information Technology—Z Formal Specification Notation—Syntax, Type System and Semantics, 1st edn. 2002-07-01 (2002)Google Scholar
- 4.Clarke, E.M., Grumberg, O., Peled, D.A.: Model checking. MIT Press, Cambridge (1999)Google Scholar
- 5.Fidge, C., McComb, T.: Tracing information flow through mode changes. In: Estivill-Castro, V., Dobbie, G. (eds.) Twenty-Ninth Australasian Computer Science Conference (ACSC 2006), Hobart, Australia. CRPIT, vol. 48, pp. 303–310. ACS (2006)Google Scholar
- 7.MIL-STD. Procedures for performing a failure mode, effects and criticality analysis. Department of Defense USA (1629A)Google Scholar
- 8.U. S. Nuclear Regulatory Commission NRC. Fault Tree Handbook. NUREG-0492, Springfield (1981)Google Scholar
- 9.Rae, A., Fidge, C.: Identifying critical components during information security evaluations. Journal of Research and Practice in Information Technology 37(4) (November 2005)Google Scholar
- 11.Rae, A., Fidge, C., Wildman, L.: Information security fault mode evaluation for communications devices. IEEE Computer 39(3) (March 2006)Google Scholar
- 13.Rushby, J.: Noninterference, transitivity, and channel-control security policies. Technical Report CSL-92-02, Computer Science Laboratory, SRI International (December 1992)Google Scholar