Verifying Abstract Information Flow Properties in Fault Tolerant Security Devices

  • Tim McComb
  • Luke Wildman
Part of the Lecture Notes in Computer Science book series (LNCS, volume 4260)


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.

Unable to display preview. Download preview PDF.


  1. 1.
    ISO/IEC 13568, Information Technology—Z Formal Specification Notation—Syntax, Type System and Semantics, 1st edn. 2002-07-01 (2002)Google Scholar
  2. 2.
    Behnke, R., Berghammer, R., Meyer, E., Schneider, P.: RELVIEW – a system for calculating with relations and relational programming. In: Astesiano, E. (ed.) ETAPS 1998 and FASE 1998. LNCS, vol. 1382, pp. 318–321. Springer, Heidelberg (1998)CrossRefGoogle Scholar
  3. 3.
    Clarke, E., Grumberg, O., Jha, S., Lu, Y., Veith, H.: Counterexample-guided abstraction refinement for symbolic model checking. J. ACM 50(5), 752–794 (2003)CrossRefMathSciNetGoogle Scholar
  4. 4.
    Clarke, E.M., Grumberg, O., Peled, D.A.: Model checking. MIT Press, Cambridge (1999)Google Scholar
  5. 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
  6. 6.
    McComb, T., Wildman, L.: SIFA: A tool for evaluation of high-grade security devices. In: Boyd, C., González Nieto, J.M. (eds.) ACISP 2005. LNCS, vol. 3574, pp. 230–241. Springer, Heidelberg (2005)CrossRefGoogle Scholar
  7. 7.
    MIL-STD. Procedures for performing a failure mode, effects and criticality analysis. Department of Defense USA (1629A)Google Scholar
  8. 8.
    U. S. Nuclear Regulatory Commission NRC. Fault Tree Handbook. NUREG-0492, Springfield (1981)Google Scholar
  9. 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
  10. 10.
    Rae, A., Fidge, C., Wildman, L.: Fault evaluation for security-critical communications devices. Computer 39(5), 61–68 (2006)CrossRefGoogle Scholar
  11. 11.
    Rae, A., Fidge, C., Wildman, L.: Information security fault mode evaluation for communications devices. IEEE Computer 39(3) (March 2006)Google Scholar
  12. 12.
    Rae, A.J., Fidge, C.J.: Information flow analysis for fail-secure devices. The Computer Journal 48(1), 17–26 (2005)CrossRefGoogle Scholar
  13. 13.
    Rushby, J.: Noninterference, transitivity, and channel-control security policies. Technical Report CSL-92-02, Computer Science Laboratory, SRI International (December 1992)Google Scholar
  14. 14.
    Sabelfeld, A., Myers, A.C.: Language-based information-flow security. IEEE Journal on Selected Areas in Communications 21(1), 5–19 (2003)CrossRefGoogle Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2006

Authors and Affiliations

  • Tim McComb
    • 1
  • Luke Wildman
    • 1
  1. 1.School of Information Technology and Electrical EngineeringThe University of QueenslandAustralia

Personalised recommendations